abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
covCore.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [covCore.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Mapping into network of SOPs/ESOPs.]
8 
9  Synopsis [Core procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: covCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "cov.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static void Abc_NtkCovCovers( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose );
31 static int Abc_NtkCovCoversOne( Cov_Man_t * p, Abc_Ntk_t * pNtk, int fVerbose );
32 static void Abc_NtkCovCovers_rec( Cov_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary );
33 /*
34 static int Abc_NodeCovPropagateEsop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
35 static int Abc_NodeCovPropagateSop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
36 static int Abc_NodeCovUnionEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
37 static int Abc_NodeCovUnionSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
38 static int Abc_NodeCovProductEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
39 static int Abc_NodeCovProductSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
40 */
41 static int Abc_NodeCovPropagate( Cov_Man_t * p, Abc_Obj_t * pObj );
42 static Min_Cube_t * Abc_NodeCovProduct( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
43 static Min_Cube_t * Abc_NodeCovSum( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
44 
45 ////////////////////////////////////////////////////////////////////////
46 /// FUNCTION DEFINITIONS ///
47 ////////////////////////////////////////////////////////////////////////
48 
49 /**Function*************************************************************
50 
51  Synopsis [Performs decomposition.]
52 
53  Description []
54 
55  SideEffects []
56 
57  SeeAlso []
58 
59 ***********************************************************************/
60 Abc_Ntk_t * Abc_NtkSopEsopCover( Abc_Ntk_t * pNtk, int nFaninMax, 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 );
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 
97 /**Function*************************************************************
98 
99  Synopsis [Compute the supports.]
100 
101  Description []
102 
103  SideEffects []
104 
105  SeeAlso []
106 
107 ***********************************************************************/
108 void 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 
136 if ( fVerbose )
137 {
138 ABC_PRT( "Total", Abc_Clock() - clk );
139 }
140 }
141 
142 /**Function*************************************************************
143 
144  Synopsis [Compute the supports.]
145 
146  Description []
147 
148  SideEffects []
149 
150  SeeAlso []
151 
152 ***********************************************************************/
153 int 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 
220 if ( 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 );
224 ABC_PRT( "T", Abc_Clock() - clk );
225 }
226  return fStop;
227 }
228 
229 /**Function*************************************************************
230 
231  Synopsis []
232 
233  Description []
234 
235  SideEffects []
236 
237  SeeAlso []
238 
239 ***********************************************************************/
240 void 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 
271 /**Function*************************************************************
272 
273  Synopsis []
274 
275  Description []
276 
277  SideEffects []
278 
279  SeeAlso []
280 
281 ***********************************************************************/
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 
348 /**Function*************************************************************
349 
350  Synopsis [Propagates all types of covers.]
351 
352  Description []
353 
354  SideEffects []
355 
356  SeeAlso []
357 
358 ***********************************************************************/
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 
458 /**Function*************************************************************
459 
460  Synopsis []
461 
462  Description []
463 
464  SideEffects []
465 
466  SeeAlso []
467 
468 ***********************************************************************/
469 Min_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 /*
543 Min_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 
562 /**Function*************************************************************
563 
564  Synopsis []
565 
566  Description []
567 
568  SideEffects []
569 
570  SeeAlso []
571 
572 ***********************************************************************/
573 Min_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 
663 /**Function*************************************************************
664 
665  Synopsis []
666 
667  Description []
668 
669  SideEffects []
670 
671  SeeAlso []
672 
673 ***********************************************************************/
674 int 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 
746 /**Function*************************************************************
747 
748  Synopsis []
749 
750  Description []
751 
752  SideEffects []
753 
754  SeeAlso []
755 
756 ***********************************************************************/
757 int 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 
851 /**Function*************************************************************
852 
853  Synopsis []
854 
855  Description []
856 
857  SideEffects []
858 
859  SeeAlso []
860 
861 ***********************************************************************/
862 int 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 
920 /**Function*************************************************************
921 
922  Synopsis []
923 
924  Description []
925 
926  SideEffects []
927 
928  SeeAlso []
929 
930 ***********************************************************************/
931 int Abc_NodeCovProductSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
932 {
933  return 1;
934 }
935 
936 
937 
938 /**Function*************************************************************
939 
940  Synopsis []
941 
942  Description []
943 
944  SideEffects []
945 
946  SeeAlso []
947 
948 ***********************************************************************/
949 int 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 
1005 /**Function*************************************************************
1006 
1007  Synopsis []
1008 
1009  Description []
1010 
1011  SideEffects []
1012 
1013  SeeAlso []
1014 
1015 ***********************************************************************/
1016 int 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 
1024 ////////////////////////////////////////////////////////////////////////
1025 /// END OF FILE ///
1026 ////////////////////////////////////////////////////////////////////////
1027 
1028 
1030 
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
static Vec_Int_t * Abc_ObjGetSupp(Abc_Obj_t *pObj)
Definition: cov.h:74
unsigned fMarkA
Definition: abc.h:134
static void Min_CubeXorVar(Min_Cube_t *p, int Var, int Value)
Definition: covInt.h:87
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Int_t * Abc_NodeCovSupport(Cov_Man_t *p, Vec_Int_t *vSupp0, Vec_Int_t *vSupp1)
Definition: covCore.c:282
Min_Cube_t * pNext
Definition: covInt.h:56
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
static ABC_NAMESPACE_IMPL_START void Abc_NtkCovCovers(Cov_Man_t *p, Abc_Ntk_t *pNtk, int fVerbose)
DECLARATIONS ///.
Definition: covCore.c:108
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:288
Cov_Man_t * Cov_ManAlloc(Abc_Ntk_t *pNtk, int nFaninMax)
DECLARATIONS ///.
Definition: covMan.c:45
Abc_Ntk_t * Abc_NtkCovDeriveRegular(Cov_Man_t *p, Abc_Ntk_t *pNtk)
Definition: covBuild.c:503
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
static Min_Cube_t * Abc_ObjGetCover2(Abc_Obj_t *pObj)
Definition: cov.h:77
static int Abc_NtkCovCoversOne(Cov_Man_t *p, Abc_Ntk_t *pNtk, int fVerbose)
Definition: covCore.c:153
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
DECLARATIONS ///.
static void Abc_ObjSetCover(Abc_Obj_t *pObj, Min_Cube_t *pCov, int Pol)
Definition: cov.h:79
void Cov_ManFree(Cov_Man_t *p)
Definition: covMan.c:92
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Min_Cube_t * Min_CoverCollect(Min_Man_t *p, int nSuppSize)
Definition: covMinUtil.c:264
static Min_Cube_t * Abc_NodeCovProduct(Cov_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1, int fEsop, int nSupp)
Definition: covCore.c:469
static int Min_CubeGetVar(Min_Cube_t *p, int Var)
Definition: covInt.h:86
void Min_EsopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition: covMinEsop.c:291
static void Abc_ObjSetCover2(Abc_Obj_t *pObj, Min_Cube_t *pCov)
Definition: cov.h:76
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
static int Min_CoverCountCubes(Min_Cube_t *pCover)
Definition: covInt.h:274
void * pManCut
Definition: abc.h:193
unsigned nLits
Definition: covInt.h:59
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Counter
void Extra_ProgressBarStop(ProgressBar *p)
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static Min_Cube_t * Abc_NodeCovSum(Cov_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1, int fEsop, int nSupp)
Definition: covCore.c:573
unsigned fMarkB
Definition: abc.h:135
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
int Id
Definition: abc.h:132
#define ABC_PRT(a, t)
Definition: abc_global.h:220
#define Min_CoverForEachCube(pCover, pCube)
Definition: covInt.h:65
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
typedefABC_NAMESPACE_HEADER_START struct Cov_Man_t_ Cov_Man_t
DECLARATIONS ///.
Definition: cov.h:34
static Min_Cube_t * Min_CubeAlloc(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: covInt.h:126
ABC_DLL Vec_Int_t * Abc_NtkFanoutCounts(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:1701
#define assert(ex)
Definition: util_old.h:213
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
static void Abc_NtkCovCovers_rec(Cov_Man_t *p, Abc_Obj_t *pObj, Vec_Ptr_t *vBoundary)
Definition: covCore.c:240
static void Min_CoverRecycle(Min_Man_t *p, Min_Cube_t *pCover)
Definition: covInt.h:205
Abc_Ntk_t * Abc_NtkSopEsopCover(Abc_Ntk_t *pNtk, int nFaninMax, int fUseEsop, int fUseSop, int fUseInvs, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: covCore.c:60
static int Abc_NodeCovPropagate(Cov_Man_t *p, Abc_Obj_t *pObj)
Definition: covCore.c:359
void Min_SopAddCube(Min_Man_t *p, Min_Cube_t *pCube)
Definition: covMinSop.c:433
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Abc_ObjSetSupp(Abc_Obj_t *pObj, Vec_Int_t *vVec)
Definition: cov.h:73
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition: abc.h:446
static Min_Cube_t * Abc_ObjGetCover(Abc_Obj_t *pObj, int Pol)
Definition: cov.h:80
void Min_EsopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: covMinEsop.c:47
void Min_SopMinimize(Min_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: covMinSop.c:47
void Min_ManClean(Min_Man_t *p, int nSupp)
Definition: covMinMan.c:83
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223