ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
covCore.c
Go to the documentation of this file.
1
20
21#include "cov.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
30static void Abc_NtkCovCovers( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose );
31static int Abc_NtkCovCoversOne( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose );
32static void Abc_NtkCovCovers_rec( Cov_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary );
33/*
34static int Abc_NodeCovPropagateEsop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
35static int Abc_NodeCovPropagateSop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
36static int Abc_NodeCovUnionEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
37static int Abc_NodeCovUnionSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
38static int Abc_NodeCovProductEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
39static int Abc_NodeCovProductSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
40*/
41static int Abc_NodeCovPropagate( Cov_Man_t * p, Abc_Obj_t * pObj );
42static Min_Cube_t * Abc_NodeCovProduct( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
43static Min_Cube_t * Abc_NodeCovSum( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
44
48
60Abc_Ntk_t * Abc_NtkSopEsopCover( Abc_Ntk_t * pNtk, int nFaninMax, int nCubesMax, int fUseEsop, int fUseSop, int fUseInvs, int fVerbose )
61{
62 Abc_Ntk_t * pNtkNew;
63 Cov_Man_t * p;
64
65 assert( Abc_NtkIsStrash(pNtk) );
66
67 // create the manager
68 p = Cov_ManAlloc( pNtk, nFaninMax, nCubesMax );
69 p->fUseEsop = fUseEsop;
70 p->fUseSop = fUseSop;
71 pNtk->pManCut = p;
72
73 // perform mapping
74 Abc_NtkCovCovers( p, pNtk, fVerbose );
75
76 // derive the final network
77// if ( fUseInvs )
78// pNtkNew = Abc_NtkCovDeriveClean( p, pNtk );
79// else
80// pNtkNew = Abc_NtkCovDerive( p, pNtk );
81// pNtkNew = NULL;
82 pNtkNew = Abc_NtkCovDeriveRegular( p, pNtk );
83
84 Cov_ManFree( p );
85 pNtk->pManCut = NULL;
86
87 // make sure that everything is okay
88 if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) )
89 {
90 printf( "Abc_NtkCov: The network check has failed.\n" );
91 Abc_NtkDelete( pNtkNew );
92 return NULL;
93 }
94 return pNtkNew;
95}
96
108void Abc_NtkCovCovers( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose )
109{
110 Abc_Obj_t * pObj;
111 int i;
112 abctime clk = Abc_Clock();
113
114 // start the manager
115 p->vFanCounts = Abc_NtkFanoutCounts(pNtk);
116
117 // set trivial cuts for the constant and the CIs
118 pObj = Abc_AigConst1(pNtk);
119 pObj->fMarkA = 1;
120 Abc_NtkForEachCi( pNtk, pObj, i )
121 pObj->fMarkA = 1;
122
123 // perform iterative decomposition
124 for ( i = 0; ; i++ )
125 {
126 if ( fVerbose )
127 printf( "Iter %d : ", i+1 );
128 if ( Abc_NtkCovCoversOne(p, pNtk, fVerbose) )
129 break;
130 }
131
132 // clean the cut-point markers
133 Abc_NtkForEachObj( pNtk, pObj, i )
134 pObj->fMarkA = 0;
135
136if ( fVerbose )
137{
138ABC_PRT( "Total", Abc_Clock() - clk );
139}
140}
141
153int Abc_NtkCovCoversOne( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose )
154{
155 ProgressBar * pProgress;
156 Abc_Obj_t * pObj;
157 Vec_Ptr_t * vBoundary;
158 int i;
159 abctime clk = Abc_Clock();
160 int Counter = 0;
161 int fStop = 1;
162
163 // array to collect the nodes in the new boundary
164 vBoundary = Vec_PtrAlloc( 100 );
165
166 // start from the COs and mark visited nodes using pObj->fMarkB
167 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
168 Abc_NtkForEachCo( pNtk, pObj, i )
169 {
170 Extra_ProgressBarUpdate( pProgress, i, NULL );
171 // skip the solved nodes (including the CIs)
172 pObj = Abc_ObjFanin0(pObj);
173 if ( pObj->fMarkA )
174 {
175 Counter++;
176 continue;
177 }
178
179 // traverse the cone starting from this node
180 if ( Abc_ObjGetSupp(pObj) == NULL )
181 Abc_NtkCovCovers_rec( p, pObj, vBoundary );
182
183 // count the number of solved cones
184 if ( Abc_ObjGetSupp(pObj) == NULL )
185 fStop = 0;
186 else
187 Counter++;
188
189/*
190 printf( "%-15s : ", Abc_ObjName(pObj) );
191 printf( "lev = %5d ", pObj->Level );
192 if ( Abc_ObjGetSupp(pObj) == NULL )
193 {
194 printf( "\n" );
195 continue;
196 }
197 printf( "supp = %3d ", Abc_ObjGetSupp(pObj)->nSize );
198 printf( "esop = %3d ", Min_CoverCountCubes( Abc_ObjGetCover2(pObj) ) );
199 printf( "\n" );
200*/
201 }
202 Extra_ProgressBarStop( pProgress );
203
204 // clean visited nodes
205 Abc_NtkForEachObj( pNtk, pObj, i )
206 pObj->fMarkB = 0;
207
208 // create the new boundary
209 p->nBoundary = 0;
210 Vec_PtrForEachEntry( Abc_Obj_t *, vBoundary, pObj, i )
211 {
212 if ( !pObj->fMarkA )
213 {
214 pObj->fMarkA = 1;
215 p->nBoundary++;
216 }
217 }
218 Vec_PtrFree( vBoundary );
219
220if ( fVerbose )
221{
222 printf( "Outs = %4d (%4d) Node = %6d (%6d) Max = %6d Bound = %4d ",
223 Counter, Abc_NtkCoNum(pNtk), p->nSupps, Abc_NtkNodeNum(pNtk), p->nSuppsMax, p->nBoundary );
224ABC_PRT( "T", Abc_Clock() - clk );
225}
226 return fStop;
227}
228
240void Abc_NtkCovCovers_rec( Cov_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary )
241{
242 Abc_Obj_t * pObj0, * pObj1;
243 // return if the support is already computed
244 if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here???
245 return;
246 // mark as visited
247 pObj->fMarkB = 1;
248 // get the fanins
249 pObj0 = Abc_ObjFanin0(pObj);
250 pObj1 = Abc_ObjFanin1(pObj);
251 // solve for the fanins
252 Abc_NtkCovCovers_rec( p, pObj0, vBoundary );
253 Abc_NtkCovCovers_rec( p, pObj1, vBoundary );
254 // skip the node that spaced out
255 if ( (!pObj0->fMarkA && !Abc_ObjGetSupp(pObj0)) || // fanin is not ready
256 (!pObj1->fMarkA && !Abc_ObjGetSupp(pObj1)) || // fanin is not ready
257 !Abc_NodeCovPropagate( p, pObj ) ) // node's support or covers cannot be computed
258 {
259 // save the nodes of the future boundary
260 if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) )
261 Vec_PtrPush( vBoundary, pObj0 );
262 if ( !pObj1->fMarkA && Abc_ObjGetSupp(pObj1) )
263 Vec_PtrPush( vBoundary, pObj1 );
264 return;
265 }
266 // consider dropping the fanin supports
267// Abc_NodeCovDropData( p, pObj0 );
268// Abc_NodeCovDropData( p, pObj1 );
269}
270
282Vec_Int_t * Abc_NodeCovSupport( Cov_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1 )
283{
284 Vec_Int_t * vSupp;
285 int k0, k1;
286
287 assert( vSupp0 && vSupp1 );
288 Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 );
289 Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 );
290 Vec_IntClear( p->vPairs0 );
291 Vec_IntClear( p->vPairs1 );
292
293 vSupp = Vec_IntAlloc( vSupp0->nSize + vSupp1->nSize );
294 for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; )
295 {
296 if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] )
297 {
298 Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
299 Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
300 Vec_IntPush( p->vPairs0, k0 );
301 Vec_IntPush( p->vPairs1, k1 );
302 Vec_IntPush( vSupp, vSupp0->pArray[k0] );
303 k0++; k1++;
304 }
305 else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] )
306 {
307 Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
308 Vec_IntPush( vSupp, vSupp0->pArray[k0] );
309 k0++;
310 }
311 else
312 {
313 Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
314 Vec_IntPush( vSupp, vSupp1->pArray[k1] );
315 k1++;
316 }
317 }
318 for ( ; k0 < vSupp0->nSize; k0++ )
319 {
320 Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
321 Vec_IntPush( vSupp, vSupp0->pArray[k0] );
322 }
323 for ( ; k1 < vSupp1->nSize; k1++ )
324 {
325 Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
326 Vec_IntPush( vSupp, vSupp1->pArray[k1] );
327 }
328/*
329 printf( "Zero : " );
330 for ( k0 = 0; k0 < vSupp0->nSize; k0++ )
331 printf( "%d ", vSupp0->pArray[k0] );
332 printf( "\n" );
333
334 printf( "One : " );
335 for ( k1 = 0; k1 < vSupp1->nSize; k1++ )
336 printf( "%d ", vSupp1->pArray[k1] );
337 printf( "\n" );
338
339 printf( "Sum : " );
340 for ( k0 = 0; k0 < vSupp->nSize; k0++ )
341 printf( "%d ", vSupp->pArray[k0] );
342 printf( "\n" );
343 printf( "\n" );
344*/
345 return vSupp;
346}
347
359int Abc_NodeCovPropagate( Cov_Man_t * p, Abc_Obj_t * pObj )
360{
361 Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL;
362 Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1;
363 Vec_Int_t * vSupp, * vSupp0, * vSupp1;
364 Abc_Obj_t * pObj0, * pObj1;
365 int fCompl0, fCompl1;
366
367 pObj0 = Abc_ObjFanin0( pObj );
368 pObj1 = Abc_ObjFanin1( pObj );
369
370 if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
371 if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
372
373 // get the resulting support
374 vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
375 vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
376 vSupp = Abc_NodeCovSupport( p, vSupp0, vSupp1 );
377
378 // quit if support if too large
379 if ( vSupp->nSize > p->nFaninMax )
380 {
381 Vec_IntFree( vSupp );
382 return 0;
383 }
384
385 // get the complemented attributes
386 fCompl0 = Abc_ObjFaninC0( pObj );
387 fCompl1 = Abc_ObjFaninC1( pObj );
388
389 // propagate ESOP
390 if ( p->fUseEsop )
391 {
392 // get the covers
393 pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
394 pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
395 if ( pCov0 && pCov1 )
396 {
397 // complement the first if needed
398 if ( !fCompl0 )
399 pCover0 = pCov0;
400 else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
401 pCover0 = pCov0->pNext;
402 else
403 pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;
404
405 // complement the second if needed
406 if ( !fCompl1 )
407 pCover1 = pCov1;
408 else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
409 pCover1 = pCov1->pNext;
410 else
411 pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;
412
413 // derive the new cover
414 pCoverX = Abc_NodeCovProduct( p, pCover0, pCover1, 1, vSupp->nSize );
415 }
416 }
417 // propagate SOPs
418 if ( p->fUseSop )
419 {
420 // get the covers for the direct polarity
421 pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
422 pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
423 // derive the new cover
424 if ( pCover0 && pCover1 )
425 pCoverP = Abc_NodeCovProduct( p, pCover0, pCover1, 0, vSupp->nSize );
426
427 // get the covers for the inverse polarity
428 pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
429 pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
430 // derive the new cover
431 if ( pCover0 && pCover1 )
432 pCoverN = Abc_NodeCovSum( p, pCover0, pCover1, 0, vSupp->nSize );
433 }
434
435 // if none of the covers can be computed quit
436 if ( !pCoverX && !pCoverP && !pCoverN )
437 {
438 Vec_IntFree( vSupp );
439 return 0;
440 }
441
442 // set the covers
443 assert( Abc_ObjGetSupp(pObj) == NULL );
444 Abc_ObjSetSupp( pObj, vSupp );
445 Abc_ObjSetCover( pObj, pCoverP, 0 );
446 Abc_ObjSetCover( pObj, pCoverN, 1 );
447 Abc_ObjSetCover2( pObj, pCoverX );
448//printf( "%3d : %4d %4d %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) );
449
450 // count statistics
451 p->nSupps++;
452 p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps );
453 return 1;
454}
455
456
457
469Min_Cube_t * Abc_NodeCovProduct( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
470{
471 Min_Cube_t * pCube, * pCube0, * pCube1;
472 Min_Cube_t * pCover;
473 int i, Val0, Val1;
474 assert( pCover0 && pCover1 );
475
476 // clean storage
477 Min_ManClean( p->pManMin, nSupp );
478 // go through the cube pairs
479 Min_CoverForEachCube( pCover0, pCube0 )
480 Min_CoverForEachCube( pCover1, pCube1 )
481 {
482 // go through the support variables of the cubes
483 for ( i = 0; i < p->vPairs0->nSize; i++ )
484 {
485 Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
486 Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
487 if ( (Val0 & Val1) == 0 )
488 break;
489 }
490 // check disjointness
491 if ( i < p->vPairs0->nSize )
492 continue;
493
494 if ( p->pManMin->nCubes > p->nCubesMax )
495 {
496 pCover = Min_CoverCollect( p->pManMin, nSupp );
497//Min_CoverWriteFile( pCover, "large", 1 );
498 Min_CoverRecycle( p->pManMin, pCover );
499 return NULL;
500 }
501
502 // create the product cube
503 pCube = Min_CubeAlloc( p->pManMin );
504
505 // add the literals
506 pCube->nLits = 0;
507 for ( i = 0; i < nSupp; i++ )
508 {
509 if ( p->vComTo0->pArray[i] == -1 )
510 Val0 = 3;
511 else
512 Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
513
514 if ( p->vComTo1->pArray[i] == -1 )
515 Val1 = 3;
516 else
517 Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
518
519 if ( (Val0 & Val1) == 3 )
520 continue;
521
522 Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
523 pCube->nLits++;
524 }
525 // add the cube to storage
526 if ( fEsop )
527 Min_EsopAddCube( p->pManMin, pCube );
528 else
529 Min_SopAddCube( p->pManMin, pCube );
530 }
531
532 // minimize the cover
533 if ( fEsop )
534 Min_EsopMinimize( p->pManMin );
535 else
536 Min_SopMinimize( p->pManMin );
537 pCover = Min_CoverCollect( p->pManMin, nSupp );
538
539 // quit if the cover is too large
540 if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
541 {
542/*
543Min_CoverWriteFile( pCover, "large", 1 );
544 Min_CoverExpand( p->pManMin, pCover );
545 Min_EsopMinimize( p->pManMin );
546 Min_EsopMinimize( p->pManMin );
547 Min_EsopMinimize( p->pManMin );
548 Min_EsopMinimize( p->pManMin );
549 Min_EsopMinimize( p->pManMin );
550 Min_EsopMinimize( p->pManMin );
551 Min_EsopMinimize( p->pManMin );
552 Min_EsopMinimize( p->pManMin );
553 Min_EsopMinimize( p->pManMin );
554 pCover = Min_CoverCollect( p->pManMin, nSupp );
555*/
556 Min_CoverRecycle( p->pManMin, pCover );
557 return NULL;
558 }
559 return pCover;
560}
561
573Min_Cube_t * Abc_NodeCovSum( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
574{
575 Min_Cube_t * pCube, * pCube0, * pCube1;
576 Min_Cube_t * pCover;
577 int i, Val0, Val1;
578 assert( pCover0 && pCover1 );
579
580 // clean storage
581 Min_ManClean( p->pManMin, nSupp );
582 Min_CoverForEachCube( pCover0, pCube0 )
583 {
584 // create the cube
585 pCube = Min_CubeAlloc( p->pManMin );
586 pCube->nLits = 0;
587 for ( i = 0; i < p->vComTo0->nSize; i++ )
588 {
589 if ( p->vComTo0->pArray[i] == -1 )
590 continue;
591 Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
592 if ( Val0 == 3 )
593 continue;
594 Min_CubeXorVar( pCube, i, Val0 ^ 3 );
595 pCube->nLits++;
596 }
597 if ( p->pManMin->nCubes > p->nCubesMax )
598 {
599 pCover = Min_CoverCollect( p->pManMin, nSupp );
600 Min_CoverRecycle( p->pManMin, pCover );
601 return NULL;
602 }
603 // add the cube to storage
604 if ( fEsop )
605 Min_EsopAddCube( p->pManMin, pCube );
606 else
607 Min_SopAddCube( p->pManMin, pCube );
608 }
609 Min_CoverForEachCube( pCover1, pCube1 )
610 {
611 // create the cube
612 pCube = Min_CubeAlloc( p->pManMin );
613 pCube->nLits = 0;
614 for ( i = 0; i < p->vComTo1->nSize; i++ )
615 {
616 if ( p->vComTo1->pArray[i] == -1 )
617 continue;
618 Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
619 if ( Val1 == 3 )
620 continue;
621 Min_CubeXorVar( pCube, i, Val1 ^ 3 );
622 pCube->nLits++;
623 }
624 if ( p->pManMin->nCubes > p->nCubesMax )
625 {
626 pCover = Min_CoverCollect( p->pManMin, nSupp );
627 Min_CoverRecycle( p->pManMin, pCover );
628 return NULL;
629 }
630 // add the cube to storage
631 if ( fEsop )
632 Min_EsopAddCube( p->pManMin, pCube );
633 else
634 Min_SopAddCube( p->pManMin, pCube );
635 }
636
637 // minimize the cover
638 if ( fEsop )
639 Min_EsopMinimize( p->pManMin );
640 else
641 Min_SopMinimize( p->pManMin );
642 pCover = Min_CoverCollect( p->pManMin, nSupp );
643
644 // quit if the cover is too large
645 if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
646 {
647 Min_CoverRecycle( p->pManMin, pCover );
648 return NULL;
649 }
650 return pCover;
651}
652
653
654
655
656
657
658
659#if 0
660
661
662
674int Abc_NodeCovPropagateEsop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
675{
676 Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1;
677 Vec_Int_t * vSupp, * vSupp0, * vSupp1;
678
679 if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
680 if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
681
682 // get the resulting support
683 vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
684 vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
685 vSupp = Abc_NodeCovSupport( p, vSupp0, vSupp1 );
686
687 // quit if support if too large
688 if ( vSupp->nSize > p->nFaninMax )
689 {
690 Vec_IntFree( vSupp );
691 return 0;
692 }
693
694 // get the covers
695 pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
696 pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
697
698 // complement the first if needed
699 if ( !Abc_ObjFaninC0(pObj) )
700 pCover0 = pCov0;
701 else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
702 pCover0 = pCov0->pNext;
703 else
704 pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;
705
706 // complement the second if needed
707 if ( !Abc_ObjFaninC1(pObj) )
708 pCover1 = pCov1;
709 else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
710 pCover1 = pCov1->pNext;
711 else
712 pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;
713
714 // derive and minimize the cover (quit if too large)
715 if ( !Abc_NodeCovProductEsop( p, pCover0, pCover1, vSupp->nSize ) )
716 {
717 pCover = Min_CoverCollect( p->pManMin, vSupp->nSize );
718 Min_CoverRecycle( p->pManMin, pCover );
719 Vec_IntFree( vSupp );
720 return 0;
721 }
722
723 // minimize the cover
724 Min_EsopMinimize( p->pManMin );
725 pCover = Min_CoverCollect( p->pManMin, vSupp->nSize );
726
727 // quit if the cover is too large
728 if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
729 {
730 Min_CoverRecycle( p->pManMin, pCover );
731 Vec_IntFree( vSupp );
732 return 0;
733 }
734
735 // count statistics
736 p->nSupps++;
737 p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps );
738
739 // set the covers
740 assert( Abc_ObjGetSupp(pObj) == NULL );
741 Abc_ObjSetSupp( pObj, vSupp );
742 Abc_ObjSetCover2( pObj, pCover );
743 return 1;
744}
745
757int Abc_NodeCovPropagateSop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
758{
759 Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1;
760 Vec_Int_t * vSupp, * vSupp0, * vSupp1;
761 int fCompl0, fCompl1;
762
763 if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
764 if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
765
766 // get the resulting support
767 vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
768 vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
769 vSupp = Abc_NodeCovSupport( p, vSupp0, vSupp1 );
770
771 // quit if support if too large
772 if ( vSupp->nSize > p->nFaninMax )
773 {
774 Vec_IntFree( vSupp );
775 return 0;
776 }
777
778 // get the complemented attributes
779 fCompl0 = Abc_ObjFaninC0(pObj);
780 fCompl1 = Abc_ObjFaninC1(pObj);
781
782 // prepare the positive cover
783 pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
784 pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
785
786 // derive and minimize the cover (quit if too large)
787 if ( !pCover0 || !pCover1 )
788 pCoverP = NULL;
789 else if ( !Abc_NodeCovProductSop( p, pCover0, pCover1, vSupp->nSize ) )
790 {
791 pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize );
792 Min_CoverRecycle( p->pManMin, pCoverP );
793 pCoverP = NULL;
794 }
795 else
796 {
797 Min_SopMinimize( p->pManMin );
798 pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize );
799 // quit if the cover is too large
800 if ( Min_CoverCountCubes(pCoverP) > p->nFaninMax )
801 {
802 Min_CoverRecycle( p->pManMin, pCoverP );
803 pCoverP = NULL;
804 }
805 }
806
807 // prepare the negative cover
808 pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
809 pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
810
811 // derive and minimize the cover (quit if too large)
812 if ( !pCover0 || !pCover1 )
813 pCoverN = NULL;
814 else if ( !Abc_NodeCovUnionSop( p, pCover0, pCover1, vSupp->nSize ) )
815 {
816 pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize );
817 Min_CoverRecycle( p->pManMin, pCoverN );
818 pCoverN = NULL;
819 }
820 else
821 {
822 Min_SopMinimize( p->pManMin );
823 pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize );
824 // quit if the cover is too large
825 if ( Min_CoverCountCubes(pCoverN) > p->nFaninMax )
826 {
827 Min_CoverRecycle( p->pManMin, pCoverN );
828 pCoverN = NULL;
829 }
830 }
831
832 if ( pCoverP == NULL && pCoverN == NULL )
833 {
834 Vec_IntFree( vSupp );
835 return 0;
836 }
837
838 // count statistics
839 p->nSupps++;
840 p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps );
841
842 // set the covers
843 assert( Abc_ObjGetSupp(pObj) == NULL );
844 Abc_ObjSetSupp( pObj, vSupp );
845 Abc_ObjSetCover( pObj, pCoverP, 0 );
846 Abc_ObjSetCover( pObj, pCoverN, 1 );
847 return 1;
848}
849
850
862int Abc_NodeCovProductEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
863{
864 Min_Cube_t * pCube, * pCube0, * pCube1;
865 int i, Val0, Val1;
866
867 // clean storage
868 Min_ManClean( p->pManMin, nSupp );
869 if ( pCover0 == NULL || pCover1 == NULL )
870 return 1;
871
872 // go through the cube pairs
873 Min_CoverForEachCube( pCover0, pCube0 )
874 Min_CoverForEachCube( pCover1, pCube1 )
875 {
876 // go through the support variables of the cubes
877 for ( i = 0; i < p->vPairs0->nSize; i++ )
878 {
879 Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
880 Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
881 if ( (Val0 & Val1) == 0 )
882 break;
883 }
884 // check disjointness
885 if ( i < p->vPairs0->nSize )
886 continue;
887
888 if ( p->pManMin->nCubes >= p->nCubesMax )
889 return 0;
890
891 // create the product cube
892 pCube = Min_CubeAlloc( p->pManMin );
893
894 // add the literals
895 pCube->nLits = 0;
896 for ( i = 0; i < nSupp; i++ )
897 {
898 if ( p->vComTo0->pArray[i] == -1 )
899 Val0 = 3;
900 else
901 Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
902
903 if ( p->vComTo1->pArray[i] == -1 )
904 Val1 = 3;
905 else
906 Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
907
908 if ( (Val0 & Val1) == 3 )
909 continue;
910
911 Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
912 pCube->nLits++;
913 }
914 // add the cube to storage
915 Min_EsopAddCube( p->pManMin, pCube );
916 }
917 return 1;
918}
919
931int Abc_NodeCovProductSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
932{
933 return 1;
934}
935
936
937
949int Abc_NodeCovUnionEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
950{
951 Min_Cube_t * pCube, * pCube0, * pCube1;
952 int i, Val0, Val1;
953
954 // clean storage
955 Min_ManClean( p->pManMin, nSupp );
956 if ( pCover0 )
957 {
958 Min_CoverForEachCube( pCover0, pCube0 )
959 {
960 // create the cube
961 pCube = Min_CubeAlloc( p->pManMin );
962 pCube->nLits = 0;
963 for ( i = 0; i < p->vComTo0->nSize; i++ )
964 {
965 if ( p->vComTo0->pArray[i] == -1 )
966 continue;
967 Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
968 if ( Val0 == 3 )
969 continue;
970 Min_CubeXorVar( pCube, i, Val0 ^ 3 );
971 pCube->nLits++;
972 }
973 if ( p->pManMin->nCubes >= p->nCubesMax )
974 return 0;
975 // add the cube to storage
976 Min_EsopAddCube( p->pManMin, pCube );
977 }
978 }
979 if ( pCover1 )
980 {
981 Min_CoverForEachCube( pCover1, pCube1 )
982 {
983 // create the cube
984 pCube = Min_CubeAlloc( p->pManMin );
985 pCube->nLits = 0;
986 for ( i = 0; i < p->vComTo1->nSize; i++ )
987 {
988 if ( p->vComTo1->pArray[i] == -1 )
989 continue;
990 Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
991 if ( Val1 == 3 )
992 continue;
993 Min_CubeXorVar( pCube, i, Val1 ^ 3 );
994 pCube->nLits++;
995 }
996 if ( p->pManMin->nCubes >= p->nCubesMax )
997 return 0;
998 // add the cube to storage
999 Min_EsopAddCube( p->pManMin, pCube );
1000 }
1001 }
1002 return 1;
1003}
1004
1016int Abc_NodeCovUnionSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
1017{
1018 return 1;
1019}
1020
1021
1022#endif
1023
1027
1028
1029ABC_NAMESPACE_IMPL_END
1030
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkForEachCo
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition abc.h:522
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition abcCheck.c:64
Abc_NtkForEachObj
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition abc.h:449
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_NtkFanoutCounts
ABC_DLL Vec_Int_t * Abc_NtkFanoutCounts(Abc_Ntk_t *pNtk)
Definition abcUtil.c:1741
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition abc.h:518
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition abcNtk.c:1421
Abc_AigConst1
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition abcAig.c:683
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
ProgressBar
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
Abc_NodeCovSupport
Vec_Int_t * Abc_NodeCovSupport(Cov_Man_t *p, Vec_Int_t *vSupp0, Vec_Int_t *vSupp1)
Definition covCore.c:282
Abc_NtkSopEsopCover
Abc_Ntk_t * Abc_NtkSopEsopCover(Abc_Ntk_t *pNtk, int nFaninMax, int nCubesMax, int fUseEsop, int fUseSop, int fUseInvs, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition covCore.c:60
Min_CoverCollect
Min_Cube_t * Min_CoverCollect(Min_Man_t *p, int nSuppSize)
Definition covMinUtil.c:264
Min_Cube_t
struct Min_Cube_t_ Min_Cube_t
Definition covInt.h:35
Min_CoverForEachCube
#define Min_CoverForEachCube(pCover, pCube)
Definition covInt.h:65
Min_ManClean
void Min_ManClean(Min_Man_t *p, int nSupp)
Definition covMinMan.c:83
Min_EsopAddCube
void Min_EsopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition covMinEsop.c:291
Min_SopMinimize
void Min_SopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition covMinSop.c:47
Min_SopAddCube
void Min_SopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition covMinSop.c:433
Min_EsopMinimize
void Min_EsopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition covMinEsop.c:47
Cov_ManFree
void Cov_ManFree(Cov_Man_t *p)
Definition covMan.c:92
Abc_NtkCovDeriveRegular
Abc_Ntk_t * Abc_NtkCovDeriveRegular(Cov_Man_t *p, Abc_Ntk_t *pNtk)
Definition covBuild.c:503
Cov_Man_t
typedefABC_NAMESPACE_HEADER_START struct Cov_Man_t_ Cov_Man_t
DECLARATIONS ///.
Definition cov.h:34
Cov_ManAlloc
Cov_Man_t * Cov_ManAlloc(Abc_Ntk_t *pNtk, int nFaninMax, int nCubesMax)
DECLARATIONS ///.
Definition covMan.c:45
p
Cube * p
Definition exorList.c:222
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition extraUtilProgress.c:118
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition extraUtilProgress.c:62
Abc_Ntk_t_::pManCut
void * pManCut
Definition abc.h:193
Abc_Obj_t_::Id
int Id
Definition abc.h:132
Abc_Obj_t_::fMarkB
unsigned fMarkB
Definition abc.h:135
Abc_Obj_t_::fMarkA
unsigned fMarkA
Definition abc.h:134
Min_Cube_t_::nLits
unsigned nLits
Definition covInt.h:59
Min_Cube_t_::pNext
Min_Cube_t * pNext
Definition covInt.h:56
assert
#define assert(ex)
Definition util_old.h:213
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55