Various changes to enable better CNF generation.

9 files changed, 422 insertions, 223 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 426660a4..8872ef83 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1175,6 +1175,9 @@ extern void                Gia_MmStepStop( Gia_MmStep_t * p, int fVerbose );
 extern char *              Gia_MmStepEntryFetch( Gia_MmStep_t * p, int nBytes );
 extern void                Gia_MmStepEntryRecycle( Gia_MmStep_t * p, char * pEntry, int nBytes );
 extern int                 Gia_MmStepReadMemUsage( Gia_MmStep_t * p );
+/*=== giaMf.c ===========================================================*/
+extern void                Mf_ManSetDefaultPars( Jf_Par_t * pPars );
+extern Gia_Man_t *         Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
 /*=== giaMini.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManReadMiniAig( char * pFileName );
 extern void                Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
diff --git a/src/aig/gia/giaIso3.c b/src/aig/gia/giaIso3.c
index 18430a6c..a88a0569 100644
--- a/src/aig/gia/giaIso3.c
+++ b/src/aig/gia/giaIso3.c
@@ -34,74 +34,6 @@ static unsigned Iso_Compl[2] = { 0x8ba63e50, 0x14d87f02 }; // non-compl, compl
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of unique entries.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned Vec_IntUniqueHashKey( unsigned char * pStr, int nChars )
-{
-    static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319};
-    unsigned Key = 0; int c;
-    for ( c = 0; c < nChars; c++ )
-        Key += (unsigned)pStr[c] * s_BigPrimes[c & 3];
-    return Key;
-}
-static inline int * Vec_IntUniqueLookup( Vec_Int_t * vData, int i, int nIntSize, int * pNexts, int * pStart )
-{
-    int * pData = Vec_IntEntryP( vData, i*nIntSize );
-    for ( ; *pStart != -1; pStart = pNexts + *pStart )
-        if ( !memcmp( pData, Vec_IntEntryP(vData, *pStart*nIntSize), sizeof(int) * nIntSize ) )
-            return pStart;
-    return pStart;
-}
-static inline int Vec_IntUniqueCount( Vec_Int_t * vData, int nIntSize, Vec_Int_t ** pvMap )
-{
-    int nEntries  = Vec_IntSize(vData) / nIntSize;
-    int TableMask = (1 << Abc_Base2Log(nEntries)) - 1;
-    int * pTable  = ABC_FALLOC( int, TableMask+1 );
-    int * pNexts  = ABC_FALLOC( int, TableMask+1 );
-    int * pClass  = ABC_ALLOC( int, nEntries );
-    int i, Key, * pEnt, nUnique = 0;
-    assert( nEntries * nIntSize == Vec_IntSize(vData) );
-    for ( i = 0; i < nEntries; i++ )
-    {
-        pEnt = Vec_IntEntryP( vData, i*nIntSize );
-        Key  = TableMask & Vec_IntUniqueHashKey( (unsigned char *)pEnt, 4*nIntSize );
-        pEnt = Vec_IntUniqueLookup( vData, i, nIntSize, pNexts, pTable+Key );
-        if ( *pEnt == -1 )
-            *pEnt = i, nUnique++;
-        pClass[i] = *pEnt;
-    }
-    ABC_FREE( pTable );
-    ABC_FREE( pNexts );
-    if ( pvMap )
-        *pvMap = Vec_IntAllocArray( pClass, nEntries );
-    else
-        ABC_FREE( pClass );
-    return nUnique;
-}
-static inline Vec_Int_t * Vec_IntUniqifyHash( Vec_Int_t * vData, int nIntSize )
-{
-    Vec_Int_t * vMap, * vUnique;
-    int i, Ent, nUnique = Vec_IntUniqueCount( vData, nIntSize, &vMap );
-    vUnique = Vec_IntAlloc( nUnique * nIntSize );
-    Vec_IntForEachEntry( vMap, Ent, i )
-    {
-        if ( Ent < i ) continue;
-        assert( Ent == i );
-        Vec_IntPushArray( vUnique, Vec_IntEntryP(vData, i*nIntSize), nIntSize );
-    }
-    assert( Vec_IntSize(vUnique) == nUnique * nIntSize );
-    Vec_IntFree( vMap );
-    return vUnique;
-}
 
 /**Function*************************************************************
 
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c
new file mode 100644
index 00000000..c43b6aec
--- /dev/null
+++ b/src/aig/gia/giaMf.c
@@ -0,0 +1,62 @@
+/**CFile****************************************************************
+
+  FileName    [giaMf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaMf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/vec/vecSet.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mf_ManSetDefaultPars( Jf_Par_t * pPars )
+{
+    Jf_ManSetDefaultPars( pPars );
+}
+Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
+{
+    return Jf_ManPerformMapping( pGia, pPars );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 2f04b372..8cd50ce8 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -34,6 +34,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaJf.c \
     src/aig/gia/giaKf.c \
     src/aig/gia/giaLf.c \
+    src/aig/gia/giaMf.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMem.c \
     src/aig/gia/giaMfs.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3e0a26ff..cd945086 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -381,6 +381,7 @@ static int Abc_CommandAbc9If2                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Jf                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Kf                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Lf                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Mf                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Struct             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Trace              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Speedup            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -957,6 +958,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&jf",           Abc_CommandAbc9Jf,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&kf",           Abc_CommandAbc9Kf,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&lf",           Abc_CommandAbc9Lf,           0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&mf",           Abc_CommandAbc9Mf,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&struct",       Abc_CommandAbc9Struct,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&trace",        Abc_CommandAbc9Trace,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&speedup",      Abc_CommandAbc9Speedup,      0 );
@@ -1012,6 +1014,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Liveness",     "nck",           Abc_CommandNChooseK,                   0 );
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,         0 );
+    {
+//        extern Mf_ManTruthCount();
+//        Mf_ManTruthCount();
+    }
 
     {
         extern void Dar_LibStart();
@@ -31100,6 +31106,193 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char Buffer[200];
+    Jf_Par_t Pars, * pPars = &Pars;
+    Gia_Man_t * pNew; int c;
+    Mf_ManSetDefaultPars( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLDWaekmcgvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLutSize < 2 || pPars->nLutSize > pPars->nLutSizeMax )
+            {
+                Abc_Print( -1, "LUT size %d is not supported.\n", pPars->nLutSize );
+                goto usage;
+            }
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nCutNum = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutNum < 1 || pPars->nCutNum > pPars->nCutNumMax )
+            {
+                Abc_Print( -1, "This number of cuts (%d) is not supported.\n", pPars->nCutNum );
+                goto usage;
+            }
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nRounds = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRounds < 0 )
+                goto usage;
+            break;
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-A\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nRoundsEla = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRoundsEla < 0 )
+                goto usage;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-R\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            pPars->nRelaxRatio = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRelaxRatio < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-R\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            pPars->nCoarseLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCoarseLimit < 0 ) 
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            pPars->DelayTarget = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->DelayTarget <= 0.0 )
+                goto usage;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nVerbLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nVerbLimit < 0 )
+                goto usage;
+            break;
+        case 'a':
+            pPars->fAreaOnly ^= 1;
+            break;
+        case 'e':
+            pPars->fOptEdge ^= 1;
+            break;
+        case 'k':
+            pPars->fCoarsen ^= 1;
+            break;
+        case 'm':
+            pPars->fCutMin ^= 1;
+            break;
+        case 'c':
+            pPars->fGenCnf ^= 1;
+            break;
+        case 'g':
+            pPars->fPureAig ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Empty GIA network.\n" );
+        return 1;
+    }
+
+    pNew = Mf_ManPerformMapping( pAbc->pGia, pPars );
+    if ( pNew == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Lf(): Mapping into LUTs has failed.\n" );
+        return 1;
+    }
+    Abc_FrameUpdateGia( pAbc, pNew );
+    return 0;
+
+usage:
+    if ( pPars->DelayTarget == -1 )
+        sprintf(Buffer, "best possible" );
+    else
+        sprintf(Buffer, "%d", pPars->DelayTarget );
+    Abc_Print( -2, "usage: &mf [-KCFARLD num] [-akmcgvwh]\n" );
+    Abc_Print( -2, "\t           performs technology mapping of the network\n" );
+    Abc_Print( -2, "\t-K num   : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize );
+    Abc_Print( -2, "\t-C num   : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum );
+    Abc_Print( -2, "\t-F num   : the number of area flow rounds [default = %d]\n", pPars->nRounds );
+    Abc_Print( -2, "\t-A num   : the number of exact area rounds [default = %d]\n", pPars->nRoundsEla );
+    Abc_Print( -2, "\t-R num   : the delay relaxation ratio (num >= 0) [default = %d]\n", pPars->nRelaxRatio );
+    Abc_Print( -2, "\t-L num   : the fanout limit for coarsening XOR/MUX (num >= 2) [default = %d]\n", pPars->nCoarseLimit );
+    Abc_Print( -2, "\t-D num   : sets the delay constraint for the mapping [default = %s]\n", Buffer );
+    Abc_Print( -2, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
+    Abc_Print( -2, "\t-e       : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" );
+    Abc_Print( -2, "\t-k       : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
+    Abc_Print( -2, "\t-m       : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" );
+    Abc_Print( -2, "\t-c       : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "yes": "no" );
+    Abc_Print( -2, "\t-g       : toggles generating AIG without mapping [default = %s]\n", pPars->fPureAig? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : prints the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/map/mpm/mpmDsd.c b/src/map/mpm/mpmDsd.c
index 662c9bb4..4b25fcd6 100644
--- a/src/map/mpm/mpmDsd.c
+++ b/src/map/mpm/mpmDsd.c
@@ -629,6 +629,28 @@ static Mpm_Dsd_t s_DsdClass6[595] = {
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Mpm_ManGetTruthWithCnf( int Limit )
+{
+    Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
+    int i;
+    for ( i = 0; i < 595; i++ )
+        if ( s_DsdClass6[i].nClauses <= Limit )
+            Vec_WrdPush( vRes, s_DsdClass6[i].uTruth );
+    return vRes;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/misc/extra/extraUtilSupp.c b/src/misc/extra/extraUtilSupp.c
index a2e089bb..baf9f3f6 100644
--- a/src/misc/extra/extraUtilSupp.c
+++ b/src/misc/extra/extraUtilSupp.c
@@ -40,149 +40,6 @@ extern void         Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of unique entries.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned Vec_IntUniqueHashKeyDebug( unsigned char * pStr, int nChars, int TableMask )
-{
-    static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319};
-    unsigned Key = 0; int c;
-    for ( c = 0; c < nChars; c++ )
-    {
-        Key += (unsigned)pStr[c] * s_BigPrimes[c & 3];
-        printf( "%d : ", c );
-        printf( "%3d  ", pStr[c] );
-        printf( "%12u ", Key );
-        printf( "%12u ", Key&TableMask );
-        printf( "\n" );
-    }
-    return Key;
-}
-void Vec_IntUniqueProfile( Vec_Int_t * vData, int * pTable, int * pNexts, int TableMask, int nIntSize )
-{
-    int i, Key, Counter;
-    for ( i = 0; i <= TableMask; i++ )
-    {
-        Counter = 0;
-        for ( Key = pTable[i]; Key != -1; Key = pNexts[Key] )
-            Counter++;
-        if ( Counter < 7 )
-            continue;
-        printf( "%d\n", Counter );
-        for ( Key = pTable[i]; Key != -1; Key = pNexts[Key] )
-        {
-            Extra_PrintBinary( stdout, (unsigned *)Vec_IntEntryP(vData, Key*nIntSize), 40 ), printf( "\n" );
-//            Vec_IntUniqueHashKeyDebug( (unsigned char *)Vec_IntEntryP(vData, Key*nIntSize), 4*nIntSize, TableMask );
-        }
-    }
-    printf( "\n" );
-}
-
-
-static inline unsigned Vec_IntUniqueHashKey2( unsigned char * pStr, int nChars )
-{
-    static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319};
-    unsigned Key = 0; int c;
-    for ( c = 0; c < nChars; c++ )
-        Key += (unsigned)pStr[c] * s_BigPrimes[c & 3];
-    return Key;
-}
-
-static inline unsigned Vec_IntUniqueHashKey( unsigned char * pStr, int nChars )
-{
-    static unsigned s_BigPrimes[16] = 
-    {
-        0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
-        0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055
-    };
-    static unsigned s_BigPrimes2[16] = 
-    {
-        0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035,
-        0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10
-    };
-    unsigned Key = 0; int c;
-    for ( c = 0; c < nChars; c++ )
-        Key += s_BigPrimes2[(2*c)&15]   * s_BigPrimes[(unsigned)pStr[c] & 15] +
-               s_BigPrimes2[(2*c+1)&15] * s_BigPrimes[(unsigned)pStr[c] >> 4];
-    return Key;
-}
-static inline int * Vec_IntUniqueLookup( Vec_Int_t * vData, int i, int nIntSize, int * pNexts, int * pStart )
-{
-    int * pData = Vec_IntEntryP( vData, i*nIntSize );
-    for ( ; *pStart != -1; pStart = pNexts + *pStart )
-        if ( !memcmp( pData, Vec_IntEntryP(vData, *pStart*nIntSize), sizeof(int) * nIntSize ) )
-            return pStart;
-    return pStart;
-}
-static inline int Vec_IntUniqueCount( Vec_Int_t * vData, int nIntSize, Vec_Int_t ** pvMap )
-{
-    int nEntries  = Vec_IntSize(vData) / nIntSize;
-    int TableMask = (1 << Abc_Base2Log(nEntries)) - 1;
-    int * pTable  = ABC_FALLOC( int, TableMask+1 );
-    int * pNexts  = ABC_FALLOC( int, TableMask+1 );
-    int * pClass  = ABC_ALLOC( int, nEntries );
-    int i, Key, * pEnt, nUnique = 0;
-    assert( nEntries * nIntSize == Vec_IntSize(vData) );
-    for ( i = 0; i < nEntries; i++ )
-    {
-        pEnt = Vec_IntEntryP( vData, i*nIntSize );
-        Key  = TableMask & Vec_IntUniqueHashKey( (unsigned char *)pEnt, 4*nIntSize );
-        pEnt = Vec_IntUniqueLookup( vData, i, nIntSize, pNexts, pTable+Key );
-        if ( *pEnt == -1 )
-            *pEnt = i, nUnique++;
-        pClass[i] = *pEnt;
-    }
-//    Vec_IntUniqueProfile( vData, pTable, pNexts, TableMask, nIntSize );
-    ABC_FREE( pTable );
-    ABC_FREE( pNexts );
-    if ( pvMap )
-        *pvMap = Vec_IntAllocArray( pClass, nEntries );
-    else
-        ABC_FREE( pClass );
-    return nUnique;
-}
-static inline Vec_Int_t * Vec_IntUniqifyHash( Vec_Int_t * vData, int nIntSize )
-{
-    Vec_Int_t * vMap, * vUnique;
-    int i, Ent, nUnique = Vec_IntUniqueCount( vData, nIntSize, &vMap );
-    vUnique = Vec_IntAlloc( nUnique * nIntSize );
-    Vec_IntForEachEntry( vMap, Ent, i )
-    {
-        if ( Ent < i ) continue;
-        assert( Ent == i );
-        Vec_IntPushArray( vUnique, Vec_IntEntryP(vData, i*nIntSize), nIntSize );
-    }
-    assert( Vec_IntSize(vUnique) == nUnique * nIntSize );
-    Vec_IntFree( vMap );
-    return vUnique;
-}
-static inline Vec_Wrd_t * Vec_WrdUniqifyHash( Vec_Wrd_t * vData, int nWordSize )
-{
-    Vec_Int_t * vResInt;
-    Vec_Int_t * vDataInt = (Vec_Int_t *)vData;
-    vDataInt->nSize *= 2;
-    vDataInt->nCap *= 2;
-    vResInt = Vec_IntUniqifyHash( vDataInt, 2 * nWordSize );
-    vDataInt->nSize /= 2;
-    vDataInt->nCap /= 2;
-    vResInt->nSize /= 2;
-    vResInt->nCap /= 2;
-    return (Vec_Wrd_t *)vResInt;
-}
-static inline word * Vec_WrdLimit( Vec_Wrd_t * p )
-{
-    return p->pArray + p->nSize;
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Generate m-out-of-n vectors.]
 
   Description []
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 824846b4..535a15ef 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -331,18 +331,6 @@ static inline int ** Vec_IntArrayP( Vec_Int_t * p )
 {
     return &p->pArray;
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static inline int * Vec_IntLimit( Vec_Int_t * p )
 {
     return p->pArray + p->nSize;
@@ -1317,6 +1305,130 @@ static inline int Vec_IntCountUnique( Vec_Int_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of unique entries.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Vec_IntUniqueHashKeyDebug( unsigned char * pStr, int nChars, int TableMask )
+{
+    static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319};
+    unsigned Key = 0; int c;
+    for ( c = 0; c < nChars; c++ )
+    {
+        Key += (unsigned)pStr[c] * s_BigPrimes[c & 3];
+        printf( "%d : ", c );
+        printf( "%3d  ", pStr[c] );
+        printf( "%12u ", Key );
+        printf( "%12u ", Key&TableMask );
+        printf( "\n" );
+    }
+    return Key;
+}
+static inline void Vec_IntUniqueProfile( Vec_Int_t * vData, int * pTable, int * pNexts, int TableMask, int nIntSize )
+{
+    int i, Key, Counter;
+    for ( i = 0; i <= TableMask; i++ )
+    {
+        Counter = 0;
+        for ( Key = pTable[i]; Key != -1; Key = pNexts[Key] )
+            Counter++;
+        if ( Counter < 7 )
+            continue;
+        printf( "%d\n", Counter );
+        for ( Key = pTable[i]; Key != -1; Key = pNexts[Key] )
+        {
+//            Extra_PrintBinary( stdout, (unsigned *)Vec_IntEntryP(vData, Key*nIntSize), 40 ), printf( "\n" );
+//            Vec_IntUniqueHashKeyDebug( (unsigned char *)Vec_IntEntryP(vData, Key*nIntSize), 4*nIntSize, TableMask );
+        }
+    }
+    printf( "\n" );
+}
+
+static inline unsigned Vec_IntUniqueHashKey2( unsigned char * pStr, int nChars )
+{
+    static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319};
+    unsigned Key = 0; int c;
+    for ( c = 0; c < nChars; c++ )
+        Key += (unsigned)pStr[c] * s_BigPrimes[c & 3];
+    return Key;
+}
+
+static inline unsigned Vec_IntUniqueHashKey( unsigned char * pStr, int nChars )
+{
+    static unsigned s_BigPrimes[16] = 
+    {
+        0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
+        0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055
+    };
+    static unsigned s_BigPrimes2[16] = 
+    {
+        0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035,
+        0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10
+    };
+    unsigned Key = 0; int c;
+    for ( c = 0; c < nChars; c++ )
+        Key += s_BigPrimes2[(2*c)&15]   * s_BigPrimes[(unsigned)pStr[c] & 15] +
+               s_BigPrimes2[(2*c+1)&15] * s_BigPrimes[(unsigned)pStr[c] >> 4];
+    return Key;
+}
+static inline int * Vec_IntUniqueLookup( Vec_Int_t * vData, int i, int nIntSize, int * pNexts, int * pStart )
+{
+    int * pData = Vec_IntEntryP( vData, i*nIntSize );
+    for ( ; *pStart != -1; pStart = pNexts + *pStart )
+        if ( !memcmp( pData, Vec_IntEntryP(vData, *pStart*nIntSize), sizeof(int) * nIntSize ) )
+            return pStart;
+    return pStart;
+}
+static inline int Vec_IntUniqueCount( Vec_Int_t * vData, int nIntSize, Vec_Int_t ** pvMap )
+{
+    int nEntries  = Vec_IntSize(vData) / nIntSize;
+    int TableMask = (1 << Abc_Base2Log(nEntries)) - 1;
+    int * pTable  = ABC_FALLOC( int, TableMask+1 );
+    int * pNexts  = ABC_FALLOC( int, TableMask+1 );
+    int * pClass  = ABC_ALLOC( int, nEntries );
+    int i, Key, * pEnt, nUnique = 0;
+    assert( nEntries * nIntSize == Vec_IntSize(vData) );
+    for ( i = 0; i < nEntries; i++ )
+    {
+        pEnt = Vec_IntEntryP( vData, i*nIntSize );
+        Key  = TableMask & Vec_IntUniqueHashKey( (unsigned char *)pEnt, 4*nIntSize );
+        pEnt = Vec_IntUniqueLookup( vData, i, nIntSize, pNexts, pTable+Key );
+        if ( *pEnt == -1 )
+            *pEnt = i, nUnique++;
+        pClass[i] = *pEnt;
+    }
+//    Vec_IntUniqueProfile( vData, pTable, pNexts, TableMask, nIntSize );
+    ABC_FREE( pTable );
+    ABC_FREE( pNexts );
+    if ( pvMap )
+        *pvMap = Vec_IntAllocArray( pClass, nEntries );
+    else
+        ABC_FREE( pClass );
+    return nUnique;
+}
+static inline Vec_Int_t * Vec_IntUniqifyHash( Vec_Int_t * vData, int nIntSize )
+{
+    Vec_Int_t * vMap, * vUnique;
+    int i, Ent, nUnique = Vec_IntUniqueCount( vData, nIntSize, &vMap );
+    vUnique = Vec_IntAlloc( nUnique * nIntSize );
+    Vec_IntForEachEntry( vMap, Ent, i )
+    {
+        if ( Ent < i ) continue;
+        assert( Ent == i );
+        Vec_IntPushArray( vUnique, Vec_IntEntryP(vData, i*nIntSize), nIntSize );
+    }
+    assert( Vec_IntSize(vUnique) == nUnique * nIntSize );
+    Vec_IntFree( vMap );
+    return vUnique;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Comparison procedure for two integers.]
 
   Description []
diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index 9c33a5ba..c765dd8d 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -317,6 +317,10 @@ static inline word * Vec_WrdArray( Vec_Wrd_t * p )
 {
     return p->pArray;
 }
+static inline word * Vec_WrdLimit( Vec_Wrd_t * p )
+{
+    return p->pArray + p->nSize;
+}
 
 /**Function*************************************************************
 
@@ -1080,6 +1084,19 @@ static inline void Vec_WrdUniqify( Vec_Wrd_t * p )
             p->pArray[k++] = p->pArray[i];
     p->nSize = k;
 }
+static inline Vec_Wrd_t * Vec_WrdUniqifyHash( Vec_Wrd_t * vData, int nWordSize )
+{
+    Vec_Int_t * vResInt;
+    Vec_Int_t * vDataInt = (Vec_Int_t *)vData;
+    vDataInt->nSize *= 2;
+    vDataInt->nCap *= 2;
+    vResInt = Vec_IntUniqifyHash( vDataInt, 2 * nWordSize );
+    vDataInt->nSize /= 2;
+    vDataInt->nCap /= 2;
+    vResInt->nSize /= 2;
+    vResInt->nCap /= 2;
+    return (Vec_Wrd_t *)vResInt;
+}
 
 /**Function*************************************************************