1 /**CFile****************************************************************
2
3 FileName [ FxchMan.c ]
4
5 PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
6
7 Synopsis [ Fxch Manager implementation ]
8
9 Author [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
10
11 Affiliation [ UFRGS ]
12
13 Date [ Ver. 1.0. Started - March 6, 2016. ]
14
15 Revision []
16
17 ***********************************************************************/
18 #include "Fxch.h"
19
20 ABC_NAMESPACE_IMPL_START
21
22 ////////////////////////////////////////////////////////////////////////
23 /// LOCAL FUNCTIONS DEFINITIONS ///
24 ////////////////////////////////////////////////////////////////////////
Fxch_ManSCAddRemove(Fxch_Man_t * pFxchMan,unsigned int SubCubeID,unsigned int iCube,unsigned int iLit0,unsigned int iLit1,char fAdd,char fUpdate)25 static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan,
26 unsigned int SubCubeID,
27 unsigned int iCube,
28 unsigned int iLit0,
29 unsigned int iLit1,
30 char fAdd,
31 char fUpdate )
32 {
33 int ret = 0;
34
35 if ( fAdd )
36 {
37 ret = Fxch_SCHashTableInsert( pFxchMan->pSCHashTable, pFxchMan->vCubes,
38 SubCubeID,
39 iCube, iLit0, iLit1, fUpdate );
40 }
41 else
42 {
43 ret = Fxch_SCHashTableRemove( pFxchMan->pSCHashTable, pFxchMan->vCubes,
44 SubCubeID,
45 iCube, iLit0, iLit1, fUpdate );
46 }
47
48 return ret;
49 }
50
51
Fxch_ManDivSingleCube(Fxch_Man_t * pFxchMan,int iCube,int fAdd,int fUpdate)52 static inline int Fxch_ManDivSingleCube( Fxch_Man_t* pFxchMan,
53 int iCube,
54 int fAdd,
55 int fUpdate )
56 {
57 Vec_Int_t* vCube = Vec_WecEntry( pFxchMan->vCubes, iCube );
58 int i, k,
59 Lit0,
60 Lit1,
61 fSingleCube = 1,
62 fBase = 0;
63
64 if ( Vec_IntSize( vCube ) < 2 )
65 return 0;
66
67 Vec_IntForEachEntryStart( vCube, Lit0, i, 1)
68 Vec_IntForEachEntryStart( vCube, Lit1, k, (i + 1) )
69 {
70 int * pOutputID, nOnes, j, z;
71 assert( Lit0 < Lit1 );
72
73 Vec_IntClear( pFxchMan->vCubeFree );
74 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( Abc_LitNot( Lit0 ), 0 ) );
75 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( Abc_LitNot( Lit1 ), 1 ) );
76
77 pOutputID = Vec_IntEntryP( pFxchMan->vOutputID, iCube * pFxchMan->nSizeOutputID );
78 nOnes = 0;
79
80 for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
81 nOnes += Fxch_CountOnes( pOutputID[j] );
82
83 if ( nOnes == 0 )
84 nOnes = 1;
85
86 if (fAdd)
87 {
88 for ( z = 0; z < nOnes; z++ )
89 Fxch_DivAdd( pFxchMan, fUpdate, fSingleCube, fBase );
90 pFxchMan->nPairsS++;
91 }
92 else
93 {
94 for ( z = 0; z < nOnes; z++ )
95 Fxch_DivRemove( pFxchMan, fUpdate, fSingleCube, fBase );
96 pFxchMan->nPairsS--;
97 }
98 }
99
100 return Vec_IntSize( vCube ) * ( Vec_IntSize( vCube ) - 1 ) / 2;
101 }
102
Fxch_ManDivDoubleCube(Fxch_Man_t * pFxchMan,int iCube,int fAdd,int fUpdate)103 static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
104 int iCube,
105 int fAdd,
106 int fUpdate )
107 {
108 Vec_Int_t* vLitHashKeys = pFxchMan->vLitHashKeys,
109 * vCube = Vec_WecEntry( pFxchMan->vCubes, iCube );
110 int SubCubeID = 0,
111 iLit0,
112 Lit0;
113
114 Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1)
115 SubCubeID += Vec_IntEntry( vLitHashKeys, Lit0 );
116
117 Fxch_ManSCAddRemove( pFxchMan, SubCubeID,
118 iCube, 0, 0,
119 (char)fAdd, (char)fUpdate );
120
121 Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1)
122 {
123 /* 1 Lit remove */
124 SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit0 );
125
126 pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, SubCubeID,
127 iCube, iLit0, 0,
128 (char)fAdd, (char)fUpdate );
129
130 if ( Vec_IntSize( vCube ) >= 3 )
131 {
132 int Lit1,
133 iLit1;
134
135 Vec_IntForEachEntryStart( vCube, Lit1, iLit1, iLit0 + 1)
136 {
137 /* 2 Lit remove */
138 SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit1 );
139
140 pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, SubCubeID,
141 iCube, iLit0, iLit1,
142 (char)fAdd, (char)fUpdate );
143
144 SubCubeID += Vec_IntEntry( vLitHashKeys, Lit1 );
145 }
146 }
147
148 SubCubeID += Vec_IntEntry( vLitHashKeys, Lit0 );
149 }
150 }
151
Fxch_ManCompressCubes(Vec_Wec_t * vCubes,Vec_Int_t * vLit2Cube)152 static inline void Fxch_ManCompressCubes( Vec_Wec_t* vCubes,
153 Vec_Int_t* vLit2Cube )
154 {
155 int i,
156 k = 0,
157 CubeId;
158
159 Vec_IntForEachEntry( vLit2Cube, CubeId, i )
160 if ( Vec_IntSize(Vec_WecEntry(vCubes, CubeId)) > 0 )
161 Vec_IntWriteEntry( vLit2Cube, k++, CubeId );
162
163 Vec_IntShrink( vLit2Cube, k );
164 }
165
166 ////////////////////////////////////////////////////////////////////////
167 /// PUBLIC INTERFACE ///
168 ////////////////////////////////////////////////////////////////////////
Fxch_ManAlloc(Vec_Wec_t * vCubes)169 Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes )
170 {
171 Fxch_Man_t* pFxchMan = ABC_CALLOC( Fxch_Man_t, 1 );
172
173 pFxchMan->vCubes = vCubes;
174 pFxchMan->nCubesInit = Vec_WecSize( vCubes );
175
176 pFxchMan->pDivHash = Hsh_VecManStart( 1024 );
177 pFxchMan->vDivWeights = Vec_FltAlloc( 1024 );
178 pFxchMan->vDivCubePairs = Vec_WecAlloc( 1024 );
179
180 pFxchMan->vCubeFree = Vec_IntAlloc( 4 );
181 pFxchMan->vDiv = Vec_IntAlloc( 4 );
182
183 pFxchMan->vCubesS = Vec_IntAlloc( 128 );
184 pFxchMan->vPairs = Vec_IntAlloc( 128 );
185 pFxchMan->vCubesToUpdate = Vec_IntAlloc( 64 );
186 pFxchMan->vCubesToRemove = Vec_IntAlloc( 64 );
187 pFxchMan->vSCC = Vec_IntAlloc( 64 );
188
189 return pFxchMan;
190 }
191
Fxch_ManFree(Fxch_Man_t * pFxchMan)192 void Fxch_ManFree( Fxch_Man_t* pFxchMan )
193 {
194 Vec_WecFree( pFxchMan->vLits );
195 Vec_IntFree( pFxchMan->vLitCount );
196 Vec_IntFree( pFxchMan->vLitHashKeys );
197 Hsh_VecManStop( pFxchMan->pDivHash );
198 Vec_FltFree( pFxchMan->vDivWeights );
199 Vec_QueFree( pFxchMan->vDivPrio );
200 Vec_WecFree( pFxchMan->vDivCubePairs );
201 Vec_IntFree( pFxchMan->vLevels );
202
203 Vec_IntFree( pFxchMan->vCubeFree );
204 Vec_IntFree( pFxchMan->vDiv );
205
206 Vec_IntFree( pFxchMan->vCubesS );
207 Vec_IntFree( pFxchMan->vPairs );
208 Vec_IntFree( pFxchMan->vCubesToUpdate );
209 Vec_IntFree( pFxchMan->vCubesToRemove );
210 Vec_IntFree( pFxchMan->vSCC );
211
212 ABC_FREE( pFxchMan );
213 }
214
Fxch_ManMapLiteralsIntoCubes(Fxch_Man_t * pFxchMan,int nVars)215 void Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan,
216 int nVars )
217 {
218
219 Vec_Int_t* vCube;
220 int i, k,
221 Lit,
222 Count;
223
224 pFxchMan->nVars = 0;
225 pFxchMan->nLits = 0;
226 Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
227 {
228 assert( Vec_IntSize(vCube) > 0 );
229 pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Vec_IntEntry( vCube, 0 ) );
230 pFxchMan->nLits += Vec_IntSize(vCube) - 1;
231 Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
232 pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Abc_Lit2Var( Lit ) );
233 }
234
235 assert( pFxchMan->nVars < nVars );
236 pFxchMan->nVars = nVars;
237
238 /* Count the number of time each literal appears on the SOP */
239 pFxchMan->vLitCount = Vec_IntStart( 2 * pFxchMan->nVars );
240 Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
241 Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
242 Vec_IntAddToEntry( pFxchMan->vLitCount, Lit, 1 );
243
244 /* Allocate space to the array of arrays wich maps Literals into cubes which uses them */
245 pFxchMan->vLits = Vec_WecStart( 2 * pFxchMan->nVars );
246 Vec_IntForEachEntry( pFxchMan->vLitCount, Count, Lit )
247 Vec_IntGrow( Vec_WecEntry( pFxchMan->vLits, Lit ), Count );
248
249 /* Maps Literals into cubes which uses them */
250 Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
251 Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
252 Vec_WecPush( pFxchMan->vLits, Lit, i );
253 }
254
Fxch_ManGenerateLitHashKeys(Fxch_Man_t * pFxchMan)255 void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan )
256 {
257 int i;
258 /* Generates the random number which will be used for hashing cubes */
259 Gia_ManRandom( 1 );
260 pFxchMan->vLitHashKeys = Vec_IntAlloc( ( 2 * pFxchMan->nVars ) );
261 for ( i = 0; i < (2 * pFxchMan->nVars); i++ )
262 Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
263 }
264
Fxch_ManSCHashTablesInit(Fxch_Man_t * pFxchMan)265 void Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan )
266 {
267 Vec_Wec_t* vCubes = pFxchMan->vCubes;
268 Vec_Int_t* vCube;
269 int iCube,
270 nTotalHashed = 0;
271
272 Vec_WecForEachLevel( vCubes, vCube, iCube )
273 {
274 int nLits = Vec_IntSize( vCube ) - 1,
275 nSubCubes = nLits <= 2? nLits + 1: ( nLits * nLits + nLits ) / 2;
276
277 nTotalHashed += nSubCubes + 1;
278 }
279
280 pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, nTotalHashed );
281 }
282
Fxch_ManSCHashTablesFree(Fxch_Man_t * pFxchMan)283 void Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan )
284 {
285 Fxch_SCHashTableDelete( pFxchMan->pSCHashTable );
286 }
287
Fxch_ManDivCreate(Fxch_Man_t * pFxchMan)288 void Fxch_ManDivCreate( Fxch_Man_t* pFxchMan )
289 {
290 Vec_Int_t* vCube;
291 float Weight;
292 int fAdd = 1,
293 fUpdate = 0,
294 iCube;
295
296 Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube )
297 {
298 Fxch_ManDivSingleCube( pFxchMan, iCube, fAdd, fUpdate );
299 Fxch_ManDivDoubleCube( pFxchMan, iCube, fAdd, fUpdate );
300 }
301
302 pFxchMan->vDivPrio = Vec_QueAlloc( Vec_FltSize( pFxchMan->vDivWeights ) );
303 Vec_QueSetPriority( pFxchMan->vDivPrio, Vec_FltArrayP( pFxchMan->vDivWeights ) );
304 Vec_FltForEachEntry( pFxchMan->vDivWeights, Weight, iCube )
305 {
306 if ( Weight > 0.0 )
307 Vec_QuePush( pFxchMan->vDivPrio, iCube );
308 }
309 }
310
311 /* Level Computation */
Fxch_ManComputeLevelDiv(Fxch_Man_t * pFxchMan,Vec_Int_t * vCubeFree)312 int Fxch_ManComputeLevelDiv( Fxch_Man_t* pFxchMan,
313 Vec_Int_t* vCubeFree )
314 {
315 int i,
316 Lit,
317 Level = 0;
318
319 Vec_IntForEachEntry( vCubeFree, Lit, i )
320 Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Abc_Lit2Var( Lit ) ) ) );
321
322 return Abc_MinInt( Level, 800 );
323 }
324
Fxch_ManComputeLevelCube(Fxch_Man_t * pFxchMan,Vec_Int_t * vCube)325 int Fxch_ManComputeLevelCube( Fxch_Man_t* pFxchMan,
326 Vec_Int_t * vCube )
327 {
328 int k,
329 Lit,
330 Level = 0;
331
332 Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
333 Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Lit ) ) );
334
335 return Level;
336 }
337
Fxch_ManComputeLevel(Fxch_Man_t * pFxchMan)338 void Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan )
339 {
340 Vec_Int_t* vCube;
341 int i,
342 iVar,
343 iFirst = 0;
344
345 iVar = Vec_IntEntry( Vec_WecEntry( pFxchMan->vCubes, 0 ), 0 );
346 pFxchMan->vLevels = Vec_IntStart( pFxchMan->nVars );
347
348 Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
349 {
350 if ( iVar != Vec_IntEntry( vCube, 0 ) )
351 {
352 Vec_IntAddToEntry( pFxchMan->vLevels, iVar, i - iFirst );
353 iVar = Vec_IntEntry( vCube, 0 );
354 iFirst = i;
355 }
356 Vec_IntUpdateEntry( pFxchMan->vLevels, iVar, Fxch_ManComputeLevelCube( pFxchMan, vCube ) );
357 }
358 }
359
360 /* Extract divisor from single-cubes */
Fxch_ManExtractDivFromCube(Fxch_Man_t * pFxchMan,const int Lit0,const int Lit1,const int iVarNew)361 static inline void Fxch_ManExtractDivFromCube( Fxch_Man_t* pFxchMan,
362 const int Lit0,
363 const int Lit1,
364 const int iVarNew )
365 {
366 int i, iCube0;
367 Vec_Int_t* vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 );
368
369 Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
370 {
371 int RetValue;
372 Vec_Int_t* vCube0;
373
374 vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 );
375 RetValue = Vec_IntRemove1( vCube0, Abc_LitNot( Lit0 ) );
376 RetValue += Vec_IntRemove1( vCube0, Abc_LitNot( Lit1 ) );
377 assert( RetValue == 2 );
378
379 Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) );
380 Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
381 Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 );
382
383 pFxchMan->nLits--;
384 }
385 }
386
387 /* Extract divisor from cube pairs */
Fxch_ManExtractDivFromCubePairs(Fxch_Man_t * pFxchMan,const int iVarNew)388 static inline void Fxch_ManExtractDivFromCubePairs( Fxch_Man_t* pFxchMan,
389 const int iVarNew )
390 {
391 /* For each pair (Ci, Cj) */
392 int iCube0, iCube1, i;
393
394
395 Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
396 {
397 int j, Lit,
398 RetValue,
399 fCompl = 0;
400 int * pOutputID0, * pOutputID1;
401
402 Vec_Int_t* vCube = NULL,
403 * vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ),
404 * vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 ),
405 * vCube0Copy = Vec_IntDup( vCube0 ),
406 * vCube1Copy = Vec_IntDup( vCube1 );
407
408 RetValue = Fxch_DivRemoveLits( vCube0Copy, vCube1Copy, pFxchMan->vDiv, &fCompl );
409
410 assert( RetValue == Vec_IntSize( pFxchMan->vDiv ) );
411
412 pFxchMan->nLits -= Vec_IntSize( pFxchMan->vDiv ) + Vec_IntSize( vCube1 ) - 2;
413
414 /* Identify type of Extraction */
415 pOutputID0 = Vec_IntEntryP( pFxchMan->vOutputID, iCube0 * pFxchMan->nSizeOutputID );
416 pOutputID1 = Vec_IntEntryP( pFxchMan->vOutputID, iCube1 * pFxchMan->nSizeOutputID );
417 RetValue = 1;
418 for ( j = 0; j < pFxchMan->nSizeOutputID && RetValue; j++ )
419 RetValue = ( pOutputID0[j] == pOutputID1[j] );
420
421 /* Exact Extractraion */
422 if ( RetValue )
423 {
424 Vec_IntClear( vCube0 );
425 Vec_IntAppend( vCube0, vCube0Copy );
426 vCube = vCube0;
427
428 Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 );
429 Vec_IntClear( vCube1 );
430
431 /* Update Lit -> Cube mapping */
432 Vec_IntForEachEntry( pFxchMan->vDiv, Lit, j )
433 {
434 Vec_IntRemove( Vec_WecEntry( pFxchMan->vLits, Abc_Lit2Var( Lit ) ),
435 Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
436 Vec_IntRemove( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Abc_Lit2Var( Lit ) ) ),
437 Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
438 }
439
440 }
441 /* Unexact Extraction */
442 else
443 {
444 for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
445 pFxchMan->pTempOutputID[j] = ( pOutputID0[j] & pOutputID1[j] );
446
447 /* Create new cube */
448 vCube = Vec_WecPushLevel( pFxchMan->vCubes );
449 Vec_IntAppend( vCube, vCube0Copy );
450 Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID );
451 Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube ) );
452
453 /* Update Lit -> Cube mapping */
454 Vec_IntForEachEntryStart( vCube, Lit, j, 1 )
455 Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube ) );
456
457 /*********************************************************/
458 RetValue = 0;
459 for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
460 {
461 pFxchMan->pTempOutputID[j] = pOutputID0[j];
462 RetValue |= ( pOutputID0[j] & ~( pOutputID1[j] ) );
463 pOutputID0[j] &= ~( pOutputID1[j] );
464 }
465
466 if ( RetValue != 0 )
467 Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 );
468 else
469 Vec_IntClear( vCube0 );
470
471 /*********************************************************/
472 RetValue = 0;
473 for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
474 {
475 RetValue |= ( pOutputID1[j] & ~( pFxchMan->pTempOutputID[j] ) );
476 pOutputID1[j] &= ~( pFxchMan->pTempOutputID[j] );
477 }
478
479 if ( RetValue != 0 )
480 Vec_IntPush( pFxchMan->vCubesToUpdate, iCube1 );
481 else
482 Vec_IntClear( vCube1 );
483
484 }
485 Vec_IntFree( vCube0Copy );
486 Vec_IntFree( vCube1Copy );
487
488 if ( iVarNew )
489 {
490 Vec_Int_t* vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ),
491 * vLitN = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 1 );
492
493 assert( vCube );
494 if ( Vec_IntSize( pFxchMan->vDiv ) == 2 || fCompl )
495 {
496 Vec_IntPush( vCube, Abc_Var2Lit( iVarNew, 1 ) );
497 Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube ) );
498 Vec_IntSort( vLitN, 0 );
499 }
500 else
501 {
502 Vec_IntPush( vCube, Abc_Var2Lit( iVarNew, 0 ) );
503 Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube ) );
504 Vec_IntSort( vLitP, 0 );
505 }
506 }
507 }
508
509 return;
510 }
511
Fxch_ManCreateCube(Fxch_Man_t * pFxchMan,int Lit0,int Lit1)512 static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan,
513 int Lit0,
514 int Lit1 )
515 {
516 int Level,
517 iVarNew,
518 j;
519 Vec_Int_t* vCube0,
520 * vCube1;
521
522 /* Create a new variable */
523 iVarNew = pFxchMan->nVars;
524 pFxchMan->nVars++;
525
526 /* Clear temporary outputID vector */
527 for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
528 pFxchMan->pTempOutputID[j] = 0;
529
530 /* Create new Lit hash keys */
531 Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
532 Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
533
534 /* Create new Cube */
535 vCube0 = Vec_WecPushLevel( pFxchMan->vCubes );
536 Vec_IntPush( vCube0, iVarNew );
537 Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID );
538
539 if ( Vec_IntSize( pFxchMan->vDiv ) == 2 )
540 {
541 if ( Lit0 > Lit1 )
542 ABC_SWAP(int, Lit0, Lit1);
543
544 Vec_IntPush( vCube0, Abc_LitNot( Lit0 ) );
545 Vec_IntPush( vCube0, Abc_LitNot( Lit1 ) );
546 Level = 1 + Fxch_ManComputeLevelCube( pFxchMan, vCube0 );
547 }
548 else
549 {
550 int i;
551 int Lit;
552
553 vCube1 = Vec_WecPushLevel( pFxchMan->vCubes );
554 Vec_IntPush( vCube1, iVarNew );
555 Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID );
556
557 vCube0 = Fxch_ManGetCube( pFxchMan, Vec_WecSize( pFxchMan->vCubes ) - 2 );
558 Fxch_DivSepareteCubes( pFxchMan->vDiv, vCube0, vCube1 );
559 Level = 2 + Abc_MaxInt( Fxch_ManComputeLevelCube( pFxchMan, vCube0 ),
560 Fxch_ManComputeLevelCube( pFxchMan, vCube1 ) );
561
562 Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
563 Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) );
564
565 /* Update Lit -> Cube mapping */
566 Vec_IntForEachEntryStart( vCube0, Lit, i, 1 )
567 Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
568
569 Vec_IntForEachEntryStart( vCube1, Lit, i, 1 )
570 Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) );
571 }
572 assert( Vec_IntSize( pFxchMan->vLevels ) == iVarNew );
573 Vec_IntPush( pFxchMan->vLevels, Level );
574
575 pFxchMan->nLits += Vec_IntSize( pFxchMan->vDiv );
576
577 /* Create new literals */
578 Vec_WecPushLevel( pFxchMan->vLits );
579 Vec_WecPushLevel( pFxchMan->vLits );
580
581 return iVarNew;
582 }
583
Fxch_ManUpdate(Fxch_Man_t * pFxchMan,int iDiv)584 void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
585 int iDiv )
586 {
587 int i, iCube0, iCube1,
588 Lit0 = -1,
589 Lit1 = -1,
590 iVarNew;
591
592 Vec_Int_t* vCube0,
593 * vCube1,
594 * vDivCubePairs;
595
596 /* Get the selected candidate (divisor) */
597 Vec_IntClear( pFxchMan->vDiv );
598 Vec_IntAppend( pFxchMan->vDiv, Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv ) );
599
600 /* Find cubes associated with the divisor */
601 Vec_IntClear( pFxchMan->vCubesS );
602 if ( Vec_IntSize( pFxchMan->vDiv ) == 2 )
603 {
604 Lit0 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 0 ) );
605 Lit1 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 1 ) );
606 assert( Lit0 >= 0 && Lit1 >= 0 );
607
608 Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ) );
609 Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ) );
610 Vec_IntTwoRemoveCommon( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ),
611 Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ),
612 pFxchMan->vCubesS );
613 }
614
615 /* Find pairs associated with the divisor */
616 Vec_IntClear( pFxchMan->vPairs );
617 vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv );
618 Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs );
619 Vec_IntErase( vDivCubePairs );
620
621 Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
622 {
623 assert( Fxch_ManGetLit( pFxchMan, iCube0, 0) == Fxch_ManGetLit( pFxchMan, iCube1, 0) );
624 if (iCube0 > iCube1)
625 {
626 Vec_IntSetEntry( pFxchMan->vPairs, i, iCube1);
627 Vec_IntSetEntry( pFxchMan->vPairs, i+1, iCube0);
628 }
629 }
630
631 Vec_IntUniqifyPairs( pFxchMan->vPairs );
632 assert( Vec_IntSize( pFxchMan->vPairs ) % 2 == 0 );
633
634 /* subtract cost of single-cube divisors */
635 Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
636 {
637 Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1);
638
639 if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 )
640 Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 );
641 }
642
643 Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
644 {
645 Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1);
646
647 if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 )
648 Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 );
649 }
650
651 Vec_IntClear( pFxchMan->vCubesToUpdate );
652 if ( Fxch_DivIsNotConstant1( pFxchMan->vDiv ) )
653 {
654 iVarNew = Fxch_ManCreateCube( pFxchMan, Lit0, Lit1 );
655 Fxch_ManExtractDivFromCube( pFxchMan, Lit0, Lit1, iVarNew );
656 Fxch_ManExtractDivFromCubePairs( pFxchMan, iVarNew );
657 }
658 else
659 Fxch_ManExtractDivFromCubePairs( pFxchMan, 0 );
660
661 assert( Vec_IntSize( pFxchMan->vCubesToUpdate ) );
662
663 /* Add cost */
664 Vec_IntForEachEntry( pFxchMan->vCubesToUpdate, iCube0, i )
665 {
666 Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 );
667
668 if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 )
669 Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 );
670 }
671
672 /* Deal with SCC */
673 if ( Vec_IntSize( pFxchMan->vSCC ) )
674 {
675 Vec_IntUniqifyPairs( pFxchMan->vSCC );
676 assert( Vec_IntSize( pFxchMan->vSCC ) % 2 == 0 );
677
678 Vec_IntForEachEntryDouble( pFxchMan->vSCC, iCube0, iCube1, i )
679 {
680 int j, RetValue = 1;
681 int* pOutputID0 = Vec_IntEntryP( pFxchMan->vOutputID, iCube0 * pFxchMan->nSizeOutputID );
682 int* pOutputID1 = Vec_IntEntryP( pFxchMan->vOutputID, iCube1 * pFxchMan->nSizeOutputID );
683 vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 );
684 vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 );
685
686 if ( !Vec_WecIntHasMark( vCube0 ) )
687 {
688 Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1 );
689 Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 );
690 Vec_WecIntSetMark( vCube0 );
691 }
692
693 if ( !Vec_WecIntHasMark( vCube1 ) )
694 {
695 Fxch_ManDivSingleCube( pFxchMan, iCube1, 0, 1 );
696 Fxch_ManDivDoubleCube( pFxchMan, iCube1, 0, 1 );
697 Vec_WecIntSetMark( vCube1 );
698 }
699
700 if ( Vec_IntSize( vCube0 ) == Vec_IntSize( vCube1 ) )
701 {
702 for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
703 {
704 pOutputID1[j] |= pOutputID0[j];
705 pOutputID0[j] = 0;
706 }
707 Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) );
708 Vec_WecIntXorMark( vCube0 );
709 continue;
710 }
711
712 for ( j = 0; j < pFxchMan->nSizeOutputID && RetValue; j++ )
713 RetValue = ( pOutputID0[j] == pOutputID1[j] );
714
715 if ( RetValue )
716 {
717 Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) );
718 Vec_WecIntXorMark( vCube0 );
719 }
720 else
721 {
722 RetValue = 0;
723 for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
724 {
725 RetValue |= ( pOutputID0[j] & ~( pOutputID1[j] ) );
726 pOutputID0[j] &= ~( pOutputID1[j] );
727 }
728
729 if ( RetValue == 0 )
730 {
731 Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) );
732 Vec_WecIntXorMark( vCube0 );
733 }
734 }
735 }
736
737 Vec_IntForEachEntryDouble( pFxchMan->vSCC, iCube0, iCube1, i )
738 {
739 vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 );
740 vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 );
741
742 if ( Vec_WecIntHasMark( vCube0 ) )
743 {
744 Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 );
745 Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 );
746 Vec_WecIntXorMark( vCube0 );
747 }
748
749 if ( Vec_WecIntHasMark( vCube1 ) )
750 {
751 Fxch_ManDivSingleCube( pFxchMan, iCube1, 1, 1 );
752 Fxch_ManDivDoubleCube( pFxchMan, iCube1, 1, 1 );
753 Vec_WecIntXorMark( vCube1 );
754 }
755 }
756
757 Vec_IntClear( pFxchMan->vSCC );
758 }
759
760 pFxchMan->nExtDivs++;
761 }
762
763 /* Print */
Fxch_ManPrintDivs(Fxch_Man_t * pFxchMan)764 void Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan )
765 {
766 int iDiv;
767
768 for ( iDiv = 0; iDiv < Vec_FltSize( pFxchMan->vDivWeights ); iDiv++ )
769 Fxch_DivPrint( pFxchMan, iDiv );
770 }
771
Fxch_ManPrintStats(Fxch_Man_t * pFxchMan)772 void Fxch_ManPrintStats( Fxch_Man_t* pFxchMan )
773 {
774 printf( "Cubes =%8d ", Vec_WecSizeUsed( pFxchMan->vCubes ) );
775 printf( "Lits =%8d ", Vec_WecSizeUsed( pFxchMan->vLits ) );
776 printf( "Divs =%8d ", Hsh_VecSize( pFxchMan->pDivHash ) );
777 printf( "Divs+ =%8d ", Vec_QueSize( pFxchMan->vDivPrio ) );
778 printf( "Extr =%7d \n", pFxchMan->nExtDivs );
779 }
780
781 ////////////////////////////////////////////////////////////////////////
782 /// END OF FILE ///
783 ////////////////////////////////////////////////////////////////////////
784
785 ABC_NAMESPACE_IMPL_END
786