ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
FxchSCHashTable.c
Go to the documentation of this file.
1
18#include "Fxch.h"
19
20#if (__GNUC__ >= 8)
21 #pragma GCC diagnostic ignored "-Wimplicit-fallthrough"
22#endif
23
25
29static inline void MurmurHash3_x86_32 ( const void* key,
30 int len,
31 uint32_t seed,
32 void* out )
33{
34 const uint8_t* data = (const uint8_t*)key;
35 const int nblocks = len / 4;
36
37 uint32_t h1 = seed;
38
39 const uint32_t c1 = 0xcc9e2d51;
40 const uint32_t c2 = 0x1b873593;
41
42 const uint8_t * tail;
43 uint32_t k1;
44
45 //----------
46 // body
47
48 const uint32_t * blocks = (const uint32_t *)(data + nblocks*4);
49 int i;
50
51 for(i = -nblocks; i; i++)
52 {
53 uint32_t k1 = blocks[i];
54
55 k1 *= c1;
56 k1 = (k1 << 15) | (k1 >> (32 - 15));
57 k1 *= c2;
58
59 h1 ^= k1;
60 h1 = (h1 << 13) | (h1 >> (32 - 13));
61 h1 = h1*5+0xe6546b64;
62 }
63
64 //----------
65 // tail
66
67 tail = (const uint8_t*)(data + nblocks*4);
68
69 k1 = 0;
70
71 switch(len & 3)
72 {
73 case 3: k1 ^= tail[2] << 16;
74 case 2: k1 ^= tail[1] << 8;
75 case 1: k1 ^= tail[0];
76 k1 *= c1; k1 = (k1 << 15) | (k1 >> (32 - 15)); k1 *= c2; h1 ^= k1;
77 };
78
79 //----------
80 // finalization
81
82 h1 ^= len;
83
84 h1 ^= h1 >> 16;
85 h1 *= 0x85ebca6b;
86 h1 ^= h1 >> 13;
87 h1 *= 0xc2b2ae35;
88 h1 ^= h1 >> 16;
89
90 *(uint32_t*)out = h1;
91}
92
94 int nEntries )
95{
97 int nBits = Abc_Base2Log( nEntries + 1 );
98
99
100 pSCHashTable->pFxchMan = pFxchMan;
101 pSCHashTable->SizeMask = (1 << nBits) - 1;
102 pSCHashTable->pBins = ABC_CALLOC( Fxch_SCHashTable_Entry_t, pSCHashTable->SizeMask + 1 );
103
104 return pSCHashTable;
105}
106
108{
109 unsigned i;
110 for ( i = 0; i <= pSCHashTable->SizeMask; i++ )
111 ABC_FREE( pSCHashTable->pBins[i].vSCData );
112 Vec_IntErase( &pSCHashTable->vSubCube0 );
113 Vec_IntErase( &pSCHashTable->vSubCube1 );
114 ABC_FREE( pSCHashTable->pBins );
115 ABC_FREE( pSCHashTable );
116}
117
118static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableBin( Fxch_SCHashTable_t* pSCHashTable,
119 unsigned int SubCubeID )
120{
121 return pSCHashTable->pBins + (SubCubeID & pSCHashTable->SizeMask);
122}
123
124static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable,
125 Vec_Wec_t* vCubes,
126 Fxch_SubCube_t* pSCData0,
127 Fxch_SubCube_t* pSCData1 )
128{
129 Vec_Int_t* vCube0 = Vec_WecEntry( vCubes, pSCData0->iCube ),
130 * vCube1 = Vec_WecEntry( vCubes, pSCData1->iCube );
131
132 int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pSCData0->iCube * pSCHashTable->pFxchMan->nSizeOutputID ),
133 * pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pSCData1->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
134 int i, Result = 0;
135
136 if ( !Vec_IntSize( vCube0 ) ||
137 !Vec_IntSize( vCube1 ) ||
138 Vec_IntEntry( vCube0, 0 ) != Vec_IntEntry( vCube1, 0 ) ||
139 pSCData0->Id != pSCData1->Id )
140 return 0;
141
142 for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID && Result == 0; i++ )
143 Result = ( pOutputID0[i] & pOutputID1[i] );
144
145 if ( Result == 0 )
146 return 0;
147
148 Vec_IntClear( &pSCHashTable->vSubCube0 );
149 Vec_IntClear( &pSCHashTable->vSubCube1 );
150
151 if ( pSCData0->iLit1 > 0 && pSCData1->iLit1 > 0 &&
152 ( Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) ||
153 Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ||
154 Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) ||
155 Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ) )
156 return 0;
157
158 if ( pSCData0->iLit0 > 0 )
159 Vec_IntAppendSkip( &pSCHashTable->vSubCube0, vCube0, pSCData0->iLit0 );
160 else
161 Vec_IntAppend( &pSCHashTable->vSubCube0, vCube0 );
162
163 if ( pSCData1->iLit0 > 0 )
164 Vec_IntAppendSkip( &pSCHashTable->vSubCube1, vCube1, pSCData1->iLit0 );
165 else
166 Vec_IntAppend( &pSCHashTable->vSubCube1, vCube1 );
167
168 if ( pSCData0->iLit1 > 0)
169 Vec_IntDrop( &pSCHashTable->vSubCube0,
170 pSCData0->iLit0 < pSCData0->iLit1 ? pSCData0->iLit1 - 1 : pSCData0->iLit1 );
171
172 if ( pSCData1->iLit1 > 0 )
173 Vec_IntDrop( &pSCHashTable->vSubCube1,
174 pSCData1->iLit0 < pSCData1->iLit1 ? pSCData1->iLit1 - 1 : pSCData1->iLit1 );
175
176 return Vec_IntEqual( &pSCHashTable->vSubCube0, &pSCHashTable->vSubCube1 );
177}
178
180 Vec_Wec_t* vCubes,
181 uint32_t SubCubeID,
182 uint32_t iCube,
183 uint32_t iLit0,
184 uint32_t iLit1,
185 char fUpdate )
186{
187 int iNewEntry;
188 int Pairs = 0;
189 uint32_t BinID;
191 Fxch_SubCube_t* pNewEntry;
192 int iEntry;
193
194 MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
195 pBin = Fxch_SCHashTableBin( pSCHashTable, BinID );
196
197 if ( pBin->vSCData == NULL )
198 {
199 pBin->vSCData = ABC_CALLOC( Fxch_SubCube_t, 16 );
200 pBin->Size = 0;
201 pBin->Cap = 16;
202 }
203 else if ( pBin->Size == pBin->Cap )
204 {
205 assert(pBin->Cap <= 0xAAAA);
206 pBin->Cap = ( pBin->Cap >> 1 ) * 3;
207 pBin->vSCData = ABC_REALLOC( Fxch_SubCube_t, pBin->vSCData, pBin->Cap );
208 }
209
210 iNewEntry = pBin->Size++;
211 pBin->vSCData[iNewEntry].Id = SubCubeID;
212 pBin->vSCData[iNewEntry].iCube = iCube;
213 pBin->vSCData[iNewEntry].iLit0 = iLit0;
214 pBin->vSCData[iNewEntry].iLit1 = iLit1;
215 pSCHashTable->nEntries++;
216
217 if ( pBin->Size == 1 )
218 return 0;
219
220 pNewEntry = &( pBin->vSCData[iNewEntry] );
221 for ( iEntry = 0; iEntry < (int)pBin->Size - 1; iEntry++ )
222 {
223 Fxch_SubCube_t* pEntry = &( pBin->vSCData[iEntry] );
224 int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
225 int* pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pNewEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
226 int Result = 0;
227 int Base;
228 int iNewDiv = -1, i, z;
229
230 if ( (pEntry->iLit1 != 0 && pNewEntry->iLit1 == 0) || (pEntry->iLit1 == 0 && pNewEntry->iLit1 != 0) )
231 continue;
232
233 if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, pEntry, pNewEntry ) )
234 continue;
235
236 if ( ( pEntry->iLit0 == 0 ) || ( pNewEntry->iLit0 == 0 ) )
237 {
238 Vec_Int_t* vCube0 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->iCube ),
239 * vCube1 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pNewEntry->iCube );
240
241 if ( Vec_IntSize( vCube0 ) > Vec_IntSize( vCube1 ) )
242 {
243 Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->iCube );
244 Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->iCube );
245 }
246 else
247 {
248 Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->iCube );
249 Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->iCube );
250 }
251
252 continue;
253 }
254
255 Base = Fxch_DivCreate( pSCHashTable->pFxchMan, pEntry, pNewEntry );
256
257 if ( Base < 0 )
258 continue;
259
260 for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID; i++ )
261 Result += Fxch_CountOnes( pOutputID0[i] & pOutputID1[i] );
262
263 for ( z = 0; z < Result; z++ )
264 iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base );
265
266 Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->iCube );
267 Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->iCube );
268
269 Pairs++;
270 }
271
272 return Pairs;
273}
274
276 Vec_Wec_t* vCubes,
277 uint32_t SubCubeID,
278 uint32_t iCube,
279 uint32_t iLit0,
280 uint32_t iLit1,
281 char fUpdate )
282{
283 int iEntry;
284 int Pairs = 0;
285 uint32_t BinID;
287 Fxch_SubCube_t* pEntry;
288 int idx;
289
290 MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
291
292 pBin = Fxch_SCHashTableBin( pSCHashTable, BinID );
293
294 if ( pBin->Size == 1 )
295 {
296 pBin->Size = 0;
297 return 0;
298 }
299
300 for ( iEntry = 0; iEntry < (int)pBin->Size; iEntry++ )
301 if ( pBin->vSCData[iEntry].iCube == iCube )
302 break;
303
304 assert( ( iEntry != (int)pBin->Size ) && ( pBin->Size != 0 ) );
305
306 pEntry = &( pBin->vSCData[iEntry] );
307 for ( idx = 0; idx < (int)pBin->Size; idx++ )
308 if ( idx != iEntry )
309 {
310 int Base,
311 iDiv = -1;
312
313 int i, z,
314 iCube0,
315 iCube1;
316
317 Fxch_SubCube_t* pNextEntry = &( pBin->vSCData[idx] );
318 Vec_Int_t* vDivCubePairs;
319 int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
320 int* pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pNextEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
321 int Result = 0;
322
323 if ( (pEntry->iLit1 != 0 && pNextEntry->iLit1 == 0) || (pEntry->iLit1 == 0 && pNextEntry->iLit1 != 0) )
324 continue;
325
326 if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, pEntry, pNextEntry )
327 || pEntry->iLit0 == 0
328 || pNextEntry->iLit0 == 0 )
329 continue;
330
331 Base = Fxch_DivCreate( pSCHashTable->pFxchMan, pNextEntry, pEntry );
332
333 if ( Base < 0 )
334 continue;
335
336 for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID; i++ )
337 Result += Fxch_CountOnes( pOutputID0[i] & pOutputID1[i] );
338
339 for ( z = 0; z < Result; z++ )
340 iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base );
341
342 vDivCubePairs = Vec_WecEntry( pSCHashTable->pFxchMan->vDivCubePairs, iDiv );
343 Vec_IntForEachEntryDouble( vDivCubePairs, iCube0, iCube1, i )
344 if ( ( iCube0 == (int)pNextEntry->iCube && iCube1 == (int)pEntry->iCube ) ||
345 ( iCube0 == (int)pEntry->iCube && iCube1 == (int)pNextEntry->iCube ) )
346 {
347 Vec_IntDrop( vDivCubePairs, i+1 );
348 Vec_IntDrop( vDivCubePairs, i );
349 }
350 if ( Vec_IntSize( vDivCubePairs ) == 0 )
351 Vec_IntErase( vDivCubePairs );
352
353 Pairs++;
354 }
355
356 memmove(pBin->vSCData + iEntry, pBin->vSCData + iEntry + 1, (pBin->Size - iEntry - 1) * sizeof(*pBin->vSCData));
357 pBin->Size -= 1;
358
359 return Pairs;
360}
361
363{
364 unsigned int Memory = sizeof ( Fxch_SCHashTable_t );
365
366 Memory += sizeof( Fxch_SubCube_t ) * ( pHashTable->SizeMask + 1 );
367
368 return Memory;
369}
370
372{
373 int Memory;
374 printf( "SubCube Hash Table at %p\n", ( void* )pHashTable );
375 printf("%20s %20s\n", "nEntries",
376 "Memory Usage (MB)" );
377
378 Memory = Fxch_SCHashTableMemory( pHashTable );
379 printf("%20d %18.2f\n", pHashTable->nEntries,
380 ( ( double ) Memory / 1048576 ) );
381}
382
385
void Fxch_SCHashTablePrint(Fxch_SCHashTable_t *pHashTable)
Fxch_SCHashTable_t * Fxch_SCHashTableCreate(Fxch_Man_t *pFxchMan, int nEntries)
int Fxch_SCHashTableRemove(Fxch_SCHashTable_t *pSCHashTable, Vec_Wec_t *vCubes, uint32_t SubCubeID, uint32_t iCube, uint32_t iLit0, uint32_t iLit1, char fUpdate)
unsigned int Fxch_SCHashTableMemory(Fxch_SCHashTable_t *pHashTable)
void Fxch_SCHashTableDelete(Fxch_SCHashTable_t *pSCHashTable)
int Fxch_SCHashTableInsert(Fxch_SCHashTable_t *pSCHashTable, Vec_Wec_t *vCubes, uint32_t SubCubeID, uint32_t iCube, uint32_t iLit0, uint32_t iLit1, char fUpdate)
struct Fxch_SCHashTable_t_ Fxch_SCHashTable_t
Definition Fxch.h:39
int Fxch_DivAdd(Fxch_Man_t *pFxchMan, int fUpdate, int fSingleCube, int fBase)
Definition FxchDiv.c:228
struct Fxch_SubCube_t_ Fxch_SubCube_t
Definition Fxch.h:38
unsigned int uint32_t
Definition Fxch.h:32
int Fxch_DivCreate(Fxch_Man_t *pFxchMan, Fxch_SubCube_t *pSubCube0, Fxch_SubCube_t *pSubCube1)
Definition FxchDiv.c:112
ABC_NAMESPACE_HEADER_START typedef unsigned char uint8_t
Definition Fxch.h:31
struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t
Definition Fxch.h:40
int Fxch_DivRemove(Fxch_Man_t *pFxchMan, int fUpdate, int fSingleCube, int fBase)
Definition FxchDiv.c:291
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
enum keys key
Definition main.h:25
struct Fxch_Man_t_ Fxch_Man_t
TYPEDEF DECLARATIONS ///.
Definition plaFxch.c:42
Vec_Int_t * vSCC
Definition Fxch.h:124
Vec_Int_t * vOutputID
Definition Fxch.h:112
int nSizeOutputID
Definition Fxch.h:114
Vec_Wec_t * vDivCubePairs
Definition Fxch.h:106
uint32_t Cap
Definition Fxch.h:73
Fxch_SubCube_t * vSCData
Definition Fxch.h:71
uint32_t Size
Definition Fxch.h:72
Fxch_SCHashTable_Entry_t * pBins
Definition Fxch.h:80
Vec_Int_t vSubCube1
Definition Fxch.h:86
unsigned int SizeMask
Definition Fxch.h:82
Fxch_Man_t * pFxchMan
Definition Fxch.h:78
unsigned int nEntries
Definition Fxch.h:81
Vec_Int_t vSubCube0
Definition Fxch.h:85
uint32_t iLit1
Definition Fxch.h:64
uint32_t Id
Definition Fxch.h:61
uint32_t iLit0
Definition Fxch.h:63
uint32_t iCube
Definition Fxch.h:62
#define assert(ex)
Definition util_old.h:213
char * memmove()
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42