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