1 /**CFile****************************************************************************************************************
2
3 FileName [ FxchDiv.c ]
4
5 PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
6
7 Synopsis [ Divisor handling functions ]
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
19 #include "Fxch.h"
20
21 ABC_NAMESPACE_IMPL_START
22
23 ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
24 // FUNCTION DEFINITIONS
25 ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
Fxch_DivNormalize(Vec_Int_t * vCubeFree)26 static inline int Fxch_DivNormalize( Vec_Int_t* vCubeFree )
27 {
28 int * L = Vec_IntArray(vCubeFree);
29 int RetValue = 0, LitA0 = -1, LitB0 = -1, LitA1 = -1, LitB1 = -1;
30 assert( Vec_IntSize(vCubeFree) == 4 );
31 if ( Abc_LitIsCompl(L[0]) != Abc_LitIsCompl(L[1]) && (L[0] >> 2) == (L[1] >> 2) ) // diff cubes, same vars
32 {
33 if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[3]) )
34 return -1;
35 LitA0 = Abc_Lit2Var(L[0]), LitB0 = Abc_Lit2Var(L[1]);
36 if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) )
37 {
38 assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) );
39 LitA1 = Abc_Lit2Var(L[2]), LitB1 = Abc_Lit2Var(L[3]);
40 }
41 else
42 {
43 assert( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) );
44 assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[2]) );
45 LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[2]);
46 }
47 }
48 else if ( Abc_LitIsCompl(L[1]) != Abc_LitIsCompl(L[2]) && (L[1] >> 2) == (L[2] >> 2) )
49 {
50 if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) )
51 return -1;
52 LitA0 = Abc_Lit2Var(L[1]), LitB0 = Abc_Lit2Var(L[2]);
53 if ( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[0]) )
54 LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[3]);
55 else
56 LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[0]);
57 }
58 else if ( Abc_LitIsCompl(L[2]) != Abc_LitIsCompl(L[3]) && (L[2] >> 2) == (L[3] >> 2) )
59 {
60 if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[1]) )
61 return -1;
62 LitA0 = Abc_Lit2Var(L[2]), LitB0 = Abc_Lit2Var(L[3]);
63 if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[0]) )
64 LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[1]);
65 else
66 LitA1 = Abc_Lit2Var(L[1]), LitB1 = Abc_Lit2Var(L[0]);
67 }
68 else
69 return -1;
70 assert( LitA0 == Abc_LitNot(LitB0) );
71 if ( Abc_LitIsCompl(LitA0) )
72 {
73 ABC_SWAP( int, LitA0, LitB0 );
74 ABC_SWAP( int, LitA1, LitB1 );
75 }
76 assert( !Abc_LitIsCompl(LitA0) );
77 if ( Abc_LitIsCompl(LitA1) )
78 {
79 LitA1 = Abc_LitNot(LitA1);
80 LitB1 = Abc_LitNot(LitB1);
81 RetValue = 1;
82 }
83 assert( !Abc_LitIsCompl(LitA1) );
84 // arrange literals in such as a way that
85 // - the first two literals are control literals from different cubes
86 // - the third literal is non-complented data input
87 // - the forth literal is possibly complemented data input
88 L[0] = Abc_Var2Lit( LitA0, 0 );
89 L[1] = Abc_Var2Lit( LitB0, 1 );
90 L[2] = Abc_Var2Lit( LitA1, 0 );
91 L[3] = Abc_Var2Lit( LitB1, 1 );
92 return RetValue;
93 }
94
95 /**Function*************************************************************
96
97 Synopsis [ Creates a Divisor. ]
98
99 Description [ This functions receive as input two sub-cubes and creates
100 a divisor using their information. The divisor is stored
101 in vCubeFree vector of the pFxchMan structure.
102
103 It returns the base value, which is the number of elements
104 that the cubes pair used to generate the devisor have in
105 common. ]
106
107 SideEffects []
108
109 SeeAlso []
110
111 ***********************************************************************/
Fxch_DivCreate(Fxch_Man_t * pFxchMan,Fxch_SubCube_t * pSubCube0,Fxch_SubCube_t * pSubCube1)112 int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
113 Fxch_SubCube_t* pSubCube0,
114 Fxch_SubCube_t* pSubCube1 )
115 {
116 int Base = 0;
117
118 int SC0_Lit0,
119 SC0_Lit1,
120 SC1_Lit0,
121 SC1_Lit1;
122
123 int Cube0Size,
124 Cube1Size;
125
126 Vec_IntClear( pFxchMan->vCubeFree );
127
128 SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 );
129 SC0_Lit1 = 0;
130 SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 );
131 SC1_Lit1 = 0;
132
133 if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 )
134 {
135 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
136 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
137 }
138 else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 )
139 {
140 int RetValue;
141
142 SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
143 SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
144
145 if ( SC0_Lit0 < SC1_Lit0 )
146 {
147 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) );
148 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) );
149 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) );
150 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) );
151 }
152 else
153 {
154 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 0 ) );
155 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 1 ) );
156 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 0 ) );
157 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 1 ) );
158 }
159
160 RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
161 if ( RetValue == -1 )
162 return -1;
163 }
164 else
165 {
166 if ( pSubCube0->iLit1 > 0 )
167 {
168 SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
169
170 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
171 if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) )
172 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 );
173 else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) )
174 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
175 }
176 else
177 {
178 SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
179
180 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
181 if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) )
182 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 );
183 else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) )
184 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
185 }
186 }
187
188 if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 )
189 return -1;
190
191 if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 )
192 {
193 Vec_IntSort( pFxchMan->vCubeFree, 0 );
194
195 Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) );
196 Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) );
197 }
198
199 Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) );
200 Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) );
201 if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 )
202 {
203 Base = Abc_MinInt( Cube0Size, Cube1Size )
204 -( Vec_IntSize( pFxchMan->vCubeFree ) / 2) - 1; /* 1 or 2 Lits, 1 SOP NodeID */
205 }
206 else
207 return -1;
208
209 return Base;
210 }
211
212 /**Function*************************************************************
213
214 Synopsis [ Add a divisor to the divisors hash table. ]
215
216 Description [ This functions will try to add the divisor store in
217 vCubeFree to the divisor hash table. If the divisor
218 is already present in the hash table it will just
219 increment its weight, otherwise it will add the divisor
220 and asign an initial weight. ]
221
222 SideEffects [ If the fUpdate option is set, the function will also
223 update the divisor priority queue. ]
224
225 SeeAlso []
226
227 ***********************************************************************/
Fxch_DivAdd(Fxch_Man_t * pFxchMan,int fUpdate,int fSingleCube,int fBase)228 int Fxch_DivAdd( Fxch_Man_t* pFxchMan,
229 int fUpdate,
230 int fSingleCube,
231 int fBase )
232 {
233 int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
234
235 /* Verify if the divisor already exist */
236 if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) )
237 {
238 Vec_WecPushLevel( pFxchMan->vDivCubePairs );
239
240 /* Assign initial weight */
241 if ( fSingleCube )
242 {
243 Vec_FltPush( pFxchMan->vDivWeights,
244 -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
245 -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
246 }
247 else
248 {
249 Vec_FltPush( pFxchMan->vDivWeights,
250 -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
251 -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
252 }
253
254 }
255
256 /* Increment weight */
257 if ( fSingleCube )
258 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 );
259 else
260 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 );
261
262 assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
263
264 if ( fUpdate )
265 if ( pFxchMan->vDivPrio )
266 {
267 if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
268 Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
269 else
270 Vec_QuePush( pFxchMan->vDivPrio, iDiv );
271 }
272
273 return iDiv;
274 }
275
276 /**Function*************************************************************
277
278 Synopsis [ Removes a divisor to the divisors hash table. ]
279
280 Description [ This function don't effectively removes a divisor from
281 the hash table (the hash table implementation don't
282 support such operation). It only assures its existence
283 and decrement its weight. ]
284
285 SideEffects [ If the fUpdate option is set, the function will also
286 update the divisor priority queue. ]
287
288 SeeAlso []
289
290 ***********************************************************************/
Fxch_DivRemove(Fxch_Man_t * pFxchMan,int fUpdate,int fSingleCube,int fBase)291 int Fxch_DivRemove( Fxch_Man_t* pFxchMan,
292 int fUpdate,
293 int fSingleCube,
294 int fBase )
295 {
296 int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
297
298 assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
299
300 /* Decrement weight */
301 if ( fSingleCube )
302 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 );
303 else
304 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) );
305
306 if ( fUpdate )
307 if ( pFxchMan->vDivPrio )
308 {
309 if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
310 Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
311 }
312
313 return iDiv;
314 }
315
316 /**Function*************************************************************
317
318 Synopsis [ Separete the cubes in present in a divisor ]
319
320 Description [ In this implementation *all* stored divsors are composed
321 of two cubes.
322
323 In order to save space and to be able to use the Vec_Int_t
324 hash table both cubes are stored in the same vector - using
325 a little hack to differentiate which literal belongs to each
326 cube.
327
328 This function separetes the two cubes in their own vectors
329 so that they can be added to the cover.
330
331 *Note* that this also applies to single cube
332 divisors beacuse of the DeMorgan Law: ab = ( a! + !b )! ]
333
334 SideEffects []
335
336 SeeAlso []
337
338 ***********************************************************************/
Fxch_DivSepareteCubes(Vec_Int_t * vDiv,Vec_Int_t * vCube0,Vec_Int_t * vCube1)339 void Fxch_DivSepareteCubes( Vec_Int_t* vDiv,
340 Vec_Int_t* vCube0,
341 Vec_Int_t* vCube1 )
342 {
343 int* pArray;
344 int i,
345 Lit;
346
347 Vec_IntForEachEntry( vDiv, Lit, i )
348 if ( Abc_LitIsCompl(Lit) )
349 Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) );
350 else
351 Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) );
352
353 if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) )
354 {
355 assert( Vec_IntSize( vCube1 ) == 3 );
356
357 pArray = Vec_IntArray( vCube0 );
358 if ( pArray[1] > pArray[2] )
359 ABC_SWAP( int, pArray[1], pArray[2] );
360
361 pArray = Vec_IntArray( vCube1 );
362 if ( pArray[1] > pArray[2] )
363 ABC_SWAP( int, pArray[1], pArray[2] );
364 }
365 }
366
367 /**Function*************************************************************
368
369 Synopsis [ Removes the literals present in the divisor from their
370 original cubes. ]
371
372 Description [ This function returns the numeber of removed literals
373 which should be equal to the size of the divisor. ]
374
375 SideEffects []
376
377 SeeAlso []
378
379 ***********************************************************************/
Fxch_DivRemoveLits(Vec_Int_t * vCube0,Vec_Int_t * vCube1,Vec_Int_t * vDiv,int * fCompl)380 int Fxch_DivRemoveLits( Vec_Int_t* vCube0,
381 Vec_Int_t* vCube1,
382 Vec_Int_t* vDiv,
383 int *fCompl )
384 {
385 int i,
386 Lit,
387 CountP = 0,
388 CountN = 0,
389 Count = 0,
390 ret = 0;
391
392 Vec_IntForEachEntry( vDiv, Lit, i )
393 if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) )
394 CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
395 else
396 CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
397
398 Vec_IntForEachEntry( vDiv, Lit, i )
399 Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) );
400
401 if ( Vec_IntSize( vDiv ) == 2 )
402 Vec_IntForEachEntry( vDiv, Lit, i )
403 {
404 Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
405 Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
406 }
407
408 ret = Count + CountP + CountN;
409
410 if ( Vec_IntSize( vDiv ) == 4 )
411 {
412 int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
413 Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ),
414 Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ),
415 Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) );
416
417 if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 )
418 *fCompl = 1;
419
420 if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 )
421 {
422 *fCompl = 1;
423
424 Vec_IntForEachEntry( vDiv, Lit, i )
425 ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
426
427 Vec_IntForEachEntry( vDiv, Lit, i )
428 ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
429 }
430 }
431
432 return ret;
433 }
434
435 /**Function*************************************************************
436
437 Synopsis [ Print the divisor identified by iDiv. ]
438
439 Description []
440
441 SideEffects []
442
443 SeeAlso []
444
445 ***********************************************************************/
Fxch_DivPrint(Fxch_Man_t * pFxchMan,int iDiv)446 void Fxch_DivPrint( Fxch_Man_t* pFxchMan,
447 int iDiv )
448 {
449 Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv );
450 int i,
451 Lit;
452
453 printf( "Div %7d : ", iDiv );
454 printf( "Weight %12.5f ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) );
455
456 Vec_IntForEachEntry( vDiv, Lit, i )
457 if ( !Abc_LitIsCompl( Lit ) )
458 printf( "%d(1)", Abc_Lit2Var( Lit ) );
459
460 printf( " + " );
461
462 Vec_IntForEachEntry( vDiv, Lit, i )
463 if ( Abc_LitIsCompl( Lit ) )
464 printf( "%d(2)", Abc_Lit2Var( Lit ) );
465
466 printf( " Lits =%7d ", pFxchMan->nLits );
467 printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) );
468 }
469
Fxch_DivIsNotConstant1(Vec_Int_t * vDiv)470 int Fxch_DivIsNotConstant1( Vec_Int_t* vDiv )
471 {
472 int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
473 Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) );
474
475 if ( ( Vec_IntSize( vDiv ) == 2 ) && ( Lit0 == Abc_LitNot( Lit1 ) ) )
476 return 0;
477
478 return 1;
479 }
480
481 ////////////////////////////////////////////////////////////////////////
482 /// END OF FILE ///
483 ////////////////////////////////////////////////////////////////////////
484
485 ABC_NAMESPACE_IMPL_END
486