1 /**CFile****************************************************************
2
3 FileName [covMinSop.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Mapping into network of SOPs/ESOPs.]
8
9 Synopsis [SOP manipulation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: covMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "covInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 static void Min_SopRewrite( Min_Man_t * p );
31
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 /**Function*************************************************************
37
38 Synopsis []
39
40 Description []
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
Min_SopMinimize(Min_Man_t * p)47 void Min_SopMinimize( Min_Man_t * p )
48 {
49 int nCubesInit, nCubesOld, nIter;
50 if ( p->nCubes < 3 )
51 return;
52 nIter = 0;
53 nCubesInit = p->nCubes;
54 do {
55 nCubesOld = p->nCubes;
56 Min_SopRewrite( p );
57 nIter++;
58 // printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
59 }
60 while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
61 // printf( "\n" );
62
63 }
64
65 /**Function*************************************************************
66
67 Synopsis []
68
69 Description []
70
71 SideEffects []
72
73 SeeAlso []
74
75 ***********************************************************************/
Min_SopRewrite(Min_Man_t * p)76 void Min_SopRewrite( Min_Man_t * p )
77 {
78 Min_Cube_t * pCube, ** ppPrev;
79 Min_Cube_t * pThis, ** ppPrevT;
80 Min_Cube_t * pTemp;
81 int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld;
82 int nPairs = 0;
83 /*
84 {
85 Min_Cube_t * pCover;
86 pCover = Min_CoverCollect( p, p->nVars );
87 printf( "\n\n" );
88 Min_CoverWrite( stdout, pCover );
89 Min_CoverExpand( p, pCover );
90 }
91 */
92
93 // insert the bubble before the first cube
94 p->pBubble->pNext = p->ppStore[0];
95 p->ppStore[0] = p->pBubble;
96 p->pBubble->nLits = 0;
97
98 // go through the cubes
99 while ( 1 )
100 {
101 // get the index of the bubble
102 Index = p->pBubble->nLits;
103
104 // find the bubble
105 Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
106 if ( pCube == p->pBubble )
107 break;
108 assert( pCube == p->pBubble );
109
110 // remove the bubble, get the next cube after the bubble
111 *ppPrev = p->pBubble->pNext;
112 pCube = p->pBubble->pNext;
113 if ( pCube == NULL )
114 for ( Index++; Index <= p->nVars; Index++ )
115 if ( p->ppStore[Index] )
116 {
117 ppPrev = &(p->ppStore[Index]);
118 pCube = p->ppStore[Index];
119 break;
120 }
121 // stop if there is no more cubes
122 if ( pCube == NULL )
123 break;
124
125 // find the first dist2 cube
126 Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
127 if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
128 break;
129 if ( pThis == NULL && Index < p->nVars )
130 Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
131 if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
132 break;
133 // continue if there is no dist2 cube
134 if ( pThis == NULL )
135 {
136 // insert the bubble after the cube
137 p->pBubble->pNext = pCube->pNext;
138 pCube->pNext = p->pBubble;
139 p->pBubble->nLits = pCube->nLits;
140 continue;
141 }
142 nPairs++;
143 /*
144 printf( "\n" );
145 Min_CubeWrite( stdout, pCube );
146 Min_CubeWrite( stdout, pThis );
147 */
148 // remove the cubes, insert the bubble instead of pCube
149 *ppPrevT = pThis->pNext;
150 *ppPrev = p->pBubble;
151 p->pBubble->pNext = pCube->pNext;
152 p->pBubble->nLits = pCube->nLits;
153 p->nCubes -= 2;
154
155 assert( pCube != p->pBubble && pThis != p->pBubble );
156
157
158 // save the dist2 parameters
159 v00 = Min_CubeGetVar( pCube, Var0 );
160 v01 = Min_CubeGetVar( pCube, Var1 );
161 v10 = Min_CubeGetVar( pThis, Var0 );
162 v11 = Min_CubeGetVar( pThis, Var1 );
163 assert( v00 != v10 && v01 != v11 );
164 assert( v00 != 3 || v01 != 3 );
165 assert( v10 != 3 || v11 != 3 );
166
167 //printf( "\n" );
168 //Min_CubeWrite( stdout, pCube );
169 //Min_CubeWrite( stdout, pThis );
170
171 //printf( "\n" );
172 //Min_CubeWrite( stdout, pCube );
173 //Min_CubeWrite( stdout, pThis );
174
175 // consider the case when both cubes have non-empty literals
176 if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
177 {
178 assert( v00 == (v10 ^ 3) );
179 assert( v01 == (v11 ^ 3) );
180 // create the temporary cube equal to the first corner
181 Min_CubeXorVar( pCube, Var0, 3 );
182 // check if this cube is contained
183 fCont0 = Min_CoverContainsCube( p, pCube );
184 // create the temporary cube equal to the first corner
185 Min_CubeXorVar( pCube, Var0, 3 );
186 Min_CubeXorVar( pCube, Var1, 3 );
187 //printf( "\n" );
188 //Min_CubeWrite( stdout, pCube );
189 //Min_CubeWrite( stdout, pThis );
190 // check if this cube is contained
191 fCont1 = Min_CoverContainsCube( p, pCube );
192 // undo the change
193 Min_CubeXorVar( pCube, Var1, 3 );
194
195 // check if the cubes can be overwritten
196 if ( fCont0 && fCont1 )
197 {
198 // one of the cubes can be recycled, the other expanded and added
199 Min_CubeRecycle( p, pThis );
200 // remove the literals
201 Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
202 Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
203 pCube->nLits -= 2;
204 Min_SopAddCube( p, pCube );
205 }
206 else if ( fCont0 )
207 {
208 // expand both cubes and add them
209 Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
210 pCube->nLits--;
211 Min_SopAddCube( p, pCube );
212 Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
213 pThis->nLits--;
214 Min_SopAddCube( p, pThis );
215 }
216 else if ( fCont1 )
217 {
218 // expand both cubes and add them
219 Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
220 pCube->nLits--;
221 Min_SopAddCube( p, pCube );
222 Min_CubeXorVar( pThis, Var0, v10 ^ 3 );
223 pThis->nLits--;
224 Min_SopAddCube( p, pThis );
225 }
226 else
227 {
228 Min_SopAddCube( p, pCube );
229 Min_SopAddCube( p, pThis );
230 }
231 // otherwise, no change is possible
232 continue;
233 }
234
235 // if one of them does not have DC lit, move it
236 if ( v00 != 3 && v01 != 3 )
237 {
238 assert( v10 == 3 || v11 == 3 );
239 pTemp = pCube; pCube = pThis; pThis = pTemp;
240 Index = v00; v00 = v10; v10 = Index;
241 Index = v01; v01 = v11; v11 = Index;
242 }
243
244 // make sure the first cube has first var DC
245 if ( v00 != 3 )
246 {
247 assert( v01 == 3 );
248 Index = Var0; Var0 = Var1; Var1 = Index;
249 Index = v00; v00 = v01; v01 = Index;
250 Index = v10; v10 = v11; v11 = Index;
251 }
252
253 // consider both cases: both have DC lit
254 if ( v00 == 3 && v11 == 3 )
255 {
256 assert( v01 != 3 && v10 != 3 );
257 // try the remaining minterm
258 // create the temporary cube equal to the first corner
259 Min_CubeXorVar( pCube, Var0, v10 );
260 Min_CubeXorVar( pCube, Var1, 3 );
261 pCube->nLits++;
262 // check if this cube is contained
263 fCont0 = Min_CoverContainsCube( p, pCube );
264 // undo the cube transformations
265 Min_CubeXorVar( pCube, Var0, v10 );
266 Min_CubeXorVar( pCube, Var1, 3 );
267 pCube->nLits--;
268 // check the case when both are covered
269 if ( fCont0 )
270 {
271 // one of the cubes can be recycled, the other expanded and added
272 Min_CubeRecycle( p, pThis );
273 // remove the literals
274 Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
275 pCube->nLits--;
276 Min_SopAddCube( p, pCube );
277 }
278 else
279 {
280 // try two reduced cubes
281 Min_CubeXorVar( pCube, Var0, v10 );
282 pCube->nLits++;
283 // remember the cubes
284 nCubesOld = p->nCubes;
285 Min_SopAddCube( p, pCube );
286 // check if the cube is absorbed
287 if ( p->nCubes < nCubesOld + 1 )
288 { // absorbed - add the second cube
289 Min_SopAddCube( p, pThis );
290 }
291 else
292 { // remove this cube, and try another one
293 assert( pCube == p->ppStore[pCube->nLits] );
294 p->ppStore[pCube->nLits] = pCube->pNext;
295 p->nCubes--;
296
297 // return the cube to the previous state
298 Min_CubeXorVar( pCube, Var0, v10 );
299 pCube->nLits--;
300
301 // generate another reduced cube
302 Min_CubeXorVar( pThis, Var1, v01 );
303 pThis->nLits++;
304
305 // add both cubes
306 Min_SopAddCube( p, pCube );
307 Min_SopAddCube( p, pThis );
308 }
309 }
310 }
311 else // the first cube has DC lit
312 {
313 assert( v01 != 3 && v10 != 3 && v11 != 3 );
314 // try the remaining minterm
315 // create the temporary cube equal to the minterm
316 Min_CubeXorVar( pThis, Var0, 3 );
317 // check if this cube is contained
318 fCont0 = Min_CoverContainsCube( p, pThis );
319 // undo the cube transformations
320 Min_CubeXorVar( pThis, Var0, 3 );
321 // check the case when both are covered
322 if ( fCont0 )
323 {
324 // one of the cubes can be recycled, the other expanded and added
325 Min_CubeRecycle( p, pThis );
326 // remove the literals
327 Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
328 pCube->nLits--;
329 Min_SopAddCube( p, pCube );
330 }
331 else
332 {
333 // try reshaping the cubes
334 // reduce the first cube
335 Min_CubeXorVar( pCube, Var0, v10 );
336 pCube->nLits++;
337 // expand the second cube
338 Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
339 pThis->nLits--;
340 // add both cubes
341 Min_SopAddCube( p, pCube );
342 Min_SopAddCube( p, pThis );
343 }
344 }
345 }
346 // printf( "Pairs = %d ", nPairs );
347 }
348
349 /**Function*************************************************************
350
351 Synopsis [Adds cube to the SOP cover stored in the manager.]
352
353 Description [Returns 0 if the cube is added or removed. Returns 1
354 if the cube is glued with some other cube and has to be added again.]
355
356 SideEffects []
357
358 SeeAlso []
359
360 ***********************************************************************/
Min_SopAddCubeInt(Min_Man_t * p,Min_Cube_t * pCube)361 int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
362 {
363 Min_Cube_t * pThis, * pThis2, ** ppPrev;
364 int i;
365 // try to find the identical cube
366 Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
367 {
368 if ( Min_CubesAreEqual( pCube, pThis ) )
369 {
370 Min_CubeRecycle( p, pCube );
371 return 0;
372 }
373 }
374 // try to find a containing cube
375 for ( i = 0; i < (int)pCube->nLits; i++ )
376 Min_CoverForEachCube( p->ppStore[i], pThis )
377 {
378 if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
379 {
380 Min_CubeRecycle( p, pCube );
381 return 0;
382 }
383 }
384 // try to find distance one in the same bin
385 Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
386 {
387 if ( Min_CubesDistOne( pCube, pThis, NULL ) )
388 {
389 *ppPrev = pThis->pNext;
390 Min_CubesTransformOr( pCube, pThis );
391 pCube->nLits--;
392 Min_CubeRecycle( p, pThis );
393 p->nCubes--;
394 return 1;
395 }
396 }
397
398 // clean the other cubes using this one
399 for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ )
400 {
401 ppPrev = &p->ppStore[i];
402 Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 )
403 {
404 if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) )
405 {
406 *ppPrev = pThis->pNext;
407 Min_CubeRecycle( p, pThis );
408 p->nCubes--;
409 }
410 else
411 ppPrev = &pThis->pNext;
412 }
413 }
414
415 // add the cube
416 pCube->pNext = p->ppStore[pCube->nLits];
417 p->ppStore[pCube->nLits] = pCube;
418 p->nCubes++;
419 return 0;
420 }
421
422 /**Function*************************************************************
423
424 Synopsis [Adds the cube to storage.]
425
426 Description []
427
428 SideEffects []
429
430 SeeAlso []
431
432 ***********************************************************************/
Min_SopAddCube(Min_Man_t * p,Min_Cube_t * pCube)433 void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
434 {
435 assert( Min_CubeCheck( pCube ) );
436 assert( pCube != p->pBubble );
437 assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
438 while ( Min_SopAddCubeInt( p, pCube ) );
439 }
440
441
442
443
444
445 /**Function*************************************************************
446
447 Synopsis []
448
449 Description []
450
451 SideEffects []
452
453 SeeAlso []
454
455 ***********************************************************************/
Min_SopContain(Min_Man_t * p)456 void Min_SopContain( Min_Man_t * p )
457 {
458 Min_Cube_t * pCube, * pCube2, ** ppPrev;
459 int i, k;
460 for ( i = 0; i <= p->nVars; i++ )
461 {
462 Min_CoverForEachCube( p->ppStore[i], pCube )
463 Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev )
464 {
465 if ( !Min_CubesAreEqual( pCube, pCube2 ) )
466 continue;
467 *ppPrev = pCube2->pNext;
468 Min_CubeRecycle( p, pCube2 );
469 p->nCubes--;
470 }
471 for ( k = i + 1; k <= p->nVars; k++ )
472 Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev )
473 {
474 if ( !Min_CubeIsContained( pCube, pCube2 ) )
475 continue;
476 *ppPrev = pCube2->pNext;
477 Min_CubeRecycle( p, pCube2 );
478 p->nCubes--;
479 }
480 }
481 }
482
483 /**Function*************************************************************
484
485 Synopsis []
486
487 Description []
488
489 SideEffects []
490
491 SeeAlso []
492
493 ***********************************************************************/
Min_SopDist1Merge(Min_Man_t * p)494 void Min_SopDist1Merge( Min_Man_t * p )
495 {
496 Min_Cube_t * pCube, * pCube2, * pCubeNew;
497 int i;
498 for ( i = p->nVars; i >= 0; i-- )
499 {
500 Min_CoverForEachCube( p->ppStore[i], pCube )
501 Min_CoverForEachCube( pCube->pNext, pCube2 )
502 {
503 assert( pCube->nLits == pCube2->nLits );
504 if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
505 continue;
506 pCubeNew = Min_CubesXor( p, pCube, pCube2 );
507 assert( pCubeNew->nLits == pCube->nLits - 1 );
508 pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
509 p->ppStore[pCubeNew->nLits] = pCubeNew;
510 p->nCubes++;
511 }
512 }
513 }
514
515 /**Function*************************************************************
516
517 Synopsis []
518
519 Description []
520
521 SideEffects []
522
523 SeeAlso []
524
525 ***********************************************************************/
Min_SopComplement(Min_Man_t * p,Min_Cube_t * pSharp)526 Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
527 {
528 Vec_Int_t * vVars;
529 Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev;
530 int Num, Value, i;
531
532 // get the variables
533 vVars = Vec_IntAlloc( 100 );
534 // create the tautology cube
535 pCover = Min_CubeAlloc( p );
536 // sharp it with all cubes
537 Min_CoverForEachCube( pSharp, pCube )
538 Min_CoverForEachCubePrev( pCover, pThis, ppPrev )
539 {
540 if ( Min_CubesDisjoint( pThis, pCube ) )
541 continue;
542 // remember the next pointer
543 pNext = pThis->pNext;
544 // get the variables, in which pThis is '-' while pCube is fixed
545 Min_CoverGetDisjVars( pThis, pCube, vVars );
546 // generate the disjoint cubes
547 pReady = pThis;
548 Vec_IntForEachEntryReverse( vVars, Num, i )
549 {
550 // correct the literal
551 Min_CubeXorVar( pReady, vVars->pArray[i], 3 );
552 if ( i == 0 )
553 break;
554 // create the new cube and clean this value
555 Value = Min_CubeGetVar( pReady, vVars->pArray[i] );
556 pReady = Min_CubeDup( p, pReady );
557 Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value );
558 // add to the cover
559 *ppPrev = pReady;
560 ppPrev = &pReady->pNext;
561 }
562 pThis = pReady;
563 pThis->pNext = pNext;
564 }
565 Vec_IntFree( vVars );
566
567 // perform dist-1 merge and contain
568 Min_CoverExpandRemoveEqual( p, pCover );
569 Min_SopDist1Merge( p );
570 Min_SopContain( p );
571 return Min_CoverCollect( p, p->nVars );
572 }
573
574 /**Function*************************************************************
575
576 Synopsis []
577
578 Description []
579
580 SideEffects []
581
582 SeeAlso []
583
584 ***********************************************************************/
Min_SopCheck(Min_Man_t * p)585 int Min_SopCheck( Min_Man_t * p )
586 {
587 Min_Cube_t * pCube, * pThis;
588 int i;
589
590 pCube = Min_CubeAlloc( p );
591 Min_CubeXorBit( pCube, 2*0+1 );
592 Min_CubeXorBit( pCube, 2*1+1 );
593 Min_CubeXorBit( pCube, 2*2+0 );
594 Min_CubeXorBit( pCube, 2*3+0 );
595 Min_CubeXorBit( pCube, 2*4+0 );
596 Min_CubeXorBit( pCube, 2*5+1 );
597 Min_CubeXorBit( pCube, 2*6+1 );
598 pCube->nLits = 7;
599
600 // Min_CubeWrite( stdout, pCube );
601
602 // check that the cubes contain it
603 for ( i = 0; i <= p->nVars; i++ )
604 Min_CoverForEachCube( p->ppStore[i], pThis )
605 if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
606 {
607 Min_CubeRecycle( p, pCube );
608 return 1;
609 }
610 Min_CubeRecycle( p, pCube );
611 return 0;
612 }
613
614 ////////////////////////////////////////////////////////////////////////
615 /// END OF FILE ///
616 ////////////////////////////////////////////////////////////////////////
617
618
619 ABC_NAMESPACE_IMPL_END
620
621