abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
darCut.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [darCut.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [DAG-aware AIG rewriting.]
8 
9  Synopsis [Computation of 4-input cuts.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: darCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "darInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Prints one cut.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Dar_CutPrint( Dar_Cut_t * pCut )
46 {
47  unsigned i;
48  printf( "{" );
49  for ( i = 0; i < pCut->nLeaves; i++ )
50  printf( " %d", pCut->pLeaves[i] );
51  printf( " }\n" );
52 }
53 
54 /**Function*************************************************************
55 
56  Synopsis [Prints one cut.]
57 
58  Description []
59 
60  SideEffects []
61 
62  SeeAlso []
63 
64 ***********************************************************************/
66 {
67  Dar_Cut_t * pCut;
68  int i;
69  printf( "Cuts for node %d:\n", pObj->Id );
70  Dar_ObjForEachCut( pObj, pCut, i )
71  Dar_CutPrint( pCut );
72 // printf( "\n" );
73 }
74 
75 /**Function*************************************************************
76 
77  Synopsis [Returns the number of 1s in the machine word.]
78 
79  Description []
80 
81  SideEffects []
82 
83  SeeAlso []
84 
85 ***********************************************************************/
86 static inline int Dar_WordCountOnes( unsigned uWord )
87 {
88  uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
89  uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
90  uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
91  uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
92  return (uWord & 0x0000FFFF) + (uWord>>16);
93 }
94 
95 /**Function*************************************************************
96 
97  Synopsis [Compute the cost of the cut.]
98 
99  Description []
100 
101  SideEffects []
102 
103  SeeAlso []
104 
105 ***********************************************************************/
106 static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
107 {
108  Aig_Obj_t * pLeaf;
109  int i, Value, nOnes;
110  assert( pCut->fUsed );
111  Value = 0;
112  nOnes = 0;
113  Dar_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
114  {
115  if ( pLeaf == NULL )
116  return 0;
117  assert( pLeaf != NULL );
118  Value += pLeaf->nRefs;
119  nOnes += (pLeaf->nRefs == 1);
120  }
121  if ( pCut->nLeaves < 2 )
122  return 1001;
123 // Value = Value * 100 / pCut->nLeaves;
124  if ( Value > 1000 )
125  Value = 1000;
126  if ( nOnes > 3 )
127  Value = 5 - nOnes;
128  return Value;
129 }
130 
131 /**Function*************************************************************
132 
133  Synopsis [Returns the next free cut to use.]
134 
135  Description [Uses the cut with the smallest value.]
136 
137  SideEffects []
138 
139  SeeAlso []
140 
141 ***********************************************************************/
142 static inline Dar_Cut_t * Dar_CutFindFree( Dar_Man_t * p, Aig_Obj_t * pObj )
143 {
144  Dar_Cut_t * pCut, * pCutMax;
145  int i;
146  pCutMax = NULL;
147  Dar_ObjForEachCutAll( pObj, pCut, i )
148  {
149  if ( pCut->fUsed == 0 )
150  return pCut;
151  if ( pCut->nLeaves < 3 )
152  continue;
153  if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
154  pCutMax = pCut;
155  }
156  if ( pCutMax == NULL )
157  {
158  Dar_ObjForEachCutAll( pObj, pCut, i )
159  {
160  if ( pCut->nLeaves < 2 )
161  continue;
162  if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
163  pCutMax = pCut;
164  }
165  }
166  if ( pCutMax == NULL )
167  {
168  Dar_ObjForEachCutAll( pObj, pCut, i )
169  {
170  if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
171  pCutMax = pCut;
172  }
173  }
174  assert( pCutMax != NULL );
175  pCutMax->fUsed = 0;
176  return pCutMax;
177 }
178 
179 /**Function*************************************************************
180 
181  Synopsis [Returns 1 if pDom is contained in pCut.]
182 
183  Description []
184 
185  SideEffects []
186 
187  SeeAlso []
188 
189 ***********************************************************************/
190 static inline int Dar_CutCheckDominance( Dar_Cut_t * pDom, Dar_Cut_t * pCut )
191 {
192  int i, k;
193  assert( pDom->fUsed && pCut->fUsed );
194  for ( i = 0; i < (int)pDom->nLeaves; i++ )
195  {
196  for ( k = 0; k < (int)pCut->nLeaves; k++ )
197  if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
198  break;
199  if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
200  return 0;
201  }
202  // every node in pDom is contained in pCut
203  return 1;
204 }
205 
206 /**Function*************************************************************
207 
208  Synopsis [Returns 1 if the cut is contained.]
209 
210  Description []
211 
212  SideEffects []
213 
214  SeeAlso []
215 
216 ***********************************************************************/
217 static inline int Dar_CutFilter( Aig_Obj_t * pObj, Dar_Cut_t * pCut )
218 {
219  Dar_Cut_t * pTemp;
220  int i;
221  assert( pCut->fUsed );
222  // go through the cuts of the node
223  Dar_ObjForEachCut( pObj, pTemp, i )
224  {
225  if ( pTemp == pCut )
226  continue;
227  if ( pTemp->nLeaves > pCut->nLeaves )
228  {
229  // skip the non-contained cuts
230  if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
231  continue;
232  // check containment seriously
233  if ( Dar_CutCheckDominance( pCut, pTemp ) )
234  {
235  // remove contained cut
236  pTemp->fUsed = 0;
237  }
238  }
239  else
240  {
241  // skip the non-contained cuts
242  if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
243  continue;
244  // check containment seriously
245  if ( Dar_CutCheckDominance( pTemp, pCut ) )
246  {
247  // remove the given cut
248  pCut->fUsed = 0;
249  return 1;
250  }
251  }
252  }
253  return 0;
254 }
255 
256 /**Function*************************************************************
257 
258  Synopsis [Merges two cuts.]
259 
260  Description []
261 
262  SideEffects []
263 
264  SeeAlso []
265 
266 ***********************************************************************/
267 static inline int Dar_CutMergeOrdered( Dar_Cut_t * pC, Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
268 {
269  int i, k, c;
270  assert( pC0->nLeaves >= pC1->nLeaves );
271 
272  // the case of the largest cut sizes
273  if ( pC0->nLeaves == 4 && pC1->nLeaves == 4 )
274  {
275  if ( pC0->uSign != pC1->uSign )
276  return 0;
277  for ( i = 0; i < (int)pC0->nLeaves; i++ )
278  if ( pC0->pLeaves[i] != pC1->pLeaves[i] )
279  return 0;
280  for ( i = 0; i < (int)pC0->nLeaves; i++ )
281  pC->pLeaves[i] = pC0->pLeaves[i];
282  pC->nLeaves = pC0->nLeaves;
283  return 1;
284  }
285 
286  // the case when one of the cuts is the largest
287  if ( pC0->nLeaves == 4 )
288  {
289  if ( (pC0->uSign & pC1->uSign) != pC1->uSign )
290  return 0;
291  for ( i = 0; i < (int)pC1->nLeaves; i++ )
292  {
293  for ( k = (int)pC0->nLeaves - 1; k >= 0; k-- )
294  if ( pC0->pLeaves[k] == pC1->pLeaves[i] )
295  break;
296  if ( k == -1 ) // did not find
297  return 0;
298  }
299  for ( i = 0; i < (int)pC0->nLeaves; i++ )
300  pC->pLeaves[i] = pC0->pLeaves[i];
301  pC->nLeaves = pC0->nLeaves;
302  return 1;
303  }
304 
305  // compare two cuts with different numbers
306  i = k = 0;
307  for ( c = 0; c < 4; c++ )
308  {
309  if ( k == (int)pC1->nLeaves )
310  {
311  if ( i == (int)pC0->nLeaves )
312  {
313  pC->nLeaves = c;
314  return 1;
315  }
316  pC->pLeaves[c] = pC0->pLeaves[i++];
317  continue;
318  }
319  if ( i == (int)pC0->nLeaves )
320  {
321  if ( k == (int)pC1->nLeaves )
322  {
323  pC->nLeaves = c;
324  return 1;
325  }
326  pC->pLeaves[c] = pC1->pLeaves[k++];
327  continue;
328  }
329  if ( pC0->pLeaves[i] < pC1->pLeaves[k] )
330  {
331  pC->pLeaves[c] = pC0->pLeaves[i++];
332  continue;
333  }
334  if ( pC0->pLeaves[i] > pC1->pLeaves[k] )
335  {
336  pC->pLeaves[c] = pC1->pLeaves[k++];
337  continue;
338  }
339  pC->pLeaves[c] = pC0->pLeaves[i++];
340  k++;
341  }
342  if ( i < (int)pC0->nLeaves || k < (int)pC1->nLeaves )
343  return 0;
344  pC->nLeaves = c;
345  return 1;
346 }
347 
348 /**Function*************************************************************
349 
350  Synopsis [Prepares the object for FPGA mapping.]
351 
352  Description []
353 
354  SideEffects []
355 
356  SeeAlso []
357 
358 ***********************************************************************/
359 static inline int Dar_CutMerge( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1 )
360 {
361  assert( !pCut->fUsed );
362  // merge the nodes
363  if ( pCut0->nLeaves <= pCut1->nLeaves )
364  {
365  if ( !Dar_CutMergeOrdered( pCut, pCut1, pCut0 ) )
366  return 0;
367  }
368  else
369  {
370  if ( !Dar_CutMergeOrdered( pCut, pCut0, pCut1 ) )
371  return 0;
372  }
373  pCut->uSign = pCut0->uSign | pCut1->uSign;
374  pCut->fUsed = 1;
375  return 1;
376 }
377 
378 
379 /**Function*************************************************************
380 
381  Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
382 
383  Description []
384 
385  SideEffects []
386 
387  SeeAlso []
388 
389 ***********************************************************************/
390 static inline unsigned Dar_CutTruthPhase( Dar_Cut_t * pCut, Dar_Cut_t * pCut1 )
391 {
392  unsigned uPhase = 0;
393  int i, k;
394  for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
395  {
396  if ( k == (int)pCut1->nLeaves )
397  break;
398  if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
399  continue;
400  assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
401  uPhase |= (1 << i);
402  k++;
403  }
404  return uPhase;
405 }
406 
407 /**Function*************************************************************
408 
409  Synopsis [Swaps two advancent variables of the truth table.]
410 
411  Description [Swaps variable iVar and iVar+1.]
412 
413  SideEffects []
414 
415  SeeAlso []
416 
417 ***********************************************************************/
418 static inline unsigned Dar_CutTruthSwapAdjacentVars( unsigned uTruth, int iVar )
419 {
420  assert( iVar >= 0 && iVar <= 2 );
421  if ( iVar == 0 )
422  return (uTruth & 0x99999999) | ((uTruth & 0x22222222) << 1) | ((uTruth & 0x44444444) >> 1);
423  if ( iVar == 1 )
424  return (uTruth & 0xC3C3C3C3) | ((uTruth & 0x0C0C0C0C) << 2) | ((uTruth & 0x30303030) >> 2);
425  if ( iVar == 2 )
426  return (uTruth & 0xF00FF00F) | ((uTruth & 0x00F000F0) << 4) | ((uTruth & 0x0F000F00) >> 4);
427  assert( 0 );
428  return 0;
429 }
430 
431 /**Function*************************************************************
432 
433  Synopsis [Swaps polarity of the variable.]
434 
435  Description []
436 
437  SideEffects []
438 
439  SeeAlso []
440 
441 ***********************************************************************/
442 static inline unsigned Dar_CutTruthSwapPolarity( unsigned uTruth, int iVar )
443 {
444  assert( iVar >= 0 && iVar <= 3 );
445  if ( iVar == 0 )
446  return ((uTruth & 0xAAAA) >> 1) | ((uTruth & 0x5555) << 1);
447  if ( iVar == 1 )
448  return ((uTruth & 0xCCCC) >> 2) | ((uTruth & 0x3333) << 2);
449  if ( iVar == 2 )
450  return ((uTruth & 0xF0F0) >> 4) | ((uTruth & 0x0F0F) << 4);
451  if ( iVar == 3 )
452  return ((uTruth & 0xFF00) >> 8) | ((uTruth & 0x00FF) << 8);
453  assert( 0 );
454  return 0;
455 }
456 
457 /**Function*************************************************************
458 
459  Synopsis [Expands the truth table according to the phase.]
460 
461  Description [The input and output truth tables are in pIn/pOut. The current number
462  of variables is nVars. The total number of variables in nVarsAll. The last argument
463  (Phase) contains shows where the variables should go.]
464 
465  SideEffects []
466 
467  SeeAlso []
468 
469 ***********************************************************************/
470 static inline unsigned Dar_CutTruthStretch( unsigned uTruth, int nVars, unsigned Phase )
471 {
472  int i, k, Var = nVars - 1;
473  for ( i = 3; i >= 0; i-- )
474  if ( Phase & (1 << i) )
475  {
476  for ( k = Var; k < i; k++ )
477  uTruth = Dar_CutTruthSwapAdjacentVars( uTruth, k );
478  Var--;
479  }
480  assert( Var == -1 );
481  return uTruth;
482 }
483 
484 /**Function*************************************************************
485 
486  Synopsis [Shrinks the truth table according to the phase.]
487 
488  Description [The input and output truth tables are in pIn/pOut. The current number
489  of variables is nVars. The total number of variables in nVarsAll. The last argument
490  (Phase) contains shows what variables should remain.]
491 
492  SideEffects []
493 
494  SeeAlso []
495 
496 ***********************************************************************/
497 static inline unsigned Dar_CutTruthShrink( unsigned uTruth, int nVars, unsigned Phase )
498 {
499  int i, k, Var = 0;
500  for ( i = 0; i < 4; i++ )
501  if ( Phase & (1 << i) )
502  {
503  for ( k = i-1; k >= Var; k-- )
504  uTruth = Dar_CutTruthSwapAdjacentVars( uTruth, k );
505  Var++;
506  }
507  return uTruth;
508 }
509 
510 /**Function*************************************************************
511 
512  Synopsis [Sort variables by their ID.]
513 
514  Description []
515 
516  SideEffects []
517 
518  SeeAlso []
519 
520 ***********************************************************************/
521 unsigned Dar_CutSortVars( unsigned uTruth, int * pVars )
522 {
523  int i, Temp, fChange, Counter = 0;
524  // replace -1 by large number
525  for ( i = 0; i < 4; i++ )
526  {
527  if ( pVars[i] == -1 )
528  pVars[i] = 0x3FFFFFFF;
529  else
530  if ( Abc_LitIsCompl(pVars[i]) )
531  {
532  pVars[i] = Abc_LitNot( pVars[i] );
533  uTruth = Dar_CutTruthSwapPolarity( uTruth, i );
534  }
535  }
536 
537  // permute variables
538  do {
539  fChange = 0;
540  for ( i = 0; i < 3; i++ )
541  {
542  if ( pVars[i] <= pVars[i+1] )
543  continue;
544  Counter++;
545  fChange = 1;
546 
547  Temp = pVars[i];
548  pVars[i] = pVars[i+1];
549  pVars[i+1] = Temp;
550 
551  uTruth = Dar_CutTruthSwapAdjacentVars( uTruth, i );
552  }
553  } while ( fChange );
554 
555  // replace large number by -1
556  for ( i = 0; i < 4; i++ )
557  {
558  if ( pVars[i] == 0x3FFFFFFF )
559  pVars[i] = -1;
560 // printf( "%d ", pVars[i] );
561  }
562 // printf( "\n" );
563 
564  return uTruth;
565 }
566 
567 
568 
569 /**Function*************************************************************
570 
571  Synopsis [Performs truth table computation.]
572 
573  Description []
574 
575  SideEffects []
576 
577  SeeAlso []
578 
579 ***********************************************************************/
580 static inline unsigned Dar_CutTruth( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1, int fCompl0, int fCompl1 )
581 {
582  unsigned uTruth0 = fCompl0 ? ~pCut0->uTruth : pCut0->uTruth;
583  unsigned uTruth1 = fCompl1 ? ~pCut1->uTruth : pCut1->uTruth;
584  uTruth0 = Dar_CutTruthStretch( uTruth0, pCut0->nLeaves, Dar_CutTruthPhase(pCut, pCut0) );
585  uTruth1 = Dar_CutTruthStretch( uTruth1, pCut1->nLeaves, Dar_CutTruthPhase(pCut, pCut1) );
586  return uTruth0 & uTruth1;
587 }
588 
589 /**Function*************************************************************
590 
591  Synopsis [Minimize support of the cut.]
592 
593  Description [Returns 1 if the node's support has changed]
594 
595  SideEffects []
596 
597  SeeAlso []
598 
599 ***********************************************************************/
600 static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
601 {
602  unsigned uMasks[4][2] = {
603  { 0x5555, 0xAAAA },
604  { 0x3333, 0xCCCC },
605  { 0x0F0F, 0xF0F0 },
606  { 0x00FF, 0xFF00 }
607  };
608  unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
609  int i, k, nLeaves;
610  assert( pCut->fUsed );
611  // compute the support of the cut's function
612  nLeaves = pCut->nLeaves;
613  for ( i = 0; i < (int)pCut->nLeaves; i++ )
614  if ( (uTruth & uMasks[i][0]) == ((uTruth & uMasks[i][1]) >> (1 << i)) )
615  nLeaves--;
616  else
617  uPhase |= (1 << i);
618  if ( nLeaves == (int)pCut->nLeaves )
619  return 0;
620  // shrink the truth table
621  uTruth = Dar_CutTruthShrink( uTruth, pCut->nLeaves, uPhase );
622  pCut->uTruth = 0xFFFF & uTruth;
623  // update leaves and signature
624  pCut->uSign = 0;
625  for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
626  {
627  if ( !(uPhase & (1 << i)) )
628  continue;
629  pCut->pLeaves[k++] = pCut->pLeaves[i];
630  pCut->uSign |= Aig_ObjCutSign( pCut->pLeaves[i] );
631  }
632  assert( k == nLeaves );
633  pCut->nLeaves = nLeaves;
634  return 1;
635 }
636 
637 /**Function*************************************************************
638 
639  Synopsis []
640 
641  Description []
642 
643  SideEffects []
644 
645  SeeAlso []
646 
647 ***********************************************************************/
649 {
650  if ( p->pMemCuts == NULL )
651  return;
652  Aig_MmFixedStop( p->pMemCuts, 0 );
653  p->pMemCuts = NULL;
654 // Aig_ManCleanData( p );
655 }
656 
657 /**Function*************************************************************
658 
659  Synopsis []
660 
661  Description []
662 
663  SideEffects []
664 
665  SeeAlso []
666 
667 ***********************************************************************/
669 {
670  Dar_Cut_t * pCutSet, * pCut;
671  int i;
672  assert( Dar_ObjCuts(pObj) == NULL );
673  pObj->nCuts = p->pPars->nCutsMax;
674  // create the cutset of the node
675  pCutSet = (Dar_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
676  memset( pCutSet, 0, p->pPars->nCutsMax * sizeof(Dar_Cut_t) );
677  Dar_ObjSetCuts( pObj, pCutSet );
678  Dar_ObjForEachCutAll( pObj, pCut, i )
679  pCut->fUsed = 0;
680  Vec_PtrPush( p->vCutNodes, pObj );
681  // add unit cut if needed
682  pCut = pCutSet;
683  pCut->fUsed = 1;
684  if ( Aig_ObjIsConst1(pObj) )
685  {
686  pCut->nLeaves = 0;
687  pCut->uSign = 0;
688  pCut->uTruth = 0xFFFF;
689  }
690  else
691  {
692  pCut->nLeaves = 1;
693  pCut->pLeaves[0] = pObj->Id;
694  pCut->uSign = Aig_ObjCutSign( pObj->Id );
695  pCut->uTruth = 0xAAAA;
696  }
697  pCut->Value = Dar_CutFindValue( p, pCut );
698  if ( p->nCutMemUsed < Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) )
699  p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
700  return pCutSet;
701 }
702 
703 /**Function*************************************************************
704 
705  Synopsis []
706 
707  Description []
708 
709  SideEffects []
710 
711  SeeAlso []
712 
713 ***********************************************************************/
715 {
716  Aig_Obj_t * pObj;
717  int i;
718  Dar_ObjSetCuts( Aig_ManConst1(p->pAig), NULL );
719  Vec_PtrForEachEntry( Aig_Obj_t *, p->vCutNodes, pObj, i )
720  if ( !Aig_ObjIsNone(pObj) )
721  Dar_ObjSetCuts( pObj, NULL );
722  Vec_PtrClear( p->vCutNodes );
723  Aig_MmFixedRestart( p->pMemCuts );
724  Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
725 }
726 
727 /**Function*************************************************************
728 
729  Synopsis []
730 
731  Description []
732 
733  SideEffects []
734 
735  SeeAlso []
736 
737 ***********************************************************************/
738 Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj, int fSkipTtMin )
739 {
740  Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
741  Aig_Obj_t * pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
742  Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0);
743  Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1);
744  Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut;
745  int i, k;
746 
747  assert( !Aig_IsComplement(pObj) );
748  assert( Aig_ObjIsNode(pObj) );
749  assert( Dar_ObjCuts(pObj) == NULL );
750  assert( Dar_ObjCuts(pFaninR0) != NULL );
751  assert( Dar_ObjCuts(pFaninR1) != NULL );
752 
753  // set up the first cut
754  pCutSet = Dar_ObjPrepareCuts( p, pObj );
755  // make sure fanins cuts are computed
756  Dar_ObjForEachCut( pFaninR0, pCut0, i )
757  Dar_ObjForEachCut( pFaninR1, pCut1, k )
758  {
759  p->nCutsAll++;
760  // make sure K-feasible cut exists
761  if ( Dar_WordCountOnes(pCut0->uSign | pCut1->uSign) > 4 )
762  continue;
763  // get the next cut of this node
764  pCut = Dar_CutFindFree( p, pObj );
765  // create the new cut
766  if ( !Dar_CutMerge( pCut, pCut0, pCut1 ) )
767  {
768  assert( !pCut->fUsed );
769  continue;
770  }
771  p->nCutsTried++;
772  // check dominance
773  if ( Dar_CutFilter( pObj, pCut ) )
774  {
775  assert( !pCut->fUsed );
776  continue;
777  }
778  // compute truth table
779  pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Aig_IsComplement(pFanin0), Aig_IsComplement(pFanin1) );
780 
781  // minimize support of the cut
782  if ( !fSkipTtMin && Dar_CutSuppMinimize( pCut ) )
783  {
784  int RetValue = Dar_CutFilter( pObj, pCut );
785  assert( !RetValue );
786  }
787 
788  // assign the value of the cut
789  pCut->Value = Dar_CutFindValue( p, pCut );
790  // if the cut contains removed node, do not use it
791  if ( pCut->Value == 0 )
792  {
793  p->nCutsSkipped++;
794  pCut->fUsed = 0;
795  }
796  else if ( pCut->nLeaves < 2 )
797  return pCutSet;
798  }
799  // count the number of nontrivial cuts cuts
800  Dar_ObjForEachCut( pObj, pCut, i )
801  p->nCutsUsed += pCut->fUsed;
802  // discount trivial cut
803  p->nCutsUsed--;
804  return pCutSet;
805 }
806 
807 /**Function*************************************************************
808 
809  Synopsis []
810 
811  Description []
812 
813  SideEffects []
814 
815  SeeAlso []
816 
817 ***********************************************************************/
819 {
820  if ( Dar_ObjCuts(pObj) )
821  return Dar_ObjCuts(pObj);
822  if ( Aig_ObjIsCi(pObj) )
823  return Dar_ObjPrepareCuts( p, pObj );
824  if ( Aig_ObjIsBuf(pObj) )
825  return Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
828  return Dar_ObjComputeCuts( p, pObj, 0 );
829 }
830 
831 ////////////////////////////////////////////////////////////////////////
832 /// END OF FILE ///
833 ////////////////////////////////////////////////////////////////////////
834 
835 
837 
char * memset()
static Dar_Cut_t * Dar_ObjCuts(Aig_Obj_t *pObj)
Definition: darInt.h:107
static unsigned Dar_CutTruthSwapAdjacentVars(unsigned uTruth, int iVar)
Definition: darCut.c:418
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Dar_ObjCutPrint(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: darCut.c:65
Aig_Obj_t * Aig_ObjReal_rec(Aig_Obj_t *pObj)
Definition: aigUtil.c:476
static int Dar_CutMerge(Dar_Cut_t *pCut, Dar_Cut_t *pCut0, Dar_Cut_t *pCut1)
Definition: darCut.c:359
unsigned uTruth
Definition: darInt.h:58
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition: aigMem.c:132
Dar_Cut_t * Dar_ObjComputeCuts(Dar_Man_t *p, Aig_Obj_t *pObj, int fSkipTtMin)
Definition: darCut.c:738
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static void Dar_ObjSetCuts(Aig_Obj_t *pObj, Dar_Cut_t *pCuts)
Definition: darInt.h:108
static unsigned Dar_CutTruthStretch(unsigned uTruth, int nVars, unsigned Phase)
Definition: darCut.c:470
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static unsigned Dar_CutTruthPhase(Dar_Cut_t *pCut, Dar_Cut_t *pCut1)
Definition: darCut.c:390
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
static unsigned Dar_CutTruth(Dar_Cut_t *pCut, Dar_Cut_t *pCut0, Dar_Cut_t *pCut1, int fCompl0, int fCompl1)
Definition: darCut.c:580
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
unsigned fUsed
Definition: darInt.h:61
void Dar_ManCutsRestart(Dar_Man_t *p, Aig_Obj_t *pRoot)
FUNCTION DECLARATIONS ///.
Definition: darCut.c:714
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
ABC_NAMESPACE_IMPL_START void Dar_CutPrint(Dar_Cut_t *pCut)
DECLARATIONS ///.
Definition: darCut.c:45
#define Dar_ObjForEachCutAll(pObj, pCut, i)
MACRO DEFINITIONS ///.
Definition: darInt.h:119
static int Dar_CutSuppMinimize(Dar_Cut_t *pCut)
Definition: darCut.c:600
static unsigned Dar_CutTruthShrink(unsigned uTruth, int nVars, unsigned Phase)
Definition: darCut.c:497
static unsigned Aig_ObjCutSign(unsigned ObjId)
MACRO DEFINITIONS ///.
Definition: aig.h:228
static int Dar_CutFindValue(Dar_Man_t *p, Dar_Cut_t *pCut)
Definition: darCut.c:106
Dar_Cut_t * Dar_ObjComputeCuts_rec(Dar_Man_t *p, Aig_Obj_t *pObj)
Definition: darCut.c:818
#define Dar_ObjForEachCut(pObj, pCut, i)
Definition: darInt.h:121
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
Definition: aig.h:277
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_ Dar_Man_t
INCLUDES ///.
Definition: darInt.h:51
int pLeaves[4]
Definition: darInt.h:63
unsigned Dar_CutSortVars(unsigned uTruth, int *pVars)
Definition: darCut.c:521
static int Aig_ObjIsNone(Aig_Obj_t *pObj)
Definition: aig.h:273
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
char * Aig_MmFixedEntryFetch(Aig_MmFixed_t *p)
Definition: aigMem.c:161
Definition: aig.h:69
static int Counter
void Dar_ManCutsFree(Dar_Man_t *p)
Definition: darCut.c:648
unsigned nLeaves
Definition: darInt.h:62
static int Dar_CutFilter(Aig_Obj_t *pObj, Dar_Cut_t *pCut)
Definition: darCut.c:217
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Dar_WordCountOnes(unsigned uWord)
Definition: darCut.c:86
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
int Aig_MmFixedReadMemUsage(Aig_MmFixed_t *p)
Definition: aigMem.c:271
#define Dar_CutForEachLeaf(p, pCut, pLeaf, i)
Definition: darInt.h:124
static Dar_Cut_t * Dar_CutFindFree(Dar_Man_t *p, Aig_Obj_t *pObj)
Definition: darCut.c:142
int Var
Definition: SolverTypes.h:42
void Aig_MmFixedRestart(Aig_MmFixed_t *p)
Definition: aigMem.c:232
unsigned uSign
Definition: darInt.h:57
#define assert(ex)
Definition: util_old.h:213
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Dar_Cut_t * Dar_ObjPrepareCuts(Dar_Man_t *p, Aig_Obj_t *pObj)
Definition: darCut.c:668
static int Dar_CutCheckDominance(Dar_Cut_t *pDom, Dar_Cut_t *pCut)
Definition: darCut.c:190
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
unsigned Value
Definition: darInt.h:59
static int Dar_CutMergeOrdered(Dar_Cut_t *pC, Dar_Cut_t *pC0, Dar_Cut_t *pC1)
Definition: darCut.c:267
int Id
Definition: aig.h:85
static unsigned Dar_CutTruthSwapPolarity(unsigned uTruth, int iVar)
Definition: darCut.c:442
unsigned int nRefs
Definition: aig.h:81
unsigned nCuts
Definition: aig.h:83