Various changes to enable better CNF generation.

1 files changed, 124 insertions, 12 deletions

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 []