abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
kitDsd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [kitDsd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Computation kit.]
8 
9  Synopsis [Performs disjoint-support decomposition based on truth tables.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - Dec 6, 2006.]
16 
17  Revision [$Id: kitDsd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "kit.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Allocates the DSD manager.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
46 {
47  Kit_DsdMan_t * p;
48  p = ABC_ALLOC( Kit_DsdMan_t, 1 );
49  memset( p, 0, sizeof(Kit_DsdMan_t) );
50  p->nVars = nVars;
51  p->nWords = Kit_TruthWordNum( p->nVars );
52  p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
53  p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
54  p->dd = Cloud_Init( 16, 14 );
55  p->vTtBdds = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
56  p->vNodes = Vec_IntAlloc( 512 );
57  return p;
58 }
59 
60 /**Function*************************************************************
61 
62  Synopsis [Deallocates the DSD manager.]
63 
64  Description []
65 
66  SideEffects []
67 
68  SeeAlso []
69 
70 ***********************************************************************/
71 void Kit_DsdManFree( Kit_DsdMan_t * p )
72 {
73  Cloud_Quit( p->dd );
74  Vec_IntFree( p->vNodes );
75  Vec_PtrFree( p->vTtBdds );
76  Vec_PtrFree( p->vTtElems );
77  Vec_PtrFree( p->vTtNodes );
78  ABC_FREE( p );
79 }
80 
81 /**Function*************************************************************
82 
83  Synopsis [Allocates the DSD node.]
84 
85  Description []
86 
87  SideEffects []
88 
89  SeeAlso []
90 
91 ***********************************************************************/
92 Kit_DsdObj_t * Kit_DsdObjAlloc( Kit_DsdNtk_t * pNtk, Kit_Dsd_t Type, int nFans )
93 {
94  Kit_DsdObj_t * pObj;
95  int nSize = sizeof(Kit_DsdObj_t) + sizeof(unsigned) * (Kit_DsdObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans));
96  pObj = (Kit_DsdObj_t *)ABC_ALLOC( char, nSize );
97  memset( pObj, 0, nSize );
98  pObj->Id = pNtk->nVars + pNtk->nNodes;
99  pObj->Type = Type;
100  pObj->nFans = nFans;
101  pObj->Offset = Kit_DsdObjOffset( nFans );
102  // add the object
103  if ( pNtk->nNodes == pNtk->nNodesAlloc )
104  {
105  pNtk->nNodesAlloc *= 2;
106  pNtk->pNodes = ABC_REALLOC( Kit_DsdObj_t *, pNtk->pNodes, pNtk->nNodesAlloc );
107  }
108  assert( pNtk->nNodes < pNtk->nNodesAlloc );
109  pNtk->pNodes[pNtk->nNodes++] = pObj;
110  return pObj;
111 }
112 
113 /**Function*************************************************************
114 
115  Synopsis [Deallocates the DSD node.]
116 
117  Description []
118 
119  SideEffects []
120 
121  SeeAlso []
122 
123 ***********************************************************************/
124 void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj )
125 {
126  ABC_FREE( pObj );
127 }
128 
129 /**Function*************************************************************
130 
131  Synopsis [Allocates the DSD network.]
132 
133  Description []
134 
135  SideEffects []
136 
137  SeeAlso []
138 
139 ***********************************************************************/
140 Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars )
141 {
142  Kit_DsdNtk_t * pNtk;
143  pNtk = ABC_ALLOC( Kit_DsdNtk_t, 1 );
144  memset( pNtk, 0, sizeof(Kit_DsdNtk_t) );
145  pNtk->pNodes = ABC_ALLOC( Kit_DsdObj_t *, nVars+1 );
146  pNtk->nVars = nVars;
147  pNtk->nNodesAlloc = nVars+1;
148  pNtk->pMem = ABC_ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) );
149  return pNtk;
150 }
151 
152 /**Function*************************************************************
153 
154  Synopsis [Deallocate the DSD network.]
155 
156  Description []
157 
158  SideEffects []
159 
160  SeeAlso []
161 
162 ***********************************************************************/
163 void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
164 {
165  Kit_DsdObj_t * pObj;
166  unsigned i;
167  Kit_DsdNtkForEachObj( pNtk, pObj, i )
168  ABC_FREE( pObj );
169  ABC_FREE( pNtk->pSupps );
170  ABC_FREE( pNtk->pNodes );
171  ABC_FREE( pNtk->pMem );
172  ABC_FREE( pNtk );
173 }
174 
175 /**Function*************************************************************
176 
177  Synopsis [Prints the hex unsigned into a file.]
178 
179  Description []
180 
181  SideEffects []
182 
183  SeeAlso []
184 
185 ***********************************************************************/
186 void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans )
187 {
188  int nDigits, Digit, k;
189  nDigits = (1 << nFans) / 4;
190  for ( k = nDigits - 1; k >= 0; k-- )
191  {
192  Digit = ((pTruth[k/8] >> ((k%8) * 4)) & 15);
193  if ( Digit < 10 )
194  fprintf( pFile, "%d", Digit );
195  else
196  fprintf( pFile, "%c", 'A' + Digit-10 );
197  }
198 }
199 
200 /**Function*************************************************************
201 
202  Synopsis [Prints the hex unsigned into a file.]
203 
204  Description []
205 
206  SideEffects []
207 
208  SeeAlso []
209 
210 ***********************************************************************/
211 char * Kit_DsdWriteHex( char * pBuff, unsigned * pTruth, int nFans )
212 {
213  int nDigits, Digit, k;
214  nDigits = (1 << nFans) / 4;
215  for ( k = nDigits - 1; k >= 0; k-- )
216  {
217  Digit = ((pTruth[k/8] >> ((k%8) * 4)) & 15);
218  if ( Digit < 10 )
219  *pBuff++ = '0' + Digit;
220  else
221  *pBuff++ = 'A' + Digit-10;
222  }
223  return pBuff;
224 }
225 
226 /**Function*************************************************************
227 
228  Synopsis [Recursively print the DSD formula.]
229 
230  Description []
231 
232  SideEffects []
233 
234  SeeAlso []
235 
236 ***********************************************************************/
237 void Kit_DsdPrint2_rec( FILE * pFile, Kit_DsdNtk_t * pNtk, int Id )
238 {
239  Kit_DsdObj_t * pObj;
240  unsigned iLit, i;
241  char Symbol;
242 
243  pObj = Kit_DsdNtkObj( pNtk, Id );
244  if ( pObj == NULL )
245  {
246  assert( Id < pNtk->nVars );
247  fprintf( pFile, "%c", 'a' + Id );
248  return;
249  }
250 
251  if ( pObj->Type == KIT_DSD_CONST1 )
252  {
253  assert( pObj->nFans == 0 );
254  fprintf( pFile, "Const1" );
255  return;
256  }
257 
258  if ( pObj->Type == KIT_DSD_VAR )
259  assert( pObj->nFans == 1 );
260 
261  if ( pObj->Type == KIT_DSD_AND )
262  Symbol = '*';
263  else if ( pObj->Type == KIT_DSD_XOR )
264  Symbol = '+';
265  else
266  Symbol = ',';
267 
268  if ( pObj->Type == KIT_DSD_PRIME )
269  fprintf( pFile, "[" );
270  else
271  fprintf( pFile, "(" );
272  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
273  {
274  if ( Abc_LitIsCompl(iLit) )
275  fprintf( pFile, "!" );
276  Kit_DsdPrint2_rec( pFile, pNtk, Abc_Lit2Var(iLit) );
277  if ( i < pObj->nFans - 1 )
278  fprintf( pFile, "%c", Symbol );
279  }
280  if ( pObj->Type == KIT_DSD_PRIME )
281  fprintf( pFile, "]" );
282  else
283  fprintf( pFile, ")" );
284 }
285 
286 /**Function*************************************************************
287 
288  Synopsis [Print the DSD formula.]
289 
290  Description []
291 
292  SideEffects []
293 
294  SeeAlso []
295 
296 ***********************************************************************/
297 void Kit_DsdPrint2( FILE * pFile, Kit_DsdNtk_t * pNtk )
298 {
299 // fprintf( pFile, "F = " );
300  if ( Abc_LitIsCompl(pNtk->Root) )
301  fprintf( pFile, "!" );
302  Kit_DsdPrint2_rec( pFile, pNtk, Abc_Lit2Var(pNtk->Root) );
303 // fprintf( pFile, "\n" );
304 }
305 
306 /**Function*************************************************************
307 
308  Synopsis [Recursively print the DSD formula.]
309 
310  Description []
311 
312  SideEffects []
313 
314  SeeAlso []
315 
316 ***********************************************************************/
317 void Kit_DsdPrint_rec( FILE * pFile, Kit_DsdNtk_t * pNtk, int Id )
318 {
319  Kit_DsdObj_t * pObj;
320  unsigned iLit, i;
321  char Symbol;
322 
323  pObj = Kit_DsdNtkObj( pNtk, Id );
324  if ( pObj == NULL )
325  {
326  assert( Id < pNtk->nVars );
327  fprintf( pFile, "%c", 'a' + Id );
328  return;
329  }
330 
331  if ( pObj->Type == KIT_DSD_CONST1 )
332  {
333  assert( pObj->nFans == 0 );
334  fprintf( pFile, "Const1" );
335  return;
336  }
337 
338  if ( pObj->Type == KIT_DSD_VAR )
339  assert( pObj->nFans == 1 );
340 
341  if ( pObj->Type == KIT_DSD_AND )
342  Symbol = '*';
343  else if ( pObj->Type == KIT_DSD_XOR )
344  Symbol = '+';
345  else
346  Symbol = ',';
347 
348  if ( pObj->Type == KIT_DSD_PRIME )
349  Kit_DsdPrintHex( pFile, Kit_DsdObjTruth(pObj), pObj->nFans );
350 
351  fprintf( pFile, "(" );
352  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
353  {
354  if ( Abc_LitIsCompl(iLit) )
355  fprintf( pFile, "!" );
356  Kit_DsdPrint_rec( pFile, pNtk, Abc_Lit2Var(iLit) );
357  if ( i < pObj->nFans - 1 )
358  fprintf( pFile, "%c", Symbol );
359  }
360  fprintf( pFile, ")" );
361 }
362 
363 /**Function*************************************************************
364 
365  Synopsis [Print the DSD formula.]
366 
367  Description []
368 
369  SideEffects []
370 
371  SeeAlso []
372 
373 ***********************************************************************/
374 void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
375 {
376  fprintf( pFile, "F = " );
377  if ( Abc_LitIsCompl(pNtk->Root) )
378  fprintf( pFile, "!" );
379  Kit_DsdPrint_rec( pFile, pNtk, Abc_Lit2Var(pNtk->Root) );
380 // fprintf( pFile, "\n" );
381 }
382 
383 /**Function*************************************************************
384 
385  Synopsis [Recursively print the DSD formula.]
386 
387  Description []
388 
389  SideEffects []
390 
391  SeeAlso []
392 
393 ***********************************************************************/
394 char * Kit_DsdWrite_rec( char * pBuff, Kit_DsdNtk_t * pNtk, int Id )
395 {
396  Kit_DsdObj_t * pObj;
397  unsigned iLit, i;
398  char Symbol;
399 
400  pObj = Kit_DsdNtkObj( pNtk, Id );
401  if ( pObj == NULL )
402  {
403  assert( Id < pNtk->nVars );
404  *pBuff++ = 'a' + Id;
405  return pBuff;
406  }
407 
408  if ( pObj->Type == KIT_DSD_CONST1 )
409  {
410  assert( pObj->nFans == 0 );
411  sprintf( pBuff, "%s", "Const1" );
412  return pBuff + strlen("Const1");
413  }
414 
415  if ( pObj->Type == KIT_DSD_VAR )
416  assert( pObj->nFans == 1 );
417 
418  if ( pObj->Type == KIT_DSD_AND )
419  Symbol = '*';
420  else if ( pObj->Type == KIT_DSD_XOR )
421  Symbol = '+';
422  else
423  Symbol = ',';
424 
425  if ( pObj->Type == KIT_DSD_PRIME )
426  pBuff = Kit_DsdWriteHex( pBuff, Kit_DsdObjTruth(pObj), pObj->nFans );
427 
428  *pBuff++ = '(';
429  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
430  {
431  if ( Abc_LitIsCompl(iLit) )
432  *pBuff++ = '!';
433  pBuff = Kit_DsdWrite_rec( pBuff, pNtk, Abc_Lit2Var(iLit) );
434  if ( i < pObj->nFans - 1 )
435  *pBuff++ = Symbol;
436  }
437  *pBuff++ = ')';
438  return pBuff;
439 }
440 
441 /**Function*************************************************************
442 
443  Synopsis [Print the DSD formula.]
444 
445  Description []
446 
447  SideEffects []
448 
449  SeeAlso []
450 
451 ***********************************************************************/
452 void Kit_DsdWrite( char * pBuff, Kit_DsdNtk_t * pNtk )
453 {
454  if ( Abc_LitIsCompl(pNtk->Root) )
455  *pBuff++ = '!';
456  pBuff = Kit_DsdWrite_rec( pBuff, pNtk, Abc_Lit2Var(pNtk->Root) );
457  *pBuff = 0;
458 }
459 
460 /**Function*************************************************************
461 
462  Synopsis [Print the DSD formula.]
463 
464  Description []
465 
466  SideEffects []
467 
468  SeeAlso []
469 
470 ***********************************************************************/
471 void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
472 {
473  Kit_DsdNtk_t * pTemp;
474  pTemp = Kit_DsdExpand( pNtk );
475  Kit_DsdPrint( stdout, pTemp );
476  Kit_DsdNtkFree( pTemp );
477 }
478 
479 /**Function*************************************************************
480 
481  Synopsis [Print the DSD formula.]
482 
483  Description []
484 
485  SideEffects []
486 
487  SeeAlso []
488 
489 ***********************************************************************/
490 void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
491 {
492  Kit_DsdNtk_t * pTemp, * pTemp2;
493 // pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
494  pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
495 // Kit_DsdPrintExpanded( pTemp );
496  pTemp2 = Kit_DsdExpand( pTemp );
497  Kit_DsdPrint( stdout, pTemp2 );
498  Kit_DsdVerify( pTemp2, pTruth, nVars );
499  Kit_DsdNtkFree( pTemp2 );
500  Kit_DsdNtkFree( pTemp );
501 }
502 
503 /**Function*************************************************************
504 
505  Synopsis [Print the DSD formula.]
506 
507  Description []
508 
509  SideEffects []
510 
511  SeeAlso []
512 
513 ***********************************************************************/
514 void Kit_DsdPrintFromTruth2( FILE * pFile, unsigned * pTruth, int nVars )
515 {
516  Kit_DsdNtk_t * pTemp, * pTemp2;
517  pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 0 );
518  pTemp2 = Kit_DsdExpand( pTemp );
519  Kit_DsdPrint2( pFile, pTemp2 );
520  Kit_DsdVerify( pTemp2, pTruth, nVars );
521  Kit_DsdNtkFree( pTemp2 );
522  Kit_DsdNtkFree( pTemp );
523 }
524 
525 /**Function*************************************************************
526 
527  Synopsis [Print the DSD formula.]
528 
529  Description []
530 
531  SideEffects []
532 
533  SeeAlso []
534 
535 ***********************************************************************/
536 void Kit_DsdWriteFromTruth( char * pBuffer, unsigned * pTruth, int nVars )
537 {
538  Kit_DsdNtk_t * pTemp, * pTemp2;
539 // pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
540  pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
541 // Kit_DsdPrintExpanded( pTemp );
542  pTemp2 = Kit_DsdExpand( pTemp );
543  Kit_DsdWrite( pBuffer, pTemp2 );
544  Kit_DsdVerify( pTemp2, pTruth, nVars );
545  Kit_DsdNtkFree( pTemp2 );
546  Kit_DsdNtkFree( pTemp );
547 }
548 
549 /**Function*************************************************************
550 
551  Synopsis [Derives the truth table of the DSD node.]
552 
553  Description []
554 
555  SideEffects []
556 
557  SeeAlso []
558 
559 ***********************************************************************/
560 unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id )
561 {
562  Kit_DsdObj_t * pObj;
563  unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
564  unsigned i, iLit, fCompl;
565 // unsigned m, nMints, * pTruthPrime, * pTruthMint;
566 
567  // get the node with this ID
568  pObj = Kit_DsdNtkObj( pNtk, Id );
569  pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
570 
571  // special case: literal of an internal node
572  if ( pObj == NULL )
573  {
574  assert( Id < pNtk->nVars );
575  return pTruthRes;
576  }
577 
578  // constant node
579  if ( pObj->Type == KIT_DSD_CONST1 )
580  {
581  assert( pObj->nFans == 0 );
582  Kit_TruthFill( pTruthRes, pNtk->nVars );
583  return pTruthRes;
584  }
585 
586  // elementary variable node
587  if ( pObj->Type == KIT_DSD_VAR )
588  {
589  assert( pObj->nFans == 1 );
590  iLit = pObj->pFans[0];
591  pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Abc_Lit2Var(iLit) );
592  if ( Abc_LitIsCompl(iLit) )
593  Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
594  else
595  Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars );
596  return pTruthRes;
597  }
598 
599  // collect the truth tables of the fanins
600  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
601  pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Abc_Lit2Var(iLit) );
602  // create the truth table
603 
604  // simple gates
605  if ( pObj->Type == KIT_DSD_AND )
606  {
607  Kit_TruthFill( pTruthRes, pNtk->nVars );
608  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
609  Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
610  return pTruthRes;
611  }
612  if ( pObj->Type == KIT_DSD_XOR )
613  {
614  Kit_TruthClear( pTruthRes, pNtk->nVars );
615  fCompl = 0;
616  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
617  {
618  Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
619  fCompl ^= Abc_LitIsCompl(iLit);
620  }
621  if ( fCompl )
622  Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
623  return pTruthRes;
624  }
625  assert( pObj->Type == KIT_DSD_PRIME );
626 /*
627  // get the truth table of the prime node
628  pTruthPrime = Kit_DsdObjTruth( pObj );
629  // get storage for the temporary minterm
630  pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
631  // go through the minterms
632  nMints = (1 << pObj->nFans);
633  Kit_TruthClear( pTruthRes, pNtk->nVars );
634  for ( m = 0; m < nMints; m++ )
635  {
636  if ( !Kit_TruthHasBit(pTruthPrime, m) )
637  continue;
638  Kit_TruthFill( pTruthMint, pNtk->nVars );
639  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
640  Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Abc_LitIsCompl(iLit) );
641  Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
642  }
643 */
644  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
645  if ( Abc_LitIsCompl(iLit) )
646  Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
647  pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
648  Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
649  return pTruthRes;
650 }
651 
652 /**Function*************************************************************
653 
654  Synopsis [Derives the truth table of the DSD network.]
655 
656  Description []
657 
658  SideEffects []
659 
660  SeeAlso []
661 
662 ***********************************************************************/
663 unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
664 {
665  unsigned * pTruthRes;
666  int i;
667  // assign elementary truth ables
668  assert( pNtk->nVars <= p->nVars );
669  for ( i = 0; i < (int)pNtk->nVars; i++ )
670  Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
671  // compute truth table for each node
672  pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Abc_Lit2Var(pNtk->Root) );
673  // complement the truth table if needed
674  if ( Abc_LitIsCompl(pNtk->Root) )
675  Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
676  return pTruthRes;
677 }
678 
679 /**Function*************************************************************
680 
681  Synopsis [Derives the truth table of the DSD node.]
682 
683  Description []
684 
685  SideEffects []
686 
687  SeeAlso []
688 
689 ***********************************************************************/
690 unsigned * Kit_DsdTruthComputeNodeOne_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
691 {
692  Kit_DsdObj_t * pObj;
693  unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
694  unsigned i, iLit, fCompl, nPartial = 0;
695 // unsigned m, nMints, * pTruthPrime, * pTruthMint;
696 
697  // get the node with this ID
698  pObj = Kit_DsdNtkObj( pNtk, Id );
699  pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
700 
701  // special case: literal of an internal node
702  if ( pObj == NULL )
703  {
704  assert( Id < pNtk->nVars );
705  assert( !uSupp || uSupp != (uSupp & ~(1<<Id)) );
706  return pTruthRes;
707  }
708 
709  // constant node
710  if ( pObj->Type == KIT_DSD_CONST1 )
711  {
712  assert( pObj->nFans == 0 );
713  Kit_TruthFill( pTruthRes, pNtk->nVars );
714  return pTruthRes;
715  }
716 
717  // elementary variable node
718  if ( pObj->Type == KIT_DSD_VAR )
719  {
720  assert( pObj->nFans == 1 );
721  iLit = pObj->pFans[0];
722  assert( Kit_DsdLitIsLeaf( pNtk, iLit ) );
723  pTruthFans[0] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), uSupp );
724  if ( Abc_LitIsCompl(iLit) )
725  Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
726  else
727  Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars );
728  return pTruthRes;
729  }
730 
731  // collect the truth tables of the fanins
732  if ( uSupp )
733  {
734  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
735  if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) )
736  pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), uSupp );
737  else
738  {
739  pTruthFans[i] = NULL;
740  nPartial = 1;
741  }
742  }
743  else
744  {
745  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
746  pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), uSupp );
747  }
748  // create the truth table
749 
750  // simple gates
751  if ( pObj->Type == KIT_DSD_AND )
752  {
753  Kit_TruthFill( pTruthRes, pNtk->nVars );
754  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
755  if ( pTruthFans[i] )
756  Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
757  return pTruthRes;
758  }
759  if ( pObj->Type == KIT_DSD_XOR )
760  {
761  Kit_TruthClear( pTruthRes, pNtk->nVars );
762  fCompl = 0;
763  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
764  {
765  if ( pTruthFans[i] )
766  {
767  Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
768  fCompl ^= Abc_LitIsCompl(iLit);
769  }
770  }
771  if ( fCompl )
772  Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
773  return pTruthRes;
774  }
775  assert( pObj->Type == KIT_DSD_PRIME );
776 
777  if ( uSupp && nPartial )
778  {
779  // find the only non-empty component
780  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
781  if ( pTruthFans[i] )
782  break;
783  assert( i < pObj->nFans );
784  return pTruthFans[i];
785  }
786 /*
787  // get the truth table of the prime node
788  pTruthPrime = Kit_DsdObjTruth( pObj );
789  // get storage for the temporary minterm
790  pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
791  // go through the minterms
792  nMints = (1 << pObj->nFans);
793  Kit_TruthClear( pTruthRes, pNtk->nVars );
794  for ( m = 0; m < nMints; m++ )
795  {
796  if ( !Kit_TruthHasBit(pTruthPrime, m) )
797  continue;
798  Kit_TruthFill( pTruthMint, pNtk->nVars );
799  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
800  Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Abc_LitIsCompl(iLit) );
801  Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
802  }
803 */
804  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
805  if ( Abc_LitIsCompl(iLit) )
806  Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
807  pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
808  Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
809  return pTruthRes;
810 }
811 
812 /**Function*************************************************************
813 
814  Synopsis [Derives the truth table of the DSD network.]
815 
816  Description []
817 
818  SideEffects []
819 
820  SeeAlso []
821 
822 ***********************************************************************/
823 unsigned * Kit_DsdTruthComputeOne( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp )
824 {
825  unsigned * pTruthRes;
826  int i;
827  // if support is specified, request that supports are available
828  if ( uSupp )
829  Kit_DsdGetSupports( pNtk );
830  // assign elementary truth tables
831  assert( pNtk->nVars <= p->nVars );
832  for ( i = 0; i < (int)pNtk->nVars; i++ )
833  Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
834  // compute truth table for each node
835  pTruthRes = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(pNtk->Root), uSupp );
836  // complement the truth table if needed
837  if ( Abc_LitIsCompl(pNtk->Root) )
838  Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
839  return pTruthRes;
840 }
841 
842 /**Function*************************************************************
843 
844  Synopsis [Derives the truth table of the DSD node.]
845 
846  Description []
847 
848  SideEffects []
849 
850  SeeAlso []
851 
852 ***********************************************************************/
853 unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp, int iVar, unsigned * pTruthDec )
854 {
855  Kit_DsdObj_t * pObj;
856  int pfBoundSet[16];
857  unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
858  unsigned i, iLit, fCompl, nPartial, uSuppFan, uSuppCur;
859 // unsigned m, nMints, * pTruthPrime, * pTruthMint;
860  assert( uSupp > 0 );
861 
862  // get the node with this ID
863  pObj = Kit_DsdNtkObj( pNtk, Id );
864  pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
865  if ( pObj == NULL )
866  {
867  assert( Id < pNtk->nVars );
868  return pTruthRes;
869  }
870  assert( pObj->Type != KIT_DSD_CONST1 );
871  assert( pObj->Type != KIT_DSD_VAR );
872 
873  // count the number of intersecting fanins
874  // collect the total support of the intersecting fanins
875  nPartial = 0;
876  uSuppFan = 0;
877  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
878  {
879  uSuppCur = Kit_DsdLitSupport(pNtk, iLit);
880  if ( uSupp & uSuppCur )
881  {
882  nPartial++;
883  uSuppFan |= uSuppCur;
884  }
885  }
886 
887  // if there is no intersection, or full intersection, use simple procedure
888  if ( nPartial == 0 || nPartial == pObj->nFans )
889  return Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Id, 0 );
890 
891  // if support of the component includes some other variables
892  // we need to continue constructing it as usual by the two-function procedure
893  if ( uSuppFan != (uSuppFan & uSupp) )
894  {
895  assert( nPartial == 1 );
896 // return Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Id, uSupp, iVar, pTruthDec );
897  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
898  {
899  if ( uSupp & Kit_DsdLitSupport(pNtk, iLit) )
900  pTruthFans[i] = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Abc_Lit2Var(iLit), uSupp, iVar, pTruthDec );
901  else
902  pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), 0 );
903  }
904 
905  // create composition/decomposition functions
906  if ( pObj->Type == KIT_DSD_AND )
907  {
908  Kit_TruthFill( pTruthRes, pNtk->nVars );
909  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
910  Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
911  return pTruthRes;
912  }
913  if ( pObj->Type == KIT_DSD_XOR )
914  {
915  Kit_TruthClear( pTruthRes, pNtk->nVars );
916  fCompl = 0;
917  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
918  {
919  fCompl ^= Abc_LitIsCompl(iLit);
920  Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
921  }
922  if ( fCompl )
923  Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
924  return pTruthRes;
925  }
926  assert( pObj->Type == KIT_DSD_PRIME );
927  }
928  else
929  {
930  assert( uSuppFan == (uSuppFan & uSupp) );
931  assert( nPartial < pObj->nFans );
932  // the support of the insecting component(s) is contained in the bound-set
933  // and yet there are components that are not contained in the bound set
934 
935  // solve the fanins and collect info, which components belong to the bound set
936  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
937  {
938  pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), 0 );
939  pfBoundSet[i] = (int)((uSupp & Kit_DsdLitSupport(pNtk, iLit)) > 0);
940  }
941 
942  // create composition/decomposition functions
943  if ( pObj->Type == KIT_DSD_AND )
944  {
945  Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
946  Kit_TruthFill( pTruthDec, pNtk->nVars );
947  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
948  if ( pfBoundSet[i] )
949  Kit_TruthAndPhase( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
950  else
951  Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
952  return pTruthRes;
953  }
954  if ( pObj->Type == KIT_DSD_XOR )
955  {
956  Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
957  Kit_TruthClear( pTruthDec, pNtk->nVars );
958  fCompl = 0;
959  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
960  {
961  fCompl ^= Abc_LitIsCompl(iLit);
962  if ( pfBoundSet[i] )
963  Kit_TruthXor( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars );
964  else
965  Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
966  }
967  if ( fCompl )
968  Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
969  return pTruthRes;
970  }
971  assert( pObj->Type == KIT_DSD_PRIME );
972  assert( nPartial == 1 );
973 
974  // find the only non-empty component
975  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
976  if ( pfBoundSet[i] )
977  break;
978  assert( i < pObj->nFans );
979 
980  // save this component as the decomposed function
981  Kit_TruthCopy( pTruthDec, pTruthFans[i], pNtk->nVars );
982  // set the corresponding component to be the new variable
983  Kit_TruthIthVar( pTruthFans[i], pNtk->nVars, iVar );
984  }
985 /*
986  // get the truth table of the prime node
987  pTruthPrime = Kit_DsdObjTruth( pObj );
988  // get storage for the temporary minterm
989  pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
990  // go through the minterms
991  nMints = (1 << pObj->nFans);
992  Kit_TruthClear( pTruthRes, pNtk->nVars );
993  for ( m = 0; m < nMints; m++ )
994  {
995  if ( !Kit_TruthHasBit(pTruthPrime, m) )
996  continue;
997  Kit_TruthFill( pTruthMint, pNtk->nVars );
998  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
999  Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Abc_LitIsCompl(iLit) );
1000  Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
1001  }
1002 */
1003 // Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1004 // assert( !Abc_LitIsCompl(iLit) );
1005  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1006  if ( Abc_LitIsCompl(iLit) )
1007  Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
1008  pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
1009  Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
1010  return pTruthRes;
1011 }
1012 
1013 /**Function*************************************************************
1014 
1015  Synopsis [Derives the truth table of the DSD network.]
1016 
1017  Description []
1018 
1019  SideEffects []
1020 
1021  SeeAlso []
1022 
1023 ***********************************************************************/
1024 unsigned * Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthDec )
1025 {
1026  unsigned * pTruthRes, uSuppAll;
1027  int i;
1028  assert( uSupp > 0 );
1029  assert( pNtk->nVars <= p->nVars );
1030  // compute support of all nodes
1031  uSuppAll = Kit_DsdGetSupports( pNtk );
1032  // consider special case - there is no overlap
1033  if ( (uSupp & uSuppAll) == 0 )
1034  {
1035  Kit_TruthClear( pTruthDec, pNtk->nVars );
1036  return Kit_DsdTruthCompute( p, pNtk );
1037  }
1038  // consider special case - support is fully contained
1039  if ( (uSupp & uSuppAll) == uSuppAll )
1040  {
1041  pTruthRes = Kit_DsdTruthCompute( p, pNtk );
1042  Kit_TruthCopy( pTruthDec, pTruthRes, pNtk->nVars );
1043  Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
1044  return pTruthRes;
1045  }
1046  // assign elementary truth tables
1047  for ( i = 0; i < (int)pNtk->nVars; i++ )
1048  Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
1049  // compute truth table for each node
1050  pTruthRes = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Abc_Lit2Var(pNtk->Root), uSupp, iVar, pTruthDec );
1051  // complement the truth table if needed
1052  if ( Abc_LitIsCompl(pNtk->Root) )
1053  Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
1054  return pTruthRes;
1055 }
1056 
1057 /**Function*************************************************************
1058 
1059  Synopsis [Derives the truth table of the DSD network.]
1060 
1061  Description []
1062 
1063  SideEffects []
1064 
1065  SeeAlso []
1066 
1067 ***********************************************************************/
1068 void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
1069 {
1070  Kit_DsdMan_t * p;
1071  unsigned * pTruth;
1072  p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
1073  pTruth = Kit_DsdTruthCompute( p, pNtk );
1074  Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
1075  Kit_DsdManFree( p );
1076 }
1077 
1078 /**Function*************************************************************
1079 
1080  Synopsis [Derives the truth table of the DSD network.]
1081 
1082  Description []
1083 
1084  SideEffects []
1085 
1086  SeeAlso []
1087 
1088 ***********************************************************************/
1089 void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec )
1090 {
1091  unsigned * pTruth = Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar, pTruthDec );
1092  if ( pTruthCo )
1093  Kit_TruthCopy( pTruthCo, pTruth, pNtk->nVars );
1094 }
1095 
1096 /**Function*************************************************************
1097 
1098  Synopsis [Derives the truth table of the DSD network.]
1099 
1100  Description []
1101 
1102  SideEffects []
1103 
1104  SeeAlso []
1105 
1106 ***********************************************************************/
1107 void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
1108 {
1109  unsigned * pTruth = Kit_DsdTruthComputeOne( p, pNtk, uSupp );
1110  Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
1111 /*
1112  // verification
1113  {
1114  // compute the same function using different procedure
1115  unsigned * pTruthTemp = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes + 1);
1116  pNtk->pSupps = NULL;
1117  Kit_DsdTruthComputeTwo( p, pNtk, uSupp, -1, pTruthTemp );
1118 // if ( !Kit_TruthIsEqual( pTruthTemp, pTruthRes, pNtk->nVars ) )
1119  if ( !Kit_TruthIsEqualWithPhase( pTruthTemp, pTruthRes, pNtk->nVars ) )
1120  {
1121  printf( "Verification FAILED!\n" );
1122  Kit_DsdPrint( stdout, pNtk );
1123  Kit_DsdPrintFromTruth( pTruthRes, pNtk->nVars );
1124  Kit_DsdPrintFromTruth( pTruthTemp, pNtk->nVars );
1125  }
1126 // else
1127 // printf( "Verification successful.\n" );
1128  }
1129 */
1130 }
1131 
1132 /**Function*************************************************************
1133 
1134  Synopsis [Counts the number of blocks of the given number of inputs.]
1135 
1136  Description []
1137 
1138  SideEffects []
1139 
1140  SeeAlso []
1141 
1142 ***********************************************************************/
1143 int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCounter )
1144 {
1145  Kit_DsdObj_t * pObj;
1146  unsigned iLit, i, Res0, Res1;
1147  pObj = Kit_DsdNtkObj( pNtk, Id );
1148  if ( pObj == NULL )
1149  return 0;
1150  if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
1151  {
1152  assert( pObj->nFans == 2 );
1153  Res0 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Abc_Lit2Var(pObj->pFans[0]), pCounter );
1154  Res1 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Abc_Lit2Var(pObj->pFans[1]), pCounter );
1155  if ( Res0 == 0 && Res1 > 0 )
1156  return Res1 - 1;
1157  if ( Res0 > 0 && Res1 == 0 )
1158  return Res0 - 1;
1159  (*pCounter)++;
1160  return nLutSize - 2;
1161  }
1162  assert( pObj->Type == KIT_DSD_PRIME );
1163  if ( (int)pObj->nFans > nLutSize ) //+ 1 )
1164  {
1165  *pCounter = 1000;
1166  return 0;
1167  }
1168  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1169  Kit_DsdCountLuts_rec( pNtk, nLutSize, Abc_Lit2Var(iLit), pCounter );
1170  (*pCounter)++;
1171 // if ( (int)pObj->nFans == nLutSize + 1 )
1172 // (*pCounter)++;
1173  return nLutSize - pObj->nFans;
1174 }
1175 
1176 /**Function*************************************************************
1177 
1178  Synopsis [Counts the number of blocks of the given number of inputs.]
1179 
1180  Description []
1181 
1182  SideEffects []
1183 
1184  SeeAlso []
1185 
1186 ***********************************************************************/
1187 int Kit_DsdCountLuts( Kit_DsdNtk_t * pNtk, int nLutSize )
1188 {
1189  int Counter = 0;
1190  if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_CONST1 )
1191  return 0;
1192  if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_VAR )
1193  return 0;
1194  Kit_DsdCountLuts_rec( pNtk, nLutSize, Abc_Lit2Var(pNtk->Root), &Counter );
1195  if ( Counter >= 1000 )
1196  return -1;
1197  return Counter;
1198 }
1199 
1200 /**Function*************************************************************
1201 
1202  Synopsis [Returns the size of the largest non-DSD block.]
1203 
1204  Description []
1205 
1206  SideEffects []
1207 
1208  SeeAlso []
1209 
1210 ***********************************************************************/
1211 int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk )
1212 {
1213  Kit_DsdObj_t * pObj;
1214  unsigned i, nSizeMax = 0;
1215  Kit_DsdNtkForEachObj( pNtk, pObj, i )
1216  {
1217  if ( pObj->Type != KIT_DSD_PRIME )
1218  continue;
1219  if ( nSizeMax < pObj->nFans )
1220  nSizeMax = pObj->nFans;
1221  }
1222  return nSizeMax;
1223 }
1224 
1225 /**Function*************************************************************
1226 
1227  Synopsis [Returns the largest non-DSD block.]
1228 
1229  Description []
1230 
1231  SideEffects []
1232 
1233  SeeAlso []
1234 
1235 ***********************************************************************/
1236 Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk )
1237 {
1238  Kit_DsdObj_t * pObj, * pObjMax = NULL;
1239  unsigned i, nSizeMax = 0;
1240  Kit_DsdNtkForEachObj( pNtk, pObj, i )
1241  {
1242  if ( pObj->Type != KIT_DSD_PRIME )
1243  continue;
1244  if ( nSizeMax < pObj->nFans )
1245  {
1246  nSizeMax = pObj->nFans;
1247  pObjMax = pObj;
1248  }
1249  }
1250  return pObjMax;
1251 }
1252 
1253 /**Function*************************************************************
1254 
1255  Synopsis [Finds the union of supports of the non-DSD blocks.]
1256 
1257  Description []
1258 
1259  SideEffects []
1260 
1261  SeeAlso []
1262 
1263 ***********************************************************************/
1264 unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk )
1265 {
1266  Kit_DsdObj_t * pObj;
1267  unsigned i, uSupport = 0;
1268 // ABC_FREE( pNtk->pSupps );
1269  Kit_DsdGetSupports( pNtk );
1270  Kit_DsdNtkForEachObj( pNtk, pObj, i )
1271  {
1272  if ( pObj->Type != KIT_DSD_PRIME )
1273  continue;
1274  uSupport |= Kit_DsdLitSupport( pNtk, Abc_Var2Lit(pObj->Id,0) );
1275  }
1276  return uSupport;
1277 }
1278 
1279 
1280 /**Function*************************************************************
1281 
1282  Synopsis [Expands the node.]
1283 
1284  Description [Returns the new literal.]
1285 
1286  SideEffects []
1287 
1288  SeeAlso []
1289 
1290 ***********************************************************************/
1291 void Kit_DsdExpandCollectAnd_rec( Kit_DsdNtk_t * p, unsigned iLit, unsigned * piLitsNew, int * nLitsNew )
1292 {
1293  Kit_DsdObj_t * pObj;
1294  unsigned i, iLitFanin;
1295  // check the end of the supergate
1296  pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1297  if ( Abc_LitIsCompl(iLit) || Abc_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_AND )
1298  {
1299  piLitsNew[(*nLitsNew)++] = iLit;
1300  return;
1301  }
1302  // iterate through the fanins
1303  Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
1304  Kit_DsdExpandCollectAnd_rec( p, iLitFanin, piLitsNew, nLitsNew );
1305 }
1306 
1307 /**Function*************************************************************
1308 
1309  Synopsis [Expands the node.]
1310 
1311  Description [Returns the new literal.]
1312 
1313  SideEffects []
1314 
1315  SeeAlso []
1316 
1317 ***********************************************************************/
1318 void Kit_DsdExpandCollectXor_rec( Kit_DsdNtk_t * p, unsigned iLit, unsigned * piLitsNew, int * nLitsNew )
1319 {
1320  Kit_DsdObj_t * pObj;
1321  unsigned i, iLitFanin;
1322  // check the end of the supergate
1323  pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1324  if ( Abc_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_XOR )
1325  {
1326  piLitsNew[(*nLitsNew)++] = iLit;
1327  return;
1328  }
1329  // iterate through the fanins
1330  pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1331  Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
1332  Kit_DsdExpandCollectXor_rec( p, iLitFanin, piLitsNew, nLitsNew );
1333  // if the literal was complemented, pass the complemented attribute somewhere
1334  if ( Abc_LitIsCompl(iLit) )
1335  piLitsNew[0] = Abc_LitNot( piLitsNew[0] );
1336 }
1337 
1338 /**Function*************************************************************
1339 
1340  Synopsis [Expands the node.]
1341 
1342  Description [Returns the new literal.]
1343 
1344  SideEffects []
1345 
1346  SeeAlso []
1347 
1348 ***********************************************************************/
1349 int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
1350 {
1351  unsigned * pTruth, * pTruthNew;
1352  unsigned i, iLitFanin, piLitsNew[16], nLitsNew = 0;
1353  Kit_DsdObj_t * pObj, * pObjNew;
1354 
1355  // consider the case of simple gate
1356  pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1357  if ( pObj == NULL )
1358  return iLit;
1359  if ( pObj->Type == KIT_DSD_AND )
1360  {
1361  Kit_DsdExpandCollectAnd_rec( p, Abc_LitRegular(iLit), piLitsNew, (int *)&nLitsNew );
1362  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
1363  for ( i = 0; i < pObjNew->nFans; i++ )
1364  pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
1365  return Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(iLit) );
1366  }
1367  if ( pObj->Type == KIT_DSD_XOR )
1368  {
1369  int fCompl = Abc_LitIsCompl(iLit);
1370  Kit_DsdExpandCollectXor_rec( p, Abc_LitRegular(iLit), piLitsNew, (int *)&nLitsNew );
1371  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
1372  for ( i = 0; i < pObjNew->nFans; i++ )
1373  {
1374  pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, Abc_LitRegular(piLitsNew[i]) );
1375  fCompl ^= Abc_LitIsCompl(piLitsNew[i]);
1376  }
1377  return Abc_Var2Lit( pObjNew->Id, fCompl );
1378  }
1379  assert( pObj->Type == KIT_DSD_PRIME );
1380 
1381  // create new PRIME node
1382  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
1383  // copy the truth table
1384  pTruth = Kit_DsdObjTruth( pObj );
1385  pTruthNew = Kit_DsdObjTruth( pObjNew );
1386  Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
1387  // create fanins
1388  Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
1389  {
1390  pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, iLitFanin );
1391  // complement the corresponding inputs of the truth table
1392  if ( Abc_LitIsCompl(pObjNew->pFans[i]) )
1393  {
1394  pObjNew->pFans[i] = Abc_LitRegular(pObjNew->pFans[i]);
1395  Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
1396  }
1397  }
1398 
1399  if ( pObj->nFans == 3 &&
1400  (pTruthNew[0] == 0xCACACACA || pTruthNew[0] == 0xC5C5C5C5 ||
1401  pTruthNew[0] == 0x3A3A3A3A || pTruthNew[0] == 0x35353535) )
1402  {
1403  // translate into regular MUXes
1404  if ( pTruthNew[0] == 0xC5C5C5C5 )
1405  pObjNew->pFans[0] = Abc_LitNot(pObjNew->pFans[0]);
1406  else if ( pTruthNew[0] == 0x3A3A3A3A )
1407  pObjNew->pFans[1] = Abc_LitNot(pObjNew->pFans[1]);
1408  else if ( pTruthNew[0] == 0x35353535 )
1409  {
1410  pObjNew->pFans[0] = Abc_LitNot(pObjNew->pFans[0]);
1411  pObjNew->pFans[1] = Abc_LitNot(pObjNew->pFans[1]);
1412  }
1413  pTruthNew[0] = 0xCACACACA;
1414  // resolve the complemented control input
1415  if ( Abc_LitIsCompl(pObjNew->pFans[2]) )
1416  {
1417  unsigned char Temp = pObjNew->pFans[0];
1418  pObjNew->pFans[0] = pObjNew->pFans[1];
1419  pObjNew->pFans[1] = Temp;
1420  pObjNew->pFans[2] = Abc_LitNot(pObjNew->pFans[2]);
1421  }
1422  // resolve the complemented true input
1423  if ( Abc_LitIsCompl(pObjNew->pFans[1]) )
1424  {
1425  iLit = Abc_LitNot(iLit);
1426  pObjNew->pFans[0] = Abc_LitNot(pObjNew->pFans[0]);
1427  pObjNew->pFans[1] = Abc_LitNot(pObjNew->pFans[1]);
1428  }
1429  return Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(iLit) );
1430  }
1431  else
1432  {
1433  // if the incoming phase is complemented, absorb it into the prime node
1434  if ( Abc_LitIsCompl(iLit) )
1435  Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
1436  return Abc_Var2Lit( pObjNew->Id, 0 );
1437  }
1438 }
1439 
1440 /**Function*************************************************************
1441 
1442  Synopsis [Expands the network.]
1443 
1444  Description []
1445 
1446  SideEffects []
1447 
1448  SeeAlso []
1449 
1450 ***********************************************************************/
1451 Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
1452 {
1453  Kit_DsdNtk_t * pNew;
1454  Kit_DsdObj_t * pObjNew;
1455  assert( p->nVars <= 16 );
1456  // create a new network
1457  pNew = Kit_DsdNtkAlloc( p->nVars );
1458  // consider simple special cases
1459  if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
1460  {
1461  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
1462  pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
1463  return pNew;
1464  }
1465  if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
1466  {
1467  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
1468  pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
1469  pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
1470  return pNew;
1471  }
1472  // convert the root node
1473  pNew->Root = Kit_DsdExpandNode_rec( pNew, p, p->Root );
1474  return pNew;
1475 }
1476 
1477 /**Function*************************************************************
1478 
1479  Synopsis [Sorts the literals by their support.]
1480 
1481  Description []
1482 
1483  SideEffects []
1484 
1485  SeeAlso []
1486 
1487 ***********************************************************************/
1488 void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned short * piLits, int nVars, unsigned piLitsRes[] )
1489 {
1490  int nSuppSizes[16], Priority[16], pOrder[16];
1491  int i, k, iVarBest, SuppMax, PrioMax;
1492  // compute support sizes and priorities of the components
1493  for ( i = 0; i < nVars; i++ )
1494  {
1495  assert( uSupps[i] );
1496  pOrder[i] = i;
1497  Priority[i] = KIT_INFINITY;
1498  for ( k = 0; k < 16; k++ )
1499  if ( uSupps[i] & (1 << k) )
1500  Priority[i] = KIT_MIN( Priority[i], pPrios[k] );
1501  assert( Priority[i] != 16 );
1502  nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
1503  }
1504  // sort the components by pririty
1505  Extra_BubbleSort( pOrder, Priority, nVars, 0 );
1506  // find the component by with largest size and lowest priority
1507  iVarBest = -1;
1508  SuppMax = 0;
1509  PrioMax = 0;
1510  for ( i = 0; i < nVars; i++ )
1511  {
1512  if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMax < Priority[i]) )
1513  {
1514  SuppMax = nSuppSizes[i];
1515  PrioMax = Priority[i];
1516  iVarBest = i;
1517  }
1518  }
1519  assert( iVarBest != -1 );
1520  // copy the resulting literals
1521  k = 0;
1522  piLitsRes[k++] = piLits[iVarBest];
1523  for ( i = 0; i < nVars; i++ )
1524  {
1525  if ( pOrder[i] == iVarBest )
1526  continue;
1527  piLitsRes[k++] = piLits[pOrder[i]];
1528  }
1529  assert( k == nVars );
1530 }
1531 
1532 /**Function*************************************************************
1533 
1534  Synopsis [Shrinks multi-input nodes.]
1535 
1536  Description [Takes the array of variable priorities pPrios.]
1537 
1538  SideEffects []
1539 
1540  SeeAlso []
1541 
1542 ***********************************************************************/
1543 int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPrios[] )
1544 {
1545  Kit_DsdObj_t * pObj;
1546  Kit_DsdObj_t * pObjNew = NULL; // Suppress "might be used uninitialized"
1547  unsigned * pTruth, * pTruthNew;
1548  unsigned i, piLitsNew[16], uSupps[16];
1549  int iLitFanin, iLitNew;
1550 
1551  // consider the case of simple gate
1552  pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1553  if ( pObj == NULL )
1554  return iLit;
1555  if ( pObj->Type == KIT_DSD_AND )
1556  {
1557  // get the supports
1558  Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
1559  uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
1560  // put the largest component last
1561  // sort other components in the decreasing order of priority of their vars
1562  Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
1563  // construct the two-input node network
1564  iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
1565  for ( i = 1; i < pObj->nFans; i++ )
1566  {
1567  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
1568  pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
1569  pObjNew->pFans[1] = iLitNew;
1570  iLitNew = Abc_Var2Lit( pObjNew->Id, 0 );
1571  }
1572  return Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(iLit) );
1573  }
1574  if ( pObj->Type == KIT_DSD_XOR )
1575  {
1576  // get the supports
1577  Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
1578  {
1579  assert( !Abc_LitIsCompl(iLitFanin) );
1580  uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
1581  }
1582  // put the largest component last
1583  // sort other components in the decreasing order of priority of their vars
1584  Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
1585  // construct the two-input node network
1586  iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
1587  for ( i = 1; i < pObj->nFans; i++ )
1588  {
1589  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
1590  pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
1591  pObjNew->pFans[1] = iLitNew;
1592  iLitNew = Abc_Var2Lit( pObjNew->Id, 0 );
1593  }
1594  return Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(iLit) );
1595  }
1596  assert( pObj->Type == KIT_DSD_PRIME );
1597 
1598  // create new PRIME node
1599  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
1600  // copy the truth table
1601  pTruth = Kit_DsdObjTruth( pObj );
1602  pTruthNew = Kit_DsdObjTruth( pObjNew );
1603  Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
1604  // create fanins
1605  Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
1606  {
1607  pObjNew->pFans[i] = Kit_DsdShrink_rec( pNew, p, iLitFanin, pPrios );
1608  // complement the corresponding inputs of the truth table
1609  if ( Abc_LitIsCompl(pObjNew->pFans[i]) )
1610  {
1611  pObjNew->pFans[i] = Abc_LitRegular(pObjNew->pFans[i]);
1612  Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
1613  }
1614  }
1615  // if the incoming phase is complemented, absorb it into the prime node
1616  if ( Abc_LitIsCompl(iLit) )
1617  Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
1618  return Abc_Var2Lit( pObjNew->Id, 0 );
1619 }
1620 
1621 /**Function*************************************************************
1622 
1623  Synopsis [Shrinks the network.]
1624 
1625  Description [Transforms the network to have two-input nodes so that the
1626  higher-ordered nodes were decomposed out first.]
1627 
1628  SideEffects []
1629 
1630  SeeAlso []
1631 
1632 ***********************************************************************/
1633 Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] )
1634 {
1635  Kit_DsdNtk_t * pNew;
1636  Kit_DsdObj_t * pObjNew;
1637  assert( p->nVars <= 16 );
1638  // create a new network
1639  pNew = Kit_DsdNtkAlloc( p->nVars );
1640  // consider simple special cases
1641  if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
1642  {
1643  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
1644  pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
1645  return pNew;
1646  }
1647  if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
1648  {
1649  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
1650  pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
1651  pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
1652  return pNew;
1653  }
1654  // convert the root node
1655  pNew->Root = Kit_DsdShrink_rec( pNew, p, p->Root, pPrios );
1656  return pNew;
1657 }
1658 
1659 /**Function*************************************************************
1660 
1661  Synopsis [Rotates the network.]
1662 
1663  Description [Transforms prime nodes to have the fanin with the
1664  highest frequency of supports go first.]
1665 
1666  SideEffects []
1667 
1668  SeeAlso []
1669 
1670 ***********************************************************************/
1671 void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
1672 {
1673  Kit_DsdObj_t * pObj;
1674  unsigned * pIn, * pOut, * pTemp, k;
1675  int i, v, Temp, uSuppFanin, iFaninLit, WeightMax, FaninMax, nSwaps;
1676  int Weights[16];
1677  // go through the prime nodes
1678  Kit_DsdNtkForEachObj( p, pObj, i )
1679  {
1680  if ( pObj->Type != KIT_DSD_PRIME )
1681  continue;
1682  // count the fanin frequencies
1683  Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
1684  {
1685  uSuppFanin = Kit_DsdLitSupport( p, iFaninLit );
1686  Weights[k] = 0;
1687  for ( v = 0; v < 16; v++ )
1688  if ( uSuppFanin & (1 << v) )
1689  Weights[k] += pFreqs[v] - 1;
1690  }
1691  // find the most frequent fanin
1692  WeightMax = 0;
1693  FaninMax = -1;
1694  for ( k = 0; k < pObj->nFans; k++ )
1695  if ( WeightMax < Weights[k] )
1696  {
1697  WeightMax = Weights[k];
1698  FaninMax = k;
1699  }
1700  // no need to reorder if there are no frequent fanins
1701  if ( FaninMax == -1 )
1702  continue;
1703  // move the fanins number k to the first place
1704  nSwaps = 0;
1705  pIn = Kit_DsdObjTruth(pObj);
1706  pOut = p->pMem;
1707 // for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ )
1708  for ( v = FaninMax-1; v >= 0; v-- )
1709  {
1710  // swap the fanins
1711  Temp = pObj->pFans[v];
1712  pObj->pFans[v] = pObj->pFans[v+1];
1713  pObj->pFans[v+1] = Temp;
1714  // swap the truth table variables
1715  Kit_TruthSwapAdjacentVars( pOut, pIn, pObj->nFans, v );
1716  pTemp = pIn; pIn = pOut; pOut = pTemp;
1717  nSwaps++;
1718  }
1719  if ( nSwaps & 1 )
1720  Kit_TruthCopy( pOut, pIn, pObj->nFans );
1721  }
1722 }
1723 
1724 /**Function*************************************************************
1725 
1726  Synopsis [Compute the support.]
1727 
1728  Description []
1729 
1730  SideEffects []
1731 
1732  SeeAlso []
1733 
1734 ***********************************************************************/
1735 unsigned Kit_DsdGetSupports_rec( Kit_DsdNtk_t * p, int iLit )
1736 {
1737  Kit_DsdObj_t * pObj;
1738  unsigned uSupport, k;
1739  int iFaninLit;
1740  pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1741  if ( pObj == NULL )
1742  return Kit_DsdLitSupport( p, iLit );
1743  uSupport = 0;
1744  Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
1745  uSupport |= Kit_DsdGetSupports_rec( p, iFaninLit );
1746  p->pSupps[pObj->Id - p->nVars] = uSupport;
1747  assert( uSupport <= 0xFFFF );
1748  return uSupport;
1749 }
1750 
1751 /**Function*************************************************************
1752 
1753  Synopsis [Compute the support.]
1754 
1755  Description []
1756 
1757  SideEffects []
1758 
1759  SeeAlso []
1760 
1761 ***********************************************************************/
1762 unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p )
1763 {
1764  Kit_DsdObj_t * pRoot;
1765  unsigned uSupport;
1766  assert( p->pSupps == NULL );
1767  p->pSupps = ABC_ALLOC( unsigned, p->nNodes );
1768  // consider simple special cases
1769  pRoot = Kit_DsdNtkRoot(p);
1770  if ( pRoot->Type == KIT_DSD_CONST1 )
1771  {
1772  assert( p->nNodes == 1 );
1773  uSupport = p->pSupps[0] = 0;
1774  }
1775  if ( pRoot->Type == KIT_DSD_VAR )
1776  {
1777  assert( p->nNodes == 1 );
1778  uSupport = p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
1779  }
1780  else
1781  uSupport = Kit_DsdGetSupports_rec( p, p->Root );
1782  assert( uSupport <= 0xFFFF );
1783  return uSupport;
1784 }
1785 
1786 /**Function*************************************************************
1787 
1788  Synopsis [Returns 1 if there is a component with more than 3 inputs.]
1789 
1790  Description []
1791 
1792  SideEffects []
1793 
1794  SeeAlso []
1795 
1796 ***********************************************************************/
1797 int Kit_DsdFindLargeBox_rec( Kit_DsdNtk_t * pNtk, int Id, int Size )
1798 {
1799  Kit_DsdObj_t * pObj;
1800  unsigned iLit, i, RetValue;
1801  pObj = Kit_DsdNtkObj( pNtk, Id );
1802  if ( pObj == NULL )
1803  return 0;
1804  if ( pObj->Type == KIT_DSD_PRIME && (int)pObj->nFans > Size )
1805  return 1;
1806  RetValue = 0;
1807  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1808  RetValue |= Kit_DsdFindLargeBox_rec( pNtk, Abc_Lit2Var(iLit), Size );
1809  return RetValue;
1810 }
1811 
1812 /**Function*************************************************************
1813 
1814  Synopsis [Returns 1 if there is a component with more than 3 inputs.]
1815 
1816  Description []
1817 
1818  SideEffects []
1819 
1820  SeeAlso []
1821 
1822 ***********************************************************************/
1823 int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size )
1824 {
1825  return Kit_DsdFindLargeBox_rec( pNtk, Abc_Lit2Var(pNtk->Root), Size );
1826 }
1827 
1828 /**Function*************************************************************
1829 
1830  Synopsis [Returns 1 if there is a component with more than 3 inputs.]
1831 
1832  Description []
1833 
1834  SideEffects []
1835 
1836  SeeAlso []
1837 
1838 ***********************************************************************/
1839 int Kit_DsdCountAigNodes_rec( Kit_DsdNtk_t * pNtk, int Id )
1840 {
1841  Kit_DsdObj_t * pObj;
1842  unsigned iLit, i, RetValue;
1843  pObj = Kit_DsdNtkObj( pNtk, Id );
1844  if ( pObj == NULL )
1845  return 0;
1846  if ( pObj->Type == KIT_DSD_CONST1 || pObj->Type == KIT_DSD_VAR )
1847  return 0;
1848  if ( pObj->nFans < 2 ) // why this happens? - need to figure out
1849  return 0;
1850  assert( pObj->nFans > 1 );
1851  if ( pObj->Type == KIT_DSD_AND )
1852  RetValue = ((int)pObj->nFans - 1);
1853  else if ( pObj->Type == KIT_DSD_XOR )
1854  RetValue = ((int)pObj->nFans - 1) * 3;
1855  else if ( pObj->Type == KIT_DSD_PRIME )
1856  {
1857  // assuming MUX decomposition
1858  assert( (int)pObj->nFans == 3 );
1859  RetValue = 3;
1860  }
1861  else assert( 0 );
1862  Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1863  RetValue += Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(iLit) );
1864  return RetValue;
1865 }
1866 
1867 
1868 /**Function*************************************************************
1869 
1870  Synopsis [Returns 1 if there is a component with more than 3 inputs.]
1871 
1872  Description []
1873 
1874  SideEffects []
1875 
1876  SeeAlso []
1877 
1878 ***********************************************************************/
1879 int Kit_DsdCountAigNodes2( Kit_DsdNtk_t * pNtk )
1880 {
1881  return Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(pNtk->Root) );
1882 }
1883 
1884 /**Function*************************************************************
1885 
1886  Synopsis [Returns 1 if there is a component with more than 3 inputs.]
1887 
1888  Description []
1889 
1890  SideEffects []
1891 
1892  SeeAlso []
1893 
1894 ***********************************************************************/
1895 int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk )
1896 {
1897  Kit_DsdObj_t * pObj;
1898  int i, Counter = 0;
1899  for ( i = 0; i < pNtk->nNodes; i++ )
1900  {
1901  pObj = pNtk->pNodes[i];
1902  if ( pObj->Type == KIT_DSD_AND )
1903  Counter += ((int)pObj->nFans - 1);
1904  else if ( pObj->Type == KIT_DSD_XOR )
1905  Counter += ((int)pObj->nFans - 1) * 3;
1906  else if ( pObj->Type == KIT_DSD_PRIME ) // assuming MUX decomposition
1907  Counter += 3;
1908  }
1909  return Counter;
1910 }
1911 
1912 /**Function*************************************************************
1913 
1914  Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
1915 
1916  Description []
1917 
1918  SideEffects []
1919 
1920  SeeAlso []
1921 
1922 ***********************************************************************/
1923 int Kit_DsdRootNodeHasCommonVars( Kit_DsdObj_t * pObj0, Kit_DsdObj_t * pObj1 )
1924 {
1925  unsigned i, k;
1926  for ( i = 0; i < pObj0->nFans; i++ )
1927  {
1928  if ( Abc_Lit2Var(pObj0->pFans[i]) >= 4 )
1929  continue;
1930  for ( k = 0; k < pObj1->nFans; k++ )
1931  if ( Abc_Lit2Var(pObj0->pFans[i]) == Abc_Lit2Var(pObj1->pFans[k]) )
1932  return 1;
1933  }
1934  return 0;
1935 }
1936 
1937 /**Function*************************************************************
1938 
1939  Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
1940 
1941  Description []
1942 
1943  SideEffects []
1944 
1945  SeeAlso []
1946 
1947 ***********************************************************************/
1948 int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
1949 {
1950  assert( pNtk0->nVars == 4 );
1951  assert( pNtk1->nVars == 4 );
1952  if ( Kit_DsdFindLargeBox(pNtk0, 2) )
1953  return 0;
1954  if ( Kit_DsdFindLargeBox(pNtk1, 2) )
1955  return 0;
1956  return Kit_DsdRootNodeHasCommonVars( Kit_DsdNtkRoot(pNtk0), Kit_DsdNtkRoot(pNtk1) );
1957 }
1958 
1959 /**Function*************************************************************
1960 
1961  Synopsis [Performs decomposition of the node.]
1962 
1963  Description []
1964 
1965  SideEffects []
1966 
1967  SeeAlso []
1968 
1969 ***********************************************************************/
1970 void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned short * pPar, int nDecMux )
1971 {
1972  Kit_DsdObj_t * pRes, * pRes0, * pRes1;
1973  int nWords = Kit_TruthWordNum(pObj->nFans);
1974  unsigned * pTruth = Kit_DsdObjTruth(pObj);
1975  unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords };
1976  unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} };
1977  int i, iLit0, iLit1, nFans0, nFans1, nPairs;
1978  int fEquals[2][2], fOppos, fPairs[4][4];
1979  unsigned j, k, nFansNew, uSupp0, uSupp1;
1980 
1981  assert( pObj->nFans > 0 );
1982  assert( pObj->Type == KIT_DSD_PRIME );
1983  assert( uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) );
1984 
1985  // compress the truth table
1986  if ( uSupp != Kit_BitMask(pObj->nFans) )
1987  {
1988  nFansNew = Kit_WordCountOnes(uSupp);
1989  Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, uSupp, 1 );
1990  for ( j = k = 0; j < pObj->nFans; j++ )
1991  if ( uSupp & (1 << j) )
1992  pObj->pFans[k++] = pObj->pFans[j];
1993  assert( k == nFansNew );
1994  pObj->nFans = k;
1995  uSupp = Kit_BitMask(pObj->nFans);
1996  }
1997 
1998  // consider the single variable case
1999  if ( pObj->nFans == 1 )
2000  {
2001  pObj->Type = KIT_DSD_NONE;
2002  if ( pTruth[0] == 0x55555555 )
2003  pObj->pFans[0] = Abc_LitNot(pObj->pFans[0]);
2004  else
2005  assert( pTruth[0] == 0xAAAAAAAA );
2006  // update the parent pointer
2007  *pPar = Abc_LitNotCond( pObj->pFans[0], Abc_LitIsCompl(*pPar) );
2008  return;
2009  }
2010 
2011  // decompose the output
2012  if ( !pObj->fMark )
2013  for ( i = pObj->nFans - 1; i >= 0; i-- )
2014  {
2015  // get the two-variable cofactors
2016  Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i );
2017  Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i );
2018 // assert( !Kit_TruthVarInSupport( pCofs2[0], pObj->nFans, i) );
2019 // assert( !Kit_TruthVarInSupport( pCofs2[1], pObj->nFans, i) );
2020  // get the constant cofs
2021  fEquals[0][0] = Kit_TruthIsConst0( pCofs2[0], pObj->nFans );
2022  fEquals[0][1] = Kit_TruthIsConst0( pCofs2[1], pObj->nFans );
2023  fEquals[1][0] = Kit_TruthIsConst1( pCofs2[0], pObj->nFans );
2024  fEquals[1][1] = Kit_TruthIsConst1( pCofs2[1], pObj->nFans );
2025  fOppos = Kit_TruthIsOpposite( pCofs2[0], pCofs2[1], pObj->nFans );
2026  assert( !Kit_TruthIsEqual(pCofs2[0], pCofs2[1], pObj->nFans) );
2027  if ( fEquals[0][0] + fEquals[0][1] + fEquals[1][0] + fEquals[1][1] + fOppos == 0 )
2028  {
2029  // check the MUX decomposition
2030  uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
2031  uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
2032  assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) );
2033  if ( uSupp0 & uSupp1 )
2034  continue;
2035  // perform MUX decomposition
2036  pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
2037  pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
2038  for ( k = 0; k < pObj->nFans; k++ )
2039  {
2040  pRes0->pFans[k] = (uSupp0 & (1 << k))? pObj->pFans[k] : 127;
2041  pRes1->pFans[k] = (uSupp1 & (1 << k))? pObj->pFans[k] : 127;
2042  }
2043  Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );
2044  Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans );
2045  // update the current one
2046  assert( pObj->Type == KIT_DSD_PRIME );
2047  pTruth[0] = 0xCACACACA;
2048  pObj->nFans = 3;
2049  pObj->pFans[2] = pObj->pFans[i];
2050  pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
2051  pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
2052  // call recursively
2053  Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
2054  Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
2055  return;
2056  }
2057 
2058  // create the new node
2059  pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
2060  pRes->nRefs++;
2061  pRes->nFans = 2;
2062  pRes->pFans[0] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i);
2063  pRes->pFans[1] = 2*pObj->Id;
2064  // update the parent pointer
2065  *pPar = Abc_LitNotCond( 2 * pRes->Id, Abc_LitIsCompl(*pPar) );
2066  // consider different decompositions
2067  if ( fEquals[0][0] )
2068  {
2069  Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
2070  }
2071  else if ( fEquals[0][1] )
2072  {
2073  pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2074  Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
2075  }
2076  else if ( fEquals[1][0] )
2077  {
2078  *pPar = Abc_LitNot(*pPar);
2079  pRes->pFans[1] = Abc_LitNot(pRes->pFans[1]);
2080  Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
2081  }
2082  else if ( fEquals[1][1] )
2083  {
2084  *pPar = Abc_LitNot(*pPar);
2085  pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2086  pRes->pFans[1] = Abc_LitNot(pRes->pFans[1]);
2087  Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
2088  }
2089  else if ( fOppos )
2090  {
2091  pRes->Type = KIT_DSD_XOR;
2092  Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
2093  }
2094  else
2095  assert( 0 );
2096  // decompose the remainder
2097  assert( Kit_DsdObjTruth(pObj) == pTruth );
2098  Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1, nDecMux );
2099  return;
2100  }
2101  pObj->fMark = 1;
2102 
2103  // decompose the input
2104  for ( i = pObj->nFans - 1; i >= 0; i-- )
2105  {
2106  assert( Kit_TruthVarInSupport( pTruth, pObj->nFans, i ) );
2107  // get the single variale cofactors
2108  Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i );
2109  Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i );
2110  // check the existence of MUX decomposition
2111  uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
2112  uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
2113  assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) );
2114  // if one of the cofs is a constant, it is time to check the output again
2115  if ( uSupp0 == 0 || uSupp1 == 0 )
2116  {
2117  pObj->fMark = 0;
2118  Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
2119  return;
2120  }
2121  assert( uSupp0 && uSupp1 );
2122  // get the number of unique variables
2123  nFans0 = Kit_WordCountOnes( uSupp0 & ~uSupp1 );
2124  nFans1 = Kit_WordCountOnes( uSupp1 & ~uSupp0 );
2125  if ( nFans0 == 1 && nFans1 == 1 )
2126  {
2127  // get the cofactors w.r.t. the unique variables
2128  iLit0 = Kit_WordFindFirstBit( uSupp0 & ~uSupp1 );
2129  iLit1 = Kit_WordFindFirstBit( uSupp1 & ~uSupp0 );
2130  // get four cofactors
2131  Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, iLit0 );
2132  Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, iLit0 );
2133  Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, iLit1 );
2134  Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, iLit1 );
2135  // check existence conditions
2136  fEquals[0][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
2137  fEquals[0][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
2138  fEquals[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans );
2139  fEquals[1][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans );
2140  if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) )
2141  {
2142  // construct the MUX
2143  pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, 3 );
2144  Kit_DsdObjTruth(pRes)[0] = 0xCACACACA;
2145  pRes->nRefs++;
2146  pRes->nFans = 3;
2147  pRes->pFans[0] = pObj->pFans[iLit0]; pObj->pFans[iLit0] = 127; uSupp &= ~(1 << iLit0);
2148  pRes->pFans[1] = pObj->pFans[iLit1]; pObj->pFans[iLit1] = 127; uSupp &= ~(1 << iLit1);
2149  pRes->pFans[2] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support
2150  // update the node
2151 // if ( fEquals[0][0] && fEquals[0][1] )
2152 // Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
2153 // else
2154 // Kit_TruthMuxVar( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
2155  Kit_TruthMuxVar( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i );
2156  if ( fEquals[1][0] && fEquals[1][1] )
2157  pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2158  // decompose the remainder
2159  Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
2160  return;
2161  }
2162  }
2163 
2164  // try other inputs
2165  for ( k = i+1; k < pObj->nFans; k++ )
2166  {
2167  // get four cofactors ik
2168  Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, k ); // 00
2169  Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, k ); // 01
2170  Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, k ); // 10
2171  Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, k ); // 11
2172  // compare equal pairs
2173  fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[0][1], pObj->nFans );
2174  fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
2175  fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans );
2176  fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans );
2177  fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
2178  fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual( pCofs4[1][0], pCofs4[1][1], pObj->nFans );
2179  nPairs = fPairs[0][1] + fPairs[0][2] + fPairs[0][3] + fPairs[1][2] + fPairs[1][3] + fPairs[2][3];
2180  if ( nPairs != 3 && nPairs != 2 )
2181  continue;
2182 
2183  // decomposition exists
2184  pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
2185  pRes->nRefs++;
2186  pRes->nFans = 2;
2187  pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id; // remains in support
2188  pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i);
2189  if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
2190  {
2191  pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2192  pRes->pFans[1] = Abc_LitNot(pRes->pFans[1]);
2193  Kit_TruthMuxVar( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
2194  }
2195  else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01
2196  {
2197  pRes->pFans[1] = Abc_LitNot(pRes->pFans[1]);
2198  Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
2199  }
2200  else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10
2201  {
2202  pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2203  Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
2204  }
2205  else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
2206  {
2207 // unsigned uSupp0 = Kit_TruthSupport(pCofs4[0][0], pObj->nFans);
2208 // unsigned uSupp1 = Kit_TruthSupport(pCofs4[1][1], pObj->nFans);
2209 // unsigned uSupp;
2210 // Extra_PrintBinary( stdout, &uSupp0, pObj->nFans ); printf( "\n" );
2211 // Extra_PrintBinary( stdout, &uSupp1, pObj->nFans ); printf( "\n" );
2212  Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k );
2213 // uSupp = Kit_TruthSupport(pTruth, pObj->nFans);
2214 // Extra_PrintBinary( stdout, &uSupp, pObj->nFans ); printf( "\n" ); printf( "\n" );
2215  }
2216  else
2217  {
2218  assert( fPairs[0][3] && fPairs[1][2] );
2219  pRes->Type = KIT_DSD_XOR;;
2220  Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
2221  }
2222  // decompose the remainder
2223  Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
2224  return;
2225  }
2226  }
2227 
2228  // if all decomposition methods failed and we are still above the limit, perform MUX-decomposition
2229  if ( nDecMux > 0 && (int)pObj->nFans > nDecMux )
2230  {
2231  int iBestVar = Kit_TruthBestCofVar( pTruth, pObj->nFans, pCofs2[0], pCofs2[1] );
2232  uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
2233  uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
2234  // perform MUX decomposition
2235  pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
2236  pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
2237  for ( k = 0; k < pObj->nFans; k++ )
2238  pRes0->pFans[k] = pRes1->pFans[k] = pObj->pFans[k];
2239  Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );
2240  Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans );
2241  // update the current one
2242  assert( pObj->Type == KIT_DSD_PRIME );
2243  pTruth[0] = 0xCACACACA;
2244  pObj->nFans = 3;
2245  pObj->pFans[2] = pObj->pFans[iBestVar];
2246  pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
2247  pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
2248  // call recursively
2249  Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
2250  Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
2251  }
2252 
2253 }
2254 
2255 /**Function*************************************************************
2256 
2257  Synopsis [Performs decomposition of the truth table.]
2258 
2259  Description []
2260 
2261  SideEffects []
2262 
2263  SeeAlso []
2264 
2265 ***********************************************************************/
2266 Kit_DsdNtk_t * Kit_DsdDecomposeInt( unsigned * pTruth, int nVars, int nDecMux )
2267 {
2268  Kit_DsdNtk_t * pNtk;
2269  Kit_DsdObj_t * pObj;
2270  unsigned uSupp;
2271  int i, nVarsReal;
2272  assert( nVars <= 16 );
2273  pNtk = Kit_DsdNtkAlloc( nVars );
2274  pNtk->Root = Abc_Var2Lit( pNtk->nVars, 0 );
2275  // create the first node
2276  pObj = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, nVars );
2277  assert( pNtk->pNodes[0] == pObj );
2278  for ( i = 0; i < nVars; i++ )
2279  pObj->pFans[i] = Abc_Var2Lit( i, 0 );
2280  Kit_TruthCopy( Kit_DsdObjTruth(pObj), pTruth, nVars );
2281  uSupp = Kit_TruthSupport( pTruth, nVars );
2282  // consider special cases
2283  nVarsReal = Kit_WordCountOnes( uSupp );
2284  if ( nVarsReal == 0 )
2285  {
2286  pObj->Type = KIT_DSD_CONST1;
2287  pObj->nFans = 0;
2288  if ( pTruth[0] == 0 )
2289  pNtk->Root = Abc_LitNot(pNtk->Root);
2290  return pNtk;
2291  }
2292  if ( nVarsReal == 1 )
2293  {
2294  pObj->Type = KIT_DSD_VAR;
2295  pObj->nFans = 1;
2296  pObj->pFans[0] = Abc_Var2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) );
2297  return pNtk;
2298  }
2299  Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root, nDecMux );
2300  return pNtk;
2301 }
2302 
2303 /**Function*************************************************************
2304 
2305  Synopsis [Performs decomposition of the truth table.]
2306 
2307  Description []
2308 
2309  SideEffects []
2310 
2311  SeeAlso []
2312 
2313 ***********************************************************************/
2314 Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
2315 {
2316  return Kit_DsdDecomposeInt( pTruth, nVars, 0 );
2317 }
2318 
2319 /**Function*************************************************************
2320 
2321  Synopsis [Performs decomposition of the truth table.]
2322 
2323  Description []
2324 
2325  SideEffects []
2326 
2327  SeeAlso []
2328 
2329 ***********************************************************************/
2330 Kit_DsdNtk_t * Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars )
2331 {
2332  Kit_DsdNtk_t * pNtk, * pTemp;
2333  pNtk = Kit_DsdDecomposeInt( pTruth, nVars, 0 );
2334  pNtk = Kit_DsdExpand( pTemp = pNtk );
2335  Kit_DsdNtkFree( pTemp );
2336  return pNtk;
2337 }
2338 
2339 /**Function*************************************************************
2340 
2341  Synopsis [Performs decomposition of the truth table.]
2342 
2343  Description [Uses MUXes to break-down large prime nodes.]
2344 
2345  SideEffects []
2346 
2347  SeeAlso []
2348 
2349 ***********************************************************************/
2350 Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux )
2351 {
2352 /*
2353  Kit_DsdNtk_t * pNew;
2354  Kit_DsdObj_t * pObjNew;
2355  assert( nVars <= 16 );
2356  // create a new network
2357  pNew = Kit_DsdNtkAlloc( nVars );
2358  // consider simple special cases
2359  if ( nVars == 0 )
2360  {
2361  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
2362  pNew->Root = Abc_Var2Lit( pObjNew->Id, (int)(pTruth[0] == 0) );
2363  return pNew;
2364  }
2365  if ( nVars == 1 )
2366  {
2367  pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
2368  pObjNew->pFans[0] = Abc_Var2Lit( 0, 0 );
2369  pNew->Root = Abc_Var2Lit( pObjNew->Id, (int)(pTruth[0] != 0xAAAAAAAA) );
2370  return pNew;
2371  }
2372 */
2373  return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux );
2374 }
2375 
2376 /**Function*************************************************************
2377 
2378  Synopsis [Performs decomposition of the truth table.]
2379 
2380  Description []
2381 
2382  SideEffects []
2383 
2384  SeeAlso []
2385 
2386 ***********************************************************************/
2387 int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
2388 {
2389  Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
2390 // Kit_DsdObj_t * pRoot;
2391  unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
2392  unsigned i, * pTruth;
2393  int fVerbose = 1;
2394  int RetValue = 0;
2395 
2396  pTruth = pTruthInit;
2397 // pRoot = Kit_DsdNtkRoot(pNtk);
2398 // pTruth = Kit_DsdObjTruth(pRoot);
2399 // assert( pRoot->nFans == pNtk->nVars );
2400 
2401  if ( fVerbose )
2402  {
2403  printf( "Function: " );
2404 // Extra_PrintBinary( stdout, pTruth, (1 << pNtk->nVars) );
2405  Extra_PrintHexadecimal( stdout, pTruth, pNtk->nVars );
2406  printf( "\n" );
2407  Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
2408  }
2409  for ( i = 0; i < pNtk->nVars; i++ )
2410  {
2411  Kit_TruthCofactor0New( pCofs2[0], pTruth, pNtk->nVars, i );
2412  pNtk0 = Kit_DsdDecompose( pCofs2[0], pNtk->nVars );
2413  pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
2414  Kit_DsdNtkFree( pTemp );
2415 
2416  if ( fVerbose )
2417  {
2418  printf( "Cof%d0: ", i );
2419  Kit_DsdPrint( stdout, pNtk0 ), printf( "\n" );
2420  }
2421 
2422  Kit_TruthCofactor1New( pCofs2[1], pTruth, pNtk->nVars, i );
2423  pNtk1 = Kit_DsdDecompose( pCofs2[1], pNtk->nVars );
2424  pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
2425  Kit_DsdNtkFree( pTemp );
2426 
2427  if ( fVerbose )
2428  {
2429  printf( "Cof%d1: ", i );
2430  Kit_DsdPrint( stdout, pNtk1 ), printf( "\n" );
2431  }
2432 
2433 // if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
2434 // RetValue = 1;
2435 
2436  Kit_DsdNtkFree( pNtk0 );
2437  Kit_DsdNtkFree( pNtk1 );
2438  }
2439  if ( fVerbose )
2440  printf( "\n" );
2441 
2442  return RetValue;
2443 }
2444 
2445 /**Function*************************************************************
2446 
2447  Synopsis [Performs decomposition of the truth table.]
2448 
2449  Description []
2450 
2451  SideEffects []
2452 
2453  SeeAlso []
2454 
2455 ***********************************************************************/
2456 int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
2457 {
2458  Kit_DsdMan_t * p;
2459  Kit_DsdNtk_t * pNtk;
2460  unsigned * pTruthC;
2461  int Result;
2462 
2463  // decompose the function
2464  pNtk = Kit_DsdDecompose( pTruth, nVars );
2465  Result = Kit_DsdCountLuts( pNtk, nLutSize );
2466 // printf( "\n" );
2467 // Kit_DsdPrint( stdout, pNtk );
2468 // printf( "Eval = %d.\n", Result );
2469 
2470  // recompute the truth table
2471  p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
2472  pTruthC = Kit_DsdTruthCompute( p, pNtk );
2473  if ( !Kit_TruthIsEqual( pTruth, pTruthC, nVars ) )
2474  printf( "Verification failed.\n" );
2475  Kit_DsdManFree( p );
2476 
2477  Kit_DsdNtkFree( pNtk );
2478  return Result;
2479 }
2480 
2481 /**Function*************************************************************
2482 
2483  Synopsis [Performs decomposition of the truth table.]
2484 
2485  Description []
2486 
2487  SideEffects []
2488 
2489  SeeAlso []
2490 
2491 ***********************************************************************/
2492 void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
2493 {
2494  Kit_DsdMan_t * p;
2495  unsigned * pTruthC;
2496  p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
2497  pTruthC = Kit_DsdTruthCompute( p, pNtk );
2498  if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
2499  printf( "Verification failed.\n" );
2500  Kit_DsdManFree( p );
2501 }
2502 
2503 /**Function*************************************************************
2504 
2505  Synopsis [Performs decomposition of the truth table.]
2506 
2507  Description []
2508 
2509  SideEffects []
2510 
2511  SeeAlso []
2512 
2513 ***********************************************************************/
2514 void Kit_DsdTest( unsigned * pTruth, int nVars )
2515 {
2516  Kit_DsdMan_t * p;
2517  unsigned * pTruthC;
2518  Kit_DsdNtk_t * pNtk, * pTemp;
2519  pNtk = Kit_DsdDecompose( pTruth, nVars );
2520 
2521 // if ( Kit_DsdFindLargeBox(pNtk, Abc_Lit2Var(pNtk->Root)) )
2522 // Kit_DsdPrint( stdout, pNtk );
2523 
2524 // if ( Kit_DsdNtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
2525 
2526 // printf( "\n" );
2527 // Kit_DsdPrint( stdout, pNtk );
2528 
2529  pNtk = Kit_DsdExpand( pTemp = pNtk );
2530  Kit_DsdNtkFree( pTemp );
2531 
2532  Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
2533 
2534 // if ( Kit_DsdFindLargeBox(pNtk, Abc_Lit2Var(pNtk->Root)) )
2535 // Kit_DsdTestCofs( pNtk, pTruth );
2536 
2537  // recompute the truth table
2538  p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
2539  pTruthC = Kit_DsdTruthCompute( p, pNtk );
2540 // Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
2541 // Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
2542  if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
2543  {
2544 // printf( "Verification is okay.\n" );
2545  }
2546  else
2547  printf( "Verification failed.\n" );
2548  Kit_DsdManFree( p );
2549 
2550 
2551  Kit_DsdNtkFree( pNtk );
2552 }
2553 
2554 /**Function*************************************************************
2555 
2556  Synopsis [Performs decomposition of the truth table.]
2557 
2558  Description []
2559 
2560  SideEffects []
2561 
2562  SeeAlso []
2563 
2564 ***********************************************************************/
2565 void Kit_DsdPrecompute4Vars()
2566 {
2567  Kit_DsdMan_t * p;
2568  Kit_DsdNtk_t * pNtk, * pTemp;
2569  FILE * pFile;
2570  unsigned uTruth;
2571  unsigned * pTruthC;
2572  char Buffer[256];
2573  int i, RetValue;
2574  int Counter1 = 0, Counter2 = 0;
2575 
2576  pFile = fopen( "5npn/npn4.txt", "r" );
2577  for ( i = 0; fgets( Buffer, 100, pFile ); i++ )
2578  {
2579  Buffer[6] = 0;
2580  Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
2581  uTruth = ((uTruth & 0xffff) << 16) | (uTruth & 0xffff);
2582  pNtk = Kit_DsdDecompose( &uTruth, 4 );
2583 
2584  pNtk = Kit_DsdExpand( pTemp = pNtk );
2585  Kit_DsdNtkFree( pTemp );
2586 
2587 
2588  if ( Kit_DsdFindLargeBox(pNtk, 3) )
2589  {
2590 // RetValue = 0;
2591  RetValue = Kit_DsdTestCofs( pNtk, &uTruth );
2592  printf( "\n" );
2593  printf( "%3d : Non-DSD function %s %s\n", i, Buffer + 2, RetValue? "implementable" : "" );
2594  Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
2595 
2596  Counter1++;
2597  Counter2 += RetValue;
2598  }
2599 
2600 /*
2601  printf( "%3d : Function %s ", i, Buffer + 2 );
2602  if ( !Kit_DsdFindLargeBox(pNtk, 3) )
2603  Kit_DsdPrint( stdout, pNtk );
2604  else
2605  printf( "\n" );
2606 */
2607 
2608  p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) );
2609  pTruthC = Kit_DsdTruthCompute( p, pNtk );
2610  if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
2611  printf( "Verification failed.\n" );
2612  Kit_DsdManFree( p );
2613 
2614  Kit_DsdNtkFree( pNtk );
2615  }
2616  fclose( pFile );
2617  printf( "non-DSD = %d implementable = %d\n", Counter1, Counter2 );
2618 }
2619 
2620 
2621 /**Function*************************************************************
2622 
2623  Synopsis [Returns the set of cofactoring variables.]
2624 
2625  Description [If there is no DSD components returns 0.]
2626 
2627  SideEffects []
2628 
2629  SeeAlso []
2630 
2631 ***********************************************************************/
2632 int Kit_DsdCofactoringGetVars( Kit_DsdNtk_t ** ppNtk, int nSize, int * pVars )
2633 {
2634  Kit_DsdObj_t * pObj;
2635  unsigned m;
2636  int i, k, v, Var, nVars, iFaninLit;
2637  // go through all the networks
2638  nVars = 0;
2639  for ( i = 0; i < nSize; i++ )
2640  {
2641  // go through the prime objects of each networks
2642  Kit_DsdNtkForEachObj( ppNtk[i], pObj, k )
2643  {
2644  if ( pObj->Type != KIT_DSD_PRIME )
2645  continue;
2646  if ( pObj->nFans == 3 )
2647  continue;
2648  // collect direct fanin variables
2649  Kit_DsdObjForEachFanin( ppNtk[i], pObj, iFaninLit, m )
2650  {
2651  if ( !Kit_DsdLitIsLeaf(ppNtk[i], iFaninLit) )
2652  continue;
2653  // add it to the array
2654  Var = Abc_Lit2Var( iFaninLit );
2655  for ( v = 0; v < nVars; v++ )
2656  if ( pVars[v] == Var )
2657  break;
2658  if ( v == nVars )
2659  pVars[nVars++] = Var;
2660  }
2661  }
2662  }
2663  return nVars;
2664 }
2665 
2666 /**Function*************************************************************
2667 
2668  Synopsis [Canonical decomposition into completely DSD-structure.]
2669 
2670  Description [Returns the number of cofactoring steps. Also returns
2671  the cofactoring variables in pVars.]
2672 
2673  SideEffects []
2674 
2675  SeeAlso []
2676 
2677 ***********************************************************************/
2678 int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit, int fVerbose )
2679 {
2680  Kit_DsdNtk_t * ppNtks[5][16] = {
2681  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
2682  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
2683  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
2684  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
2685  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
2686  };
2687  Kit_DsdNtk_t * pTemp;
2688  unsigned * ppCofs[5][16];
2689  int pTryVars[16], nTryVars;
2690  int nPrimeSizeMin, nPrimeSizeMax, nPrimeSizeCur;
2691  int nSuppSizeMin, nSuppSizeMax, iVarBest;
2692  int i, k, v, nStep, nSize, nMemSize;
2693  assert( nLimit < 5 );
2694 
2695  // allocate storage for cofactors
2696  nMemSize = Kit_TruthWordNum(nVars);
2697  ppCofs[0][0] = ABC_ALLOC( unsigned, 80 * nMemSize );
2698  nSize = 0;
2699  for ( i = 0; i < 5; i++ )
2700  for ( k = 0; k < 16; k++ )
2701  ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
2702  assert( nSize == 80 );
2703 
2704  // copy the function
2705  Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
2706  ppNtks[0][0] = Kit_DsdDecompose( ppCofs[0][0], nVars );
2707 
2708  if ( fVerbose )
2709  printf( "\nProcessing prime function with %d support variables:\n", nVars );
2710 
2711  // perform recursive cofactoring
2712  for ( nStep = 0; nStep < nLimit; nStep++ )
2713  {
2714  nSize = (1 << nStep);
2715  // find the variables to use in the cofactoring step
2716  nTryVars = Kit_DsdCofactoringGetVars( ppNtks[nStep], nSize, pTryVars );
2717  if ( nTryVars == 0 )
2718  break;
2719  // cofactor w.r.t. the above variables
2720  iVarBest = -1;
2721  nPrimeSizeMin = 10000;
2722  nSuppSizeMin = 10000;
2723  for ( v = 0; v < nTryVars; v++ )
2724  {
2725  nPrimeSizeMax = 0;
2726  nSuppSizeMax = 0;
2727  for ( i = 0; i < nSize; i++ )
2728  {
2729  // cofactor and decompose cofactors
2730  Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, pTryVars[v] );
2731  Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, pTryVars[v] );
2732  ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
2733  ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
2734  // compute the largest non-decomp block
2735  nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+0]);
2736  nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2737  nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+1]);
2738  nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2739  // compute the sum total of supports
2740  nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
2741  nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
2742  // free the networks
2743  Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
2744  Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
2745  }
2746  // find the min max support size of the prime component
2747  if ( nPrimeSizeMin > nPrimeSizeMax || (nPrimeSizeMin == nPrimeSizeMax && nSuppSizeMin > nSuppSizeMax) )
2748  {
2749  nPrimeSizeMin = nPrimeSizeMax;
2750  nSuppSizeMin = nSuppSizeMax;
2751  iVarBest = pTryVars[v];
2752  }
2753  }
2754  assert( iVarBest != -1 );
2755  // save the variable
2756  if ( pCofVars )
2757  pCofVars[nStep] = iVarBest;
2758  // cofactor w.r.t. the best
2759  for ( i = 0; i < nSize; i++ )
2760  {
2761  Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, iVarBest );
2762  Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, iVarBest );
2763  ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
2764  ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
2765  if ( fVerbose )
2766  {
2767  ppNtks[nStep+1][2*i+0] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+0] );
2768  Kit_DsdNtkFree( pTemp );
2769  ppNtks[nStep+1][2*i+1] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+1] );
2770  Kit_DsdNtkFree( pTemp );
2771 
2772  printf( "Cof%d%d: ", nStep+1, 2*i+0 );
2773  Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] ), printf( "\n" );
2774  printf( "Cof%d%d: ", nStep+1, 2*i+1 );
2775  Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] ), printf( "\n" );
2776  }
2777  }
2778  }
2779 
2780  // free the networks
2781  for ( i = 0; i < 5; i++ )
2782  for ( k = 0; k < 16; k++ )
2783  if ( ppNtks[i][k] )
2784  Kit_DsdNtkFree( ppNtks[i][k] );
2785  ABC_FREE( ppCofs[0][0] );
2786 
2787  assert( nStep <= nLimit );
2788  return nStep;
2789 }
2790 
2791 /**Function*************************************************************
2792 
2793  Synopsis [Canonical decomposition into completely DSD-structure.]
2794 
2795  Description [Returns the number of cofactoring steps. Also returns
2796  the cofactoring variables in pVars.]
2797 
2798  SideEffects []
2799 
2800  SeeAlso []
2801 
2802 ***********************************************************************/
2803 void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose )
2804 {
2805  Kit_DsdNtk_t * ppNtks[32] = {0}, * pTemp;
2806  unsigned * ppCofs[5][16];
2807  int piCofVar[5];
2808  int nPrimeSizeMax, nPrimeSizeCur, nSuppSizeMax;
2809  int i, k, v1, v2, v3, v4, s, nSteps, nSize, nMemSize;
2810  assert( nCofLevel < 5 );
2811 
2812  // print the function
2813  ppNtks[0] = Kit_DsdDecompose( pTruth, nVars );
2814  ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
2815  Kit_DsdNtkFree( pTemp );
2816  if ( fVerbose )
2817  Kit_DsdPrint( stdout, ppNtks[0] ), printf( "\n" );
2818  Kit_DsdNtkFree( ppNtks[0] );
2819 
2820  // allocate storage for cofactors
2821  nMemSize = Kit_TruthWordNum(nVars);
2822  ppCofs[0][0] = ABC_ALLOC( unsigned, 80 * nMemSize );
2823  nSize = 0;
2824  for ( i = 0; i < 5; i++ )
2825  for ( k = 0; k < 16; k++ )
2826  ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
2827  assert( nSize == 80 );
2828 
2829  // copy the function
2830  Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
2831 
2832  if ( nCofLevel == 1 )
2833  for ( v1 = 0; v1 < nVars; v1++ )
2834  {
2835  nSteps = 0;
2836  piCofVar[nSteps++] = v1;
2837 
2838  printf( " Variables { " );
2839  for ( i = 0; i < nSteps; i++ )
2840  printf( "%c ", 'a' + piCofVar[i] );
2841  printf( "}\n" );
2842 
2843  // single cofactors
2844  for ( s = 1; s <= nSteps; s++ )
2845  {
2846  for ( k = 0; k < s; k++ )
2847  {
2848  nSize = (1 << k);
2849  for ( i = 0; i < nSize; i++ )
2850  {
2851  Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
2852  Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
2853  }
2854  }
2855  }
2856  // compute DSD networks
2857  nSize = (1 << nSteps);
2858  nPrimeSizeMax = 0;
2859  nSuppSizeMax = 0;
2860  for ( i = 0; i < nSize; i++ )
2861  {
2862  ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
2863  ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
2864  Kit_DsdNtkFree( pTemp );
2865  if ( fVerbose )
2866  {
2867  printf( "Cof%d%d: ", nSteps, i );
2868  Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
2869  }
2870  // compute the largest non-decomp block
2871  nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
2872  nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2873  Kit_DsdNtkFree( ppNtks[i] );
2874  nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
2875  }
2876  printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
2877  }
2878 
2879  if ( nCofLevel == 2 )
2880  for ( v1 = 0; v1 < nVars; v1++ )
2881  for ( v2 = v1+1; v2 < nVars; v2++ )
2882  {
2883  nSteps = 0;
2884  piCofVar[nSteps++] = v1;
2885  piCofVar[nSteps++] = v2;
2886 
2887  printf( " Variables { " );
2888  for ( i = 0; i < nSteps; i++ )
2889  printf( "%c ", 'a' + piCofVar[i] );
2890  printf( "}\n" );
2891 
2892  // single cofactors
2893  for ( s = 1; s <= nSteps; s++ )
2894  {
2895  for ( k = 0; k < s; k++ )
2896  {
2897  nSize = (1 << k);
2898  for ( i = 0; i < nSize; i++ )
2899  {
2900  Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
2901  Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
2902  }
2903  }
2904  }
2905  // compute DSD networks
2906  nSize = (1 << nSteps);
2907  nPrimeSizeMax = 0;
2908  nSuppSizeMax = 0;
2909  for ( i = 0; i < nSize; i++ )
2910  {
2911  ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
2912  ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
2913  Kit_DsdNtkFree( pTemp );
2914  if ( fVerbose )
2915  {
2916  printf( "Cof%d%d: ", nSteps, i );
2917  Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
2918  }
2919  // compute the largest non-decomp block
2920  nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
2921  nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2922  Kit_DsdNtkFree( ppNtks[i] );
2923  nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
2924  }
2925  printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
2926  }
2927 
2928  if ( nCofLevel == 3 )
2929  for ( v1 = 0; v1 < nVars; v1++ )
2930  for ( v2 = v1+1; v2 < nVars; v2++ )
2931  for ( v3 = v2+1; v3 < nVars; v3++ )
2932  {
2933  nSteps = 0;
2934  piCofVar[nSteps++] = v1;
2935  piCofVar[nSteps++] = v2;
2936  piCofVar[nSteps++] = v3;
2937 
2938  printf( " Variables { " );
2939  for ( i = 0; i < nSteps; i++ )
2940  printf( "%c ", 'a' + piCofVar[i] );
2941  printf( "}\n" );
2942 
2943  // single cofactors
2944  for ( s = 1; s <= nSteps; s++ )
2945  {
2946  for ( k = 0; k < s; k++ )
2947  {
2948  nSize = (1 << k);
2949  for ( i = 0; i < nSize; i++ )
2950  {
2951  Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
2952  Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
2953  }
2954  }
2955  }
2956  // compute DSD networks
2957  nSize = (1 << nSteps);
2958  nPrimeSizeMax = 0;
2959  nSuppSizeMax = 0;
2960  for ( i = 0; i < nSize; i++ )
2961  {
2962  ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
2963  ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
2964  Kit_DsdNtkFree( pTemp );
2965  if ( fVerbose )
2966  {
2967  printf( "Cof%d%d: ", nSteps, i );
2968  Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
2969  }
2970  // compute the largest non-decomp block
2971  nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
2972  nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2973  Kit_DsdNtkFree( ppNtks[i] );
2974  nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
2975  }
2976  printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
2977  }
2978 
2979  if ( nCofLevel == 4 )
2980  for ( v1 = 0; v1 < nVars; v1++ )
2981  for ( v2 = v1+1; v2 < nVars; v2++ )
2982  for ( v3 = v2+1; v3 < nVars; v3++ )
2983  for ( v4 = v3+1; v4 < nVars; v4++ )
2984  {
2985  nSteps = 0;
2986  piCofVar[nSteps++] = v1;
2987  piCofVar[nSteps++] = v2;
2988  piCofVar[nSteps++] = v3;
2989  piCofVar[nSteps++] = v4;
2990 
2991  printf( " Variables { " );
2992  for ( i = 0; i < nSteps; i++ )
2993  printf( "%c ", 'a' + piCofVar[i] );
2994  printf( "}\n" );
2995 
2996  // single cofactors
2997  for ( s = 1; s <= nSteps; s++ )
2998  {
2999  for ( k = 0; k < s; k++ )
3000  {
3001  nSize = (1 << k);
3002  for ( i = 0; i < nSize; i++ )
3003  {
3004  Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
3005  Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
3006  }
3007  }
3008  }
3009  // compute DSD networks
3010  nSize = (1 << nSteps);
3011  nPrimeSizeMax = 0;
3012  nSuppSizeMax = 0;
3013  for ( i = 0; i < nSize; i++ )
3014  {
3015  ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
3016  ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
3017  Kit_DsdNtkFree( pTemp );
3018  if ( fVerbose )
3019  {
3020  printf( "Cof%d%d: ", nSteps, i );
3021  Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
3022  }
3023  // compute the largest non-decomp block
3024  nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
3025  nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
3026  Kit_DsdNtkFree( ppNtks[i] );
3027  nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
3028  }
3029  printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
3030  }
3031 
3032 
3033  ABC_FREE( ppCofs[0][0] );
3034 }
3035 
3036 
3037 /**Function*************************************************************
3038 
3039  Synopsis []
3040 
3041  Description []
3042 
3043  SideEffects []
3044 
3045  SeeAlso []
3046 
3047 ***********************************************************************/
3048 char ** Kit_DsdNpn4ClassNames()
3049 {
3050  static const char * pNames[222] = {
3051  "F = 0", /* 0 */
3052  "F = (!d*(!c*(!b*!a)))", /* 1 */
3053  "F = (!d*(!c*!b))", /* 2 */
3054  "F = (!d*(!c*(b+a)))", /* 3 */
3055  "F = (!d*(!c*!(b*a)))", /* 4 */
3056  "F = (!d*!c)", /* 5 */
3057  "F = (!d*16(a,b,c))", /* 6 */
3058  "F = (!d*17(a,b,c))", /* 7 */
3059  "F = (!d*18(a,b,c))", /* 8 */
3060  "F = (!d*19(a,b,c))", /* 9 */
3061  "F = (!d*CA(!b,!c,a))", /* 10 */
3062  "F = (!d*(c+!(!b*!a)))", /* 11 */
3063  "F = (!d*!(c*!(!b*!a)))", /* 12 */
3064  "F = (!d*(c+b))", /* 13 */
3065  "F = (!d*3D(a,b,c))", /* 14 */
3066  "F = (!d*!(c*b))", /* 15 */
3067  "F = (!d*(c+(b+!a)))", /* 16 */
3068  "F = (!d*6B(a,b,c))", /* 17 */
3069  "F = (!d*!(c*!(b+a)))", /* 18 */
3070  "F = (!d*7E(a,b,c))", /* 19 */
3071  "F = (!d*!(c*(b*a)))", /* 20 */
3072  "F = (!d)", /* 21 */
3073  "F = 0116(a,b,c,d)", /* 22 */
3074  "F = 0117(a,b,c,d)", /* 23 */
3075  "F = 0118(a,b,c,d)", /* 24 */
3076  "F = 0119(a,b,c,d)", /* 25 */
3077  "F = 011A(a,b,c,d)", /* 26 */
3078  "F = 011B(a,b,c,d)", /* 27 */
3079  "F = 29((!b*!a),c,d)", /* 28 */
3080  "F = 2B((!b*!a),c,d)", /* 29 */
3081  "F = 012C(a,b,c,d)", /* 30 */
3082  "F = 012D(a,b,c,d)", /* 31 */
3083  "F = 012F(a,b,c,d)", /* 32 */
3084  "F = 013C(a,b,c,d)", /* 33 */
3085  "F = 013D(a,b,c,d)", /* 34 */
3086  "F = 013E(a,b,c,d)", /* 35 */
3087  "F = 013F(a,b,c,d)", /* 36 */
3088  "F = 0168(a,b,c,d)", /* 37 */
3089  "F = 0169(a,b,c,d)", /* 38 */
3090  "F = 016A(a,b,c,d)", /* 39 */
3091  "F = 016B(a,b,c,d)", /* 40 */
3092  "F = 016E(a,b,c,d)", /* 41 */
3093  "F = 016F(a,b,c,d)", /* 42 */
3094  "F = 017E(a,b,c,d)", /* 43 */
3095  "F = 017F(a,b,c,d)", /* 44 */
3096  "F = 0180(a,b,c,d)", /* 45 */
3097  "F = 0181(a,b,c,d)", /* 46 */
3098  "F = 0182(a,b,c,d)", /* 47 */
3099  "F = 0183(a,b,c,d)", /* 48 */
3100  "F = 0186(a,b,c,d)", /* 49 */
3101  "F = 0187(a,b,c,d)", /* 50 */
3102  "F = 0189(a,b,c,d)", /* 51 */
3103  "F = 018B(a,b,c,d)", /* 52 */
3104  "F = 018F(a,b,c,d)", /* 53 */
3105  "F = 0196(a,b,c,d)", /* 54 */
3106  "F = 0197(a,b,c,d)", /* 55 */
3107  "F = 0198(a,b,c,d)", /* 56 */
3108  "F = 0199(a,b,c,d)", /* 57 */
3109  "F = 019A(a,b,c,d)", /* 58 */
3110  "F = 019B(a,b,c,d)", /* 59 */
3111  "F = 019E(a,b,c,d)", /* 60 */
3112  "F = 019F(a,b,c,d)", /* 61 */
3113  "F = 42(a,(!c*!b),d)", /* 62 */
3114  "F = 46(a,(!c*!b),d)", /* 63 */
3115  "F = 4A(a,(!c*!b),d)", /* 64 */
3116  "F = CA((!c*!b),!d,a)", /* 65 */
3117  "F = 01AC(a,b,c,d)", /* 66 */
3118  "F = 01AD(a,b,c,d)", /* 67 */
3119  "F = 01AE(a,b,c,d)", /* 68 */
3120  "F = 01AF(a,b,c,d)", /* 69 */
3121  "F = 01BC(a,b,c,d)", /* 70 */
3122  "F = 01BD(a,b,c,d)", /* 71 */
3123  "F = 01BE(a,b,c,d)", /* 72 */
3124  "F = 01BF(a,b,c,d)", /* 73 */
3125  "F = 01E8(a,b,c,d)", /* 74 */
3126  "F = 01E9(a,b,c,d)", /* 75 */
3127  "F = 01EA(a,b,c,d)", /* 76 */
3128  "F = 01EB(a,b,c,d)", /* 77 */
3129  "F = 25((!b*!a),c,d)", /* 78 */
3130  "F = !CA(d,c,(!b*!a))", /* 79 */
3131  "F = (d+!(!c*(!b*!a)))", /* 80 */
3132  "F = 16(b,c,d)", /* 81 */
3133  "F = 033D(a,b,c,d)", /* 82 */
3134  "F = 17(b,c,d)", /* 83 */
3135  "F = ((!d*!a)+(!c*!b))", /* 84 */
3136  "F = !(!(!c*!b)*!(!d*!a))", /* 85 */
3137  "F = 0358(a,b,c,d)", /* 86 */
3138  "F = 0359(a,b,c,d)", /* 87 */
3139  "F = 035A(a,b,c,d)", /* 88 */
3140  "F = 035B(a,b,c,d)", /* 89 */
3141  "F = 035E(a,b,c,d)", /* 90 */
3142  "F = 035F(a,b,c,d)", /* 91 */
3143  "F = 0368(a,b,c,d)", /* 92 */
3144  "F = 0369(a,b,c,d)", /* 93 */
3145  "F = 036A(a,b,c,d)", /* 94 */
3146  "F = 036B(a,b,c,d)", /* 95 */
3147  "F = 036C(a,b,c,d)", /* 96 */
3148  "F = 036D(a,b,c,d)", /* 97 */
3149  "F = 036E(a,b,c,d)", /* 98 */
3150  "F = 036F(a,b,c,d)", /* 99 */
3151  "F = 037C(a,b,c,d)", /* 100 */
3152  "F = 037D(a,b,c,d)", /* 101 */
3153  "F = 037E(a,b,c,d)", /* 102 */
3154  "F = 18(b,c,d)", /* 103 */
3155  "F = 03C1(a,b,c,d)", /* 104 */
3156  "F = 19(b,c,d)", /* 105 */
3157  "F = 03C5(a,b,c,d)", /* 106 */
3158  "F = 03C6(a,b,c,d)", /* 107 */
3159  "F = 03C7(a,b,c,d)", /* 108 */
3160  "F = CA(!c,!d,b)", /* 109 */
3161  "F = 03D4(a,b,c,d)", /* 110 */
3162  "F = 03D5(a,b,c,d)", /* 111 */
3163  "F = 03D6(a,b,c,d)", /* 112 */
3164  "F = 03D7(a,b,c,d)", /* 113 */
3165  "F = 03D8(a,b,c,d)", /* 114 */
3166  "F = 03D9(a,b,c,d)", /* 115 */
3167  "F = 03DB(a,b,c,d)", /* 116 */
3168  "F = 03DC(a,b,c,d)", /* 117 */
3169  "F = 03DD(a,b,c,d)", /* 118 */
3170  "F = 03DE(a,b,c,d)", /* 119 */
3171  "F = (d+!(!c*!b))", /* 120 */
3172  "F = ((d+c)*(b+a))", /* 121 */
3173  "F = 0661(a,b,c,d)", /* 122 */
3174  "F = 0662(a,b,c,d)", /* 123 */
3175  "F = 0663(a,b,c,d)", /* 124 */
3176  "F = (!(d*c)*(b+a))", /* 125 */
3177  "F = 0667(a,b,c,d)", /* 126 */
3178  "F = 29((b+a),c,d)", /* 127 */
3179  "F = 066B(a,b,c,d)", /* 128 */
3180  "F = 2B((b+a),c,d)", /* 129 */
3181  "F = 0672(a,b,c,d)", /* 130 */
3182  "F = 0673(a,b,c,d)", /* 131 */
3183  "F = 0676(a,b,c,d)", /* 132 */
3184  "F = 0678(a,b,c,d)", /* 133 */
3185  "F = 0679(a,b,c,d)", /* 134 */
3186  "F = 067A(a,b,c,d)", /* 135 */
3187  "F = 067B(a,b,c,d)", /* 136 */
3188  "F = 067E(a,b,c,d)", /* 137 */
3189  "F = 24((b+a),c,d)", /* 138 */
3190  "F = 0691(a,b,c,d)", /* 139 */
3191  "F = 0693(a,b,c,d)", /* 140 */
3192  "F = 26((b+a),c,d)", /* 141 */
3193  "F = 0697(a,b,c,d)", /* 142 */
3194  "F = !CA(d,c,(b+a))", /* 143 */
3195  "F = 06B0(a,b,c,d)", /* 144 */
3196  "F = 06B1(a,b,c,d)", /* 145 */
3197  "F = 06B2(a,b,c,d)", /* 146 */
3198  "F = 06B3(a,b,c,d)", /* 147 */
3199  "F = 06B4(a,b,c,d)", /* 148 */
3200  "F = 06B5(a,b,c,d)", /* 149 */
3201  "F = 06B6(a,b,c,d)", /* 150 */
3202  "F = 06B7(a,b,c,d)", /* 151 */
3203  "F = 06B9(a,b,c,d)", /* 152 */
3204  "F = 06BD(a,b,c,d)", /* 153 */
3205  "F = 2C((b+a),c,d)", /* 154 */
3206  "F = 06F1(a,b,c,d)", /* 155 */
3207  "F = 06F2(a,b,c,d)", /* 156 */
3208  "F = CA((b+a),!d,c)", /* 157 */
3209  "F = (d+!(!c*!(b+!a)))", /* 158 */
3210  "F = 0776(a,b,c,d)", /* 159 */
3211  "F = 16((b*a),c,d)", /* 160 */
3212  "F = 0779(a,b,c,d)", /* 161 */
3213  "F = 077A(a,b,c,d)", /* 162 */
3214  "F = 077E(a,b,c,d)", /* 163 */
3215  "F = 07B0(a,b,c,d)", /* 164 */
3216  "F = 07B1(a,b,c,d)", /* 165 */
3217  "F = 07B4(a,b,c,d)", /* 166 */
3218  "F = 07B5(a,b,c,d)", /* 167 */
3219  "F = 07B6(a,b,c,d)", /* 168 */
3220  "F = 07BC(a,b,c,d)", /* 169 */
3221  "F = 07E0(a,b,c,d)", /* 170 */
3222  "F = 07E1(a,b,c,d)", /* 171 */
3223  "F = 07E2(a,b,c,d)", /* 172 */
3224  "F = 07E3(a,b,c,d)", /* 173 */
3225  "F = 07E6(a,b,c,d)", /* 174 */
3226  "F = 07E9(a,b,c,d)", /* 175 */
3227  "F = 1C((b*a),c,d)", /* 176 */
3228  "F = 07F1(a,b,c,d)", /* 177 */
3229  "F = 07F2(a,b,c,d)", /* 178 */
3230  "F = (d+!(!c*!(b*a)))", /* 179 */
3231  "F = (d+c)", /* 180 */
3232  "F = 1668(a,b,c,d)", /* 181 */
3233  "F = 1669(a,b,c,d)", /* 182 */
3234  "F = 166A(a,b,c,d)", /* 183 */
3235  "F = 166B(a,b,c,d)", /* 184 */
3236  "F = 166E(a,b,c,d)", /* 185 */
3237  "F = 167E(a,b,c,d)", /* 186 */
3238  "F = 1681(a,b,c,d)", /* 187 */
3239  "F = 1683(a,b,c,d)", /* 188 */
3240  "F = 1686(a,b,c,d)", /* 189 */
3241  "F = 1687(a,b,c,d)", /* 190 */
3242  "F = 1689(a,b,c,d)", /* 191 */
3243  "F = 168B(a,b,c,d)", /* 192 */
3244  "F = 168E(a,b,c,d)", /* 193 */
3245  "F = 1696(a,b,c,d)", /* 194 */
3246  "F = 1697(a,b,c,d)", /* 195 */
3247  "F = 1698(a,b,c,d)", /* 196 */
3248  "F = 1699(a,b,c,d)", /* 197 */
3249  "F = 169A(a,b,c,d)", /* 198 */
3250  "F = 169B(a,b,c,d)", /* 199 */
3251  "F = 169E(a,b,c,d)", /* 200 */
3252  "F = 16A9(a,b,c,d)", /* 201 */
3253  "F = 16AC(a,b,c,d)", /* 202 */
3254  "F = 16AD(a,b,c,d)", /* 203 */
3255  "F = 16BC(a,b,c,d)", /* 204 */
3256  "F = (d+E9(a,b,c))", /* 205 */
3257  "F = 177E(a,b,c,d)", /* 206 */
3258  "F = 178E(a,b,c,d)", /* 207 */
3259  "F = 1796(a,b,c,d)", /* 208 */
3260  "F = 1798(a,b,c,d)", /* 209 */
3261  "F = 179A(a,b,c,d)", /* 210 */
3262  "F = 17AC(a,b,c,d)", /* 211 */
3263  "F = (d+E8(a,b,c))", /* 212 */
3264  "F = (d+E7(a,b,c))", /* 213 */
3265  "F = 19E1(a,b,c,d)", /* 214 */
3266  "F = 19E3(a,b,c,d)", /* 215 */
3267  "F = (d+E6(a,b,c))", /* 216 */
3268  "F = 1BD8(a,b,c,d)", /* 217 */
3269  "F = (d+CA(b,c,a))", /* 218 */
3270  "F = (d+(c+(!b*!a)))", /* 219 */
3271  "F = (d+(c+!b))", /* 220 */
3272  "F = (d+(c+(b+a)))" /* 221 */
3273  };
3274  return (char **)pNames;
3275 }
3276 
3277 
3278 ////////////////////////////////////////////////////////////////////////
3279 /// END OF FILE ///
3280 ////////////////////////////////////////////////////////////////////////
3281 
3282 
3283 ABC_NAMESPACE_IMPL_END
3284 
Kit_DsdExpand
Kit_DsdNtk_t * Kit_DsdExpand(Kit_DsdNtk_t *p)
Definition: kitDsd.c:1451
memset
char * memset()
Kit_DsdObj_t_::Type
unsigned Type
Definition: kit.h:112
Kit_DsdCheckVar4Dec2
int Kit_DsdCheckVar4Dec2(Kit_DsdNtk_t *pNtk0, Kit_DsdNtk_t *pNtk1)
Definition: kitDsd.c:1948
Kit_DsdObj_t_::fMark
unsigned fMark
Definition: kit.h:113
Kit_TruthAndPhase
static void Kit_TruthAndPhase(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars, int fCompl0, int fCompl1)
Definition: kit.h:409
Kit_DsdWriteFromTruth
void Kit_DsdWriteFromTruth(char *pBuffer, unsigned *pTruth, int nVars)
Definition: kitDsd.c:536
Kit_TruthBestCofVar
int Kit_TruthBestCofVar(unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
Definition: kitTruth.c:1365
Cloud_Quit
void Cloud_Quit(CloudManager *dd)
Definition: cloud.c:144
KIT_MAX
#define KIT_MAX(a, b)
Definition: kit.h:172
Kit_DsdNtkRoot
static Kit_DsdObj_t * Kit_DsdNtkRoot(Kit_DsdNtk_t *pNtk)
Definition: kit.h:151
Kit_DsdExpandNode_rec
int Kit_DsdExpandNode_rec(Kit_DsdNtk_t *pNew, Kit_DsdNtk_t *p, int iLit)
Definition: kitDsd.c:1349
Kit_DsdObjOffset
static unsigned Kit_DsdObjOffset(int nFans)
Definition: kit.h:147
KIT_INFINITY
#define KIT_INFINITY
Definition: kit.h:173
Kit_DsdTruthComputeOne
unsigned * Kit_DsdTruthComputeOne(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp)
Definition: kitDsd.c:823
Kit_DsdObj_t_::nRefs
unsigned nRefs
Definition: kit.h:115
Kit_DsdNpn4ClassNames
char ** Kit_DsdNpn4ClassNames()
Definition: kitDsd.c:3048
KIT_MIN
#define KIT_MIN(a, b)
MACRO DEFINITIONS ///.
Definition: kit.h:171
Kit_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
Kit_DsdObj_t_::Offset
unsigned Offset
Definition: kit.h:114
Kit_DsdShrink_rec
int Kit_DsdShrink_rec(Kit_DsdNtk_t *pNew, Kit_DsdNtk_t *p, int iLit, int pPrios[])
Definition: kitDsd.c:1543
pFreqs
static int pFreqs[13719]
Definition: rwrTemp.c:31
Kit_DsdNtkAlloc
Kit_DsdNtk_t * Kit_DsdNtkAlloc(int nVars)
Definition: kitDsd.c:140
Cloud_Init
CloudManager * Cloud_Init(int nVars, int nBits)
FUNCTION DEFINITIONS ///.
Definition: cloud.c:70
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition: kitDsd.c:490
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Kit_TruthSwapAdjacentVars
void Kit_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int Start)
DECLARATIONS ///.
Definition: kitTruth.c:46
Kit_TruthFill
static void Kit_TruthFill(unsigned *pOut, int nVars)
Definition: kit.h:367
Kit_DsdObj_t
struct Kit_DsdObj_t_ Kit_DsdObj_t
Definition: kit.h:108
Kit_DsdPrintFromTruth2
void Kit_DsdPrintFromTruth2(FILE *pFile, unsigned *pTruth, int nVars)
Definition: kitDsd.c:514
Kit_DsdObj_t_::nFans
unsigned nFans
Definition: kit.h:116
Kit_DsdVerify
void Kit_DsdVerify(Kit_DsdNtk_t *pNtk, unsigned *pTruth, int nVars)
Definition: kitDsd.c:2492
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Kit_DsdNonDsdSupports
unsigned Kit_DsdNonDsdSupports(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1264
Kit_DsdDecomposeInt
Kit_DsdNtk_t * Kit_DsdDecomposeInt(unsigned *pTruth, int nVars, int nDecMux)
Definition: kitDsd.c:2266
Kit_DsdNtk_t_::pNodes
Kit_DsdObj_t ** pNodes
Definition: kit.h:130
Kit_DsdFindLargeBox_rec
int Kit_DsdFindLargeBox_rec(Kit_DsdNtk_t *pNtk, int Id, int Size)
Definition: kitDsd.c:1797
Kit_DsdNtkObj
static Kit_DsdObj_t * Kit_DsdNtkObj(Kit_DsdNtk_t *pNtk, int Id)
Definition: kit.h:150
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Kit_DsdMan_t_::nVars
int nVars
Definition: kit.h:137
Kit_TruthCompose
unsigned * Kit_TruthCompose(CloudManager *dd, unsigned *pTruth, int nVars, unsigned **pInputs, int nVarsAll, Vec_Ptr_t *vStore, Vec_Int_t *vNodes)
Definition: kitCloud.c:263
Kit_TruthChangePhase
void Kit_TruthChangePhase(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:1259
Extra_BubbleSort
void Extra_BubbleSort(int Order[], int Costs[], int nSize, int fIncreasing)
Definition: extraUtilMisc.c:2044
Kit_DsdNtk_t_::Root
unsigned short Root
Definition: kit.h:127
Kit_DsdObj_t_::Id
unsigned Id
Definition: kit.h:111
Kit_TruthMuxVar
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition: kitTruth.c:1069
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Kit_TruthIsEqual
static int Kit_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:274
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Kit_DsdExpandCollectXor_rec
void Kit_DsdExpandCollectXor_rec(Kit_DsdNtk_t *p, unsigned iLit, unsigned *piLitsNew, int *nLitsNew)
Definition: kitDsd.c:1318
Kit_DsdMan_t_
Definition: kit.h:135
Kit_DsdNtk_t_::pMem
unsigned * pMem
Definition: kit.h:128
Kit_DsdObjAlloc
Kit_DsdObj_t * Kit_DsdObjAlloc(Kit_DsdNtk_t *pNtk, Kit_Dsd_t Type, int nFans)
Definition: kitDsd.c:92
Kit_DsdObjForEachFanin
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition: kit.h:157
Kit_DsdGetSupports
unsigned Kit_DsdGetSupports(Kit_DsdNtk_t *p)
Definition: kitDsd.c:1762
nWords
int nWords
Definition: abcNpn.c:127
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Kit_DsdWrite_rec
char * Kit_DsdWrite_rec(char *pBuff, Kit_DsdNtk_t *pNtk, int Id)
Definition: kitDsd.c:394
Kit_DsdTestCofs
int Kit_DsdTestCofs(Kit_DsdNtk_t *pNtk, unsigned *pTruthInit)
Definition: kitDsd.c:2387
Kit_DsdTruthComputeNodeOne_rec
unsigned * Kit_DsdTruthComputeNodeOne_rec(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id, unsigned uSupp)
Definition: kitDsd.c:690
Kit_DsdTruthCompute
unsigned * Kit_DsdTruthCompute(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:663
Kit_DsdNtk_t_
Definition: kit.h:122
Kit_DsdObj_t_
Definition: kit.h:109
Kit_DsdPrint
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:374
Kit_DsdPrint2_rec
void Kit_DsdPrint2_rec(FILE *pFile, Kit_DsdNtk_t *pNtk, int Id)
Definition: kitDsd.c:237
Kit_DsdTruthComputeNode_rec
unsigned * Kit_DsdTruthComputeNode_rec(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id)
Definition: kitDsd.c:560
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
Vec_PtrAllocTruthTables
static Vec_Ptr_t * Vec_PtrAllocTruthTables(int nVars)
Definition: vecPtr.h:1065
Kit_DsdWriteHex
char * Kit_DsdWriteHex(char *pBuff, unsigned *pTruth, int nFans)
Definition: kitDsd.c:211
Kit_DsdCofactoring
int Kit_DsdCofactoring(unsigned *pTruth, int nVars, int *pCofVars, int nLimit, int fVerbose)
Definition: kitDsd.c:2678
Kit_DsdEval
int Kit_DsdEval(unsigned *pTruth, int nVars, int nLutSize)
Definition: kitDsd.c:2456
Kit_TruthIsConst1
static int Kit_TruthIsConst1(unsigned *pIn, int nVars)
Definition: kit.h:323
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Kit_DsdNtkForEachObj
#define Kit_DsdNtkForEachObj(pNtk, pObj, i)
Definition: kit.h:155
Kit_TruthXor
static void Kit_TruthXor(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:391
Kit_DsdPrint_rec
void Kit_DsdPrint_rec(FILE *pFile, Kit_DsdNtk_t *pNtk, int Id)
Definition: kitDsd.c:317
Kit_DsdPrecompute4Vars
void Kit_DsdPrecompute4Vars()
Definition: kitDsd.c:2565
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Kit_DsdMan_t_::vTtBdds
Vec_Ptr_t * vTtBdds
Definition: kit.h:143
Kit_DsdWrite
void Kit_DsdWrite(char *pBuff, Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:452
Kit_DsdPrintHex
void Kit_DsdPrintHex(FILE *pFile, unsigned *pTruth, int nFans)
Definition: kitDsd.c:186
Kit_DsdMan_t_::vTtElems
Vec_Ptr_t * vTtElems
Definition: kit.h:139
Kit_DsdDecompose
Kit_DsdNtk_t * Kit_DsdDecompose(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2314
Kit_DsdTruthPartial
void Kit_DsdTruthPartial(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned *pTruthRes, unsigned uSupp)
Definition: kitDsd.c:1107
Kit_Dsd_t
Kit_Dsd_t
Definition: kit.h:98
Kit_DsdObjTruth
static unsigned * Kit_DsdObjTruth(Kit_DsdObj_t *pObj)
Definition: kit.h:148
Kit_DsdTruthPartialTwo
void Kit_DsdTruthPartialTwo(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec)
Definition: kitDsd.c:1089
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
Kit_DsdObjFree
void Kit_DsdObjFree(Kit_DsdNtk_t *p, Kit_DsdObj_t *pObj)
Definition: kitDsd.c:124
Kit_DsdPrint2
void Kit_DsdPrint2(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:297
Kit_DsdMan_t_::dd
CloudManager * dd
Definition: kit.h:142
Kit_DsdNtk_t_::pSupps
unsigned * pSupps
Definition: kit.h:129
Kit_DsdNtk_t_::nNodesAlloc
unsigned short nNodesAlloc
Definition: kit.h:125
sprintf
char * sprintf()
Kit_DsdManFree
void Kit_DsdManFree(Kit_DsdMan_t *p)
Definition: kitDsd.c:71
Kit_DsdTruthComputeTwo
unsigned * Kit_DsdTruthComputeTwo(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthDec)
Definition: kitDsd.c:1024
Counter
static int Counter
Definition: extraBddMisc.c:1877
Kit_DsdTruth
void Kit_DsdTruth(Kit_DsdNtk_t *pNtk, unsigned *pTruthRes)
Definition: kitDsd.c:1068
Kit_DsdCofactoringGetVars
int Kit_DsdCofactoringGetVars(Kit_DsdNtk_t **ppNtk, int nSize, int *pVars)
Definition: kitDsd.c:2632
Kit_DsdManAlloc
ABC_NAMESPACE_IMPL_START Kit_DsdMan_t * Kit_DsdManAlloc(int nVars, int nNodes)
DECLARATIONS ///.
Definition: kitDsd.c:45
Kit_DsdTruthComputeNodeTwo_rec
unsigned * Kit_DsdTruthComputeNodeTwo_rec(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id, unsigned uSupp, int iVar, unsigned *pTruthDec)
Definition: kitDsd.c:853
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Extra_ReadHexadecimal
int Extra_ReadHexadecimal(unsigned Sign[], char *pString, int nVars)
Definition: extraUtilFile.c:540
Kit_DsdObj_t_::pFans
unsigned short pFans[0]
Definition: kit.h:117
Kit_DsdCountAigNodes_rec
int Kit_DsdCountAigNodes_rec(Kit_DsdNtk_t *pNtk, int Id)
Definition: kitDsd.c:1839
Kit_DsdFindLargeBox
int Kit_DsdFindLargeBox(Kit_DsdNtk_t *pNtk, int Size)
Definition: kitDsd.c:1823
Kit_TruthIthVar
static void Kit_TruthIthVar(unsigned *pTruth, int nVars, int iVar)
Definition: kit.h:473
Kit_DsdNonDsdSizeMax
int Kit_DsdNonDsdSizeMax(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1211
Extra_TruthIsEqual
static int Extra_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: extra.h:270
Kit_DsdRotate
void Kit_DsdRotate(Kit_DsdNtk_t *p, int pFreqs[])
Definition: kitDsd.c:1671
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Kit_DsdCountAigNodes
int Kit_DsdCountAigNodes(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1895
Kit_TruthShrink
void Kit_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition: kitTruth.c:200
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Kit_DsdCompSort
void Kit_DsdCompSort(int pPrios[], unsigned uSupps[], unsigned short *piLits, int nVars, unsigned piLitsRes[])
Definition: kitDsd.c:1488
Kit_DsdGetSupports_rec
unsigned Kit_DsdGetSupports_rec(Kit_DsdNtk_t *p, int iLit)
Definition: kitDsd.c:1735
Kit_DsdTest
void Kit_DsdTest(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2514
Kit_DsdDecompose_rec
void Kit_DsdDecompose_rec(Kit_DsdNtk_t *pNtk, Kit_DsdObj_t *pObj, unsigned uSupp, unsigned short *pPar, int nDecMux)
Definition: kitDsd.c:1970
Kit_WordFindFirstBit
static int Kit_WordFindFirstBit(unsigned uWord)
Definition: kit.h:231
Kit_TruthIsOpposite
static int Kit_TruthIsOpposite(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:290
Kit_DsdExpandCollectAnd_rec
void Kit_DsdExpandCollectAnd_rec(Kit_DsdNtk_t *p, unsigned iLit, unsigned *piLitsNew, int *nLitsNew)
Definition: kitDsd.c:1291
Kit_DsdCountLuts
int Kit_DsdCountLuts(Kit_DsdNtk_t *pNtk, int nLutSize)
Definition: kitDsd.c:1187
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Kit_DsdMan_t_::vNodes
Vec_Int_t * vNodes
Definition: kit.h:144
Kit_DsdRootNodeHasCommonVars
int Kit_DsdRootNodeHasCommonVars(Kit_DsdObj_t *pObj0, Kit_DsdObj_t *pObj1)
Definition: kitDsd.c:1923
Kit_TruthSupport
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition: kitTruth.c:346
Kit_DsdNtk_t_::nNodes
unsigned short nNodes
Definition: kit.h:126
Kit_TruthCopy
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
Kit_DsdLitIsLeaf
static int Kit_DsdLitIsLeaf(Kit_DsdNtk_t *pNtk, int Lit)
Definition: kit.h:152
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Minisat::Var
int Var
Definition: SolverTypes.h:42
Kit_DsdNtkFree
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:163
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:270
Kit_DsdMan_t_::vTtNodes
Vec_Ptr_t * vTtNodes
Definition: kit.h:140
Kit_DsdDecomposeMux
Kit_DsdNtk_t * Kit_DsdDecomposeMux(unsigned *pTruth, int nVars, int nDecMux)
Definition: kitDsd.c:2350
Kit_DsdDecomposeExpand
Kit_DsdNtk_t * Kit_DsdDecomposeExpand(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2330
Kit_DsdNtkObjNum
static int Kit_DsdNtkObjNum(Kit_DsdNtk_t *pNtk)
Definition: kit.h:149
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Kit_DsdCountAigNodes2
int Kit_DsdCountAigNodes2(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1879
Kit_WordCountOnes
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
Extra_PrintHexadecimal
void Extra_PrintHexadecimal(FILE *pFile, unsigned Sign[], int nVars)
Definition: extraUtilFile.c:565
Kit_DsdLitSupport
static unsigned Kit_DsdLitSupport(Kit_DsdNtk_t *pNtk, int Lit)
Definition: kit.h:153
Kit_DsdCountLuts_rec
int Kit_DsdCountLuts_rec(Kit_DsdNtk_t *pNtk, int nLutSize, int Id, int *pCounter)
Definition: kitDsd.c:1143
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Kit_DsdNonDsdPrimeMax
Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1236
Kit_DsdPrintCofactors
void Kit_DsdPrintCofactors(unsigned *pTruth, int nVars, int nCofLevel, int fVerbose)
Definition: kitDsd.c:2803
Kit_DsdShrink
Kit_DsdNtk_t * Kit_DsdShrink(Kit_DsdNtk_t *p, int pPrios[])
Definition: kitDsd.c:1633
Kit_DsdPrintExpanded
void Kit_DsdPrintExpanded(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:471
Kit_TruthClear
static void Kit_TruthClear(unsigned *pOut, int nVars)
Definition: kit.h:361
Kit_DsdNtk_t_::nVars
unsigned short nVars
Definition: kit.h:124
Kit_TruthSupportSize
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition: kitTruth.c:327
Kit_DsdMan_t_::nWords
int nWords
Definition: kit.h:138
Kit_BitMask
static unsigned Kit_BitMask(int nBits)
Definition: kit.h:225
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223