abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dsdTree.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [dsdTree.c]
4 
5  PackageName [DSD: Disjoint-support decomposition package.]
6 
7  Synopsis [Managing the decomposition tree.]
8 
9  Author [Alan Mishchenko]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 8.0. Started - September 22, 2003.]
14 
15  Revision [$Id: dsdTree.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "dsdInt.h"
20 #include "misc/util/utilTruth.h"
21 #include "opt/dau/dau.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// FUNCTION DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static void Dsd_TreeUnmark_rec( Dsd_Node_t * pNode );
31 static void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur );
32 static int Dsd_TreeCountNonTerminalNodes_rec( Dsd_Node_t * pNode );
33 static int Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode );
34 static int Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars );
35 static void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes );
36 static void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fCcmp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames );
37 static void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter );
38 
39 ////////////////////////////////////////////////////////////////////////
40 /// STATIC VARIABLES ///
41 ////////////////////////////////////////////////////////////////////////
42 
43 static int s_DepthMax;
44 static int s_GateSizeMax;
45 
46 ////////////////////////////////////////////////////////////////////////
47 /// FUNCTION DEFINITIONS ///
48 ////////////////////////////////////////////////////////////////////////
49 
50 /**Function*************************************************************
51 
52  Synopsis [Create the DSD node.]
53 
54  Description []
55 
56  SideEffects []
57 
58  SeeAlso []
59 
60 ***********************************************************************/
61 Dsd_Node_t * Dsd_TreeNodeCreate( int Type, int nDecs, int BlockNum )
62 {
63  // allocate memory for this node
64  Dsd_Node_t * p = (Dsd_Node_t *) ABC_ALLOC( char, sizeof(Dsd_Node_t) );
65  memset( p, 0, sizeof(Dsd_Node_t) );
66  p->Type = (Dsd_Type_t)Type; // the type of this block
67  p->nDecs = nDecs; // the number of decompositions
68  if ( p->nDecs )
69  {
70  p->pDecs = (Dsd_Node_t **) ABC_ALLOC( char, p->nDecs * sizeof(Dsd_Node_t *) );
71  p->pDecs[0] = NULL;
72  }
73  return p;
74 }
75 
76 /**Function*************************************************************
77 
78  Synopsis [Frees the DSD node.]
79 
80  Description []
81 
82  SideEffects []
83 
84  SeeAlso []
85 
86 ***********************************************************************/
87 void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode )
88 {
89  if ( pNode->G ) Cudd_RecursiveDeref( dd, pNode->G );
90  if ( pNode->S ) Cudd_RecursiveDeref( dd, pNode->S );
91  ABC_FREE( pNode->pDecs );
92  ABC_FREE( pNode );
93 }
94 
95 /**Function*************************************************************
96 
97  Synopsis [Unmarks the decomposition tree.]
98 
99  Description [This function assumes that originally pNode->nVisits are
100  set to zero!]
101 
102  SideEffects []
103 
104  SeeAlso []
105 
106 ***********************************************************************/
107 void Dsd_TreeUnmark( Dsd_Manager_t * pDsdMan )
108 {
109  int i;
110  for ( i = 0; i < pDsdMan->nRoots; i++ )
111  Dsd_TreeUnmark_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
112 }
113 
114 
115 /**Function*************************************************************
116 
117  Synopsis [Recursive unmarking.]
118 
119  Description [This function should be called with a non-complemented
120  pointer.]
121 
122  SideEffects []
123 
124  SeeAlso []
125 
126 ***********************************************************************/
127 void Dsd_TreeUnmark_rec( Dsd_Node_t * pNode )
128 {
129  int i;
130 
131  assert( pNode );
132  assert( !Dsd_IsComplement( pNode ) );
133  assert( pNode->nVisits > 0 );
134 
135  if ( --pNode->nVisits ) // if this is not the last visit, return
136  return;
137 
138  // upon the last visit, go through the list of successors and call recursively
139  if ( pNode->Type != DSD_NODE_BUF && pNode->Type != DSD_NODE_CONST1 )
140  for ( i = 0; i < pNode->nDecs; i++ )
141  Dsd_TreeUnmark_rec( Dsd_Regular(pNode->pDecs[i]) );
142 }
143 
144 /**Function*************************************************************
145 
146  Synopsis [Getting information about the node.]
147 
148  Description [This function computes the max depth and the max gate size
149  of the tree rooted at the node.]
150 
151  SideEffects []
152 
153  SeeAlso []
154 
155 ***********************************************************************/
156 void Dsd_TreeNodeGetInfo( Dsd_Manager_t * pDsdMan, int * DepthMax, int * GateSizeMax )
157 {
158  int i;
159  s_DepthMax = 0;
160  s_GateSizeMax = 0;
161 
162  for ( i = 0; i < pDsdMan->nRoots; i++ )
163  Dsd_TreeGetInfo_rec( Dsd_Regular( pDsdMan->pRoots[i] ), 0 );
164 
165  if ( DepthMax )
166  *DepthMax = s_DepthMax;
167  if ( GateSizeMax )
168  *GateSizeMax = s_GateSizeMax;
169 }
170 
171 /**Function*************************************************************
172 
173  Synopsis [Getting information about the node.]
174 
175  Description [This function computes the max depth and the max gate size
176  of the tree rooted at the node.]
177 
178  SideEffects []
179 
180  SeeAlso []
181 
182 ***********************************************************************/
183 void Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax )
184 {
185  s_DepthMax = 0;
186  s_GateSizeMax = 0;
187 
188  Dsd_TreeGetInfo_rec( Dsd_Regular(pNode), 0 );
189 
190  if ( DepthMax )
191  *DepthMax = s_DepthMax;
192  if ( GateSizeMax )
193  *GateSizeMax = s_GateSizeMax;
194 }
195 
196 
197 /**Function*************************************************************
198 
199  Synopsis [Performs the recursive step of Dsd_TreeNodeGetInfo().]
200 
201  Description [pNode is the node, for the tree rooted in which we are
202  determining info. RankCur is the current rank to assign to the node.
203  fSetRank is the flag saying whether the rank will be written in the
204  node. s_DepthMax is the maximum depths of the tree. s_GateSizeMax is
205  the maximum gate size.]
206 
207  SideEffects []
208 
209  SeeAlso []
210 
211 ***********************************************************************/
212 void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur )
213 {
214  int i;
215  int GateSize;
216 
217  assert( pNode );
218  assert( !Dsd_IsComplement( pNode ) );
219  assert( pNode->nVisits >= 0 );
220 
221  // we don't want the two-input gates to count for non-decomposable blocks
222  if ( pNode->Type == DSD_NODE_OR ||
223  pNode->Type == DSD_NODE_EXOR )
224  GateSize = 2;
225  else
226  GateSize = pNode->nDecs;
227 
228  // update the max size of the node
229  if ( s_GateSizeMax < GateSize )
230  s_GateSizeMax = GateSize;
231 
232  if ( pNode->nDecs < 2 )
233  return;
234 
235  // update the max rank
236  if ( s_DepthMax < RankCur+1 )
237  s_DepthMax = RankCur+1;
238 
239  // call recursively
240  for ( i = 0; i < pNode->nDecs; i++ )
241  Dsd_TreeGetInfo_rec( Dsd_Regular(pNode->pDecs[i]), RankCur+1 );
242 }
243 
244 /**Function*************************************************************
245 
246  Synopsis [Counts AIG nodes needed to implement this node.]
247 
248  Description []
249 
250  SideEffects []
251 
252  SeeAlso []
253 
254 ***********************************************************************/
255 int Dsd_TreeGetAigCost_rec( Dsd_Node_t * pNode )
256 {
257  int i, Counter = 0;
258 
259  assert( pNode );
260  assert( !Dsd_IsComplement( pNode ) );
261  assert( pNode->nVisits >= 0 );
262 
263  if ( pNode->nDecs < 2 )
264  return 0;
265 
266  // we don't want the two-input gates to count for non-decomposable blocks
267  if ( pNode->Type == DSD_NODE_OR )
268  Counter += pNode->nDecs - 1;
269  else if ( pNode->Type == DSD_NODE_EXOR )
270  Counter += 3*(pNode->nDecs - 1);
271  else if ( pNode->Type == DSD_NODE_PRIME && pNode->nDecs == 3 )
272  Counter += 3;
273 
274  // call recursively
275  for ( i = 0; i < pNode->nDecs; i++ )
276  Counter += Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode->pDecs[i]) );
277  return Counter;
278 }
279 
280 /**Function*************************************************************
281 
282  Synopsis [Counts AIG nodes needed to implement this node.]
283 
284  Description [Assumes that the only primes of the DSD tree are MUXes.]
285 
286  SideEffects []
287 
288  SeeAlso []
289 
290 ***********************************************************************/
291 int Dsd_TreeGetAigCost( Dsd_Node_t * pNode )
292 {
293  return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) );
294 }
295 
296 /**Function*************************************************************
297 
298  Synopsis [Counts non-terminal nodes of the DSD tree.]
299 
300  Description [Nonterminal nodes include all the nodes with the
301  support more than 1. These are OR, EXOR, and PRIME nodes. They
302  do not include the elementary variable nodes and the constant 1
303  node.]
304 
305  SideEffects []
306 
307  SeeAlso []
308 
309 ***********************************************************************/
310 int Dsd_TreeCountNonTerminalNodes( Dsd_Manager_t * pDsdMan )
311 {
312  int Counter, i;
313  Counter = 0;
314  for ( i = 0; i < pDsdMan->nRoots; i++ )
315  Counter += Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
316  Dsd_TreeUnmark( pDsdMan );
317  return Counter;
318 }
319 
320 /**Function*************************************************************
321 
322  Synopsis []
323 
324  Description []
325 
326  SideEffects []
327 
328  SeeAlso []
329 
330 ***********************************************************************/
331 int Dsd_TreeCountNonTerminalNodesOne( Dsd_Node_t * pRoot )
332 {
333  int Counter = 0;
334 
335  // go through the list of successors and call recursively
336  Counter = Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular(pRoot) );
337 
338  Dsd_TreeUnmark_rec( Dsd_Regular(pRoot) );
339  return Counter;
340 }
341 
342 
343 /**Function*************************************************************
344 
345  Synopsis [Counts non-terminal nodes for one root.]
346 
347  Description []
348 
349  SideEffects []
350 
351  SeeAlso []
352 
353 ***********************************************************************/
354 int Dsd_TreeCountNonTerminalNodes_rec( Dsd_Node_t * pNode )
355 {
356  int i;
357  int Counter = 0;
358 
359  assert( pNode );
360  assert( !Dsd_IsComplement( pNode ) );
361  assert( pNode->nVisits >= 0 );
362 
363  if ( pNode->nVisits++ ) // if this is not the first visit, return zero
364  return 0;
365 
366  if ( pNode->nDecs <= 1 )
367  return 0;
368 
369  // upon the first visit, go through the list of successors and call recursively
370  for ( i = 0; i < pNode->nDecs; i++ )
371  Counter += Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular(pNode->pDecs[i]) );
372 
373  return Counter + 1;
374 }
375 
376 
377 /**Function*************************************************************
378 
379  Synopsis [Counts prime nodes of the DSD tree.]
380 
381  Description [Prime nodes are nodes with the support more than 2,
382  that is not an OR or EXOR gate.]
383 
384  SideEffects []
385 
386  SeeAlso []
387 
388 ***********************************************************************/
389 int Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan )
390 {
391  int Counter, i;
392  Counter = 0;
393  for ( i = 0; i < pDsdMan->nRoots; i++ )
394  Counter += Dsd_TreeCountPrimeNodes_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
395  Dsd_TreeUnmark( pDsdMan );
396  return Counter;
397 }
398 
399 /**Function*************************************************************
400 
401  Synopsis [Counts prime nodes for one root.]
402 
403  Description []
404 
405  SideEffects []
406 
407  SeeAlso []
408 
409 ***********************************************************************/
410 int Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot )
411 {
412  int Counter = 0;
413 
414  // go through the list of successors and call recursively
415  Counter = Dsd_TreeCountPrimeNodes_rec( Dsd_Regular(pRoot) );
416 
417  Dsd_TreeUnmark_rec( Dsd_Regular(pRoot) );
418  return Counter;
419 }
420 
421 
422 /**Function*************************************************************
423 
424  Synopsis []
425 
426  Description []
427 
428  SideEffects []
429 
430  SeeAlso []
431 
432 ***********************************************************************/
433 int Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode )
434 {
435  int i;
436  int Counter = 0;
437 
438  assert( pNode );
439  assert( !Dsd_IsComplement( pNode ) );
440  assert( pNode->nVisits >= 0 );
441 
442  if ( pNode->nVisits++ ) // if this is not the first visit, return zero
443  return 0;
444 
445  if ( pNode->nDecs <= 1 )
446  return 0;
447 
448  // upon the first visit, go through the list of successors and call recursively
449  for ( i = 0; i < pNode->nDecs; i++ )
450  Counter += Dsd_TreeCountPrimeNodes_rec( Dsd_Regular(pNode->pDecs[i]) );
451 
452  if ( pNode->Type == DSD_NODE_PRIME )
453  Counter++;
454 
455  return Counter;
456 }
457 
458 
459 /**Function*************************************************************
460 
461  Synopsis [Collects the decomposable vars on the PI side.]
462 
463  Description []
464 
465  SideEffects []
466 
467  SeeAlso []
468 
469 ***********************************************************************/
470 int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * pDsdMan, int * pVars )
471 {
472  int nVars;
473 
474  // set the vars collected to 0
475  nVars = 0;
476  Dsd_TreeCollectDecomposableVars_rec( pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[0]), pVars, &nVars );
477  // return the number of collected vars
478  return nVars;
479 }
480 
481 /**Function*************************************************************
482 
483  Synopsis [Implements the recursive part of Dsd_TreeCollectDecomposableVars().]
484 
485  Description [Adds decomposable variables as they are found to pVars and increments
486  nVars. Returns 1 if a non-dec node with more than 4 inputs was encountered
487  in the processed subtree. Returns 0, otherwise. ]
488 
489  SideEffects []
490 
491  SeeAlso []
492 
493 ***********************************************************************/
494 int Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars )
495 {
496  int fSkipThisNode, i;
497  Dsd_Node_t * pTemp;
498  int fVerbose = 0;
499 
500  assert( pNode );
501  assert( !Dsd_IsComplement( pNode ) );
502 
503  if ( pNode->nDecs <= 1 )
504  return 0;
505 
506  // go through the list of successors and call recursively
507  fSkipThisNode = 0;
508  for ( i = 0; i < pNode->nDecs; i++ )
509  if ( Dsd_TreeCollectDecomposableVars_rec(dd, Dsd_Regular(pNode->pDecs[i]), pVars, nVars) )
510  fSkipThisNode = 1;
511 
512  if ( !fSkipThisNode && (pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR || pNode->nDecs <= 4) )
513  {
514 if ( fVerbose )
515 printf( "Node of type <%d> (OR=6,EXOR=8,RAND=1): ", pNode->Type );
516 
517  for ( i = 0; i < pNode->nDecs; i++ )
518  {
519  pTemp = Dsd_Regular(pNode->pDecs[i]);
520  if ( pTemp->Type == DSD_NODE_BUF )
521  {
522  if ( pVars )
523  pVars[ (*nVars)++ ] = pTemp->S->index;
524  else
525  (*nVars)++;
526 
527 if ( fVerbose )
528 printf( "%d ", pTemp->S->index );
529  }
530  }
531 if ( fVerbose )
532 printf( "\n" );
533  }
534  else
535  fSkipThisNode = 1;
536 
537 
538  return fSkipThisNode;
539 }
540 
541 
542 /**Function*************************************************************
543 
544  Synopsis [Creates the DFS ordered array of DSD nodes in the tree.]
545 
546  Description [The collected nodes do not include the terminal nodes
547  and the constant 1 node. The array of nodes is returned. The number
548  of entries in the array is returned in the variale pnNodes.]
549 
550  SideEffects []
551 
552  SeeAlso []
553 
554 ***********************************************************************/
555 Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * pDsdMan, int * pnNodes )
556 {
557  Dsd_Node_t ** ppNodes;
558  int nNodes, nNodesAlloc;
559  int i;
560 
561  nNodesAlloc = Dsd_TreeCountNonTerminalNodes(pDsdMan);
562  nNodes = 0;
563  ppNodes = ABC_ALLOC( Dsd_Node_t *, nNodesAlloc );
564  for ( i = 0; i < pDsdMan->nRoots; i++ )
565  Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pDsdMan->pRoots[i]), ppNodes, &nNodes );
566  Dsd_TreeUnmark( pDsdMan );
567  assert( nNodesAlloc == nNodes );
568  *pnNodes = nNodes;
569  return ppNodes;
570 }
571 
572 /**Function*************************************************************
573 
574  Synopsis [Creates the DFS ordered array of DSD nodes in the tree.]
575 
576  Description [The collected nodes do not include the terminal nodes
577  and the constant 1 node. The array of nodes is returned. The number
578  of entries in the array is returned in the variale pnNodes.]
579 
580  SideEffects []
581 
582  SeeAlso []
583 
584 ***********************************************************************/
585 Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes )
586 {
587  Dsd_Node_t ** ppNodes;
588  int nNodes, nNodesAlloc;
589  nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode);
590  nNodes = 0;
591  ppNodes = ABC_ALLOC( Dsd_Node_t *, nNodesAlloc );
592  Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes );
593  Dsd_TreeUnmark_rec(Dsd_Regular(pNode));
594  assert( nNodesAlloc == nNodes );
595  *pnNodes = nNodes;
596  return ppNodes;
597 }
598 
599 
600 /**Function*************************************************************
601 
602  Synopsis []
603 
604  Description []
605 
606  SideEffects []
607 
608  SeeAlso []
609 
610 ***********************************************************************/
611 void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes )
612 {
613  int i;
614  assert( pNode );
615  assert( !Dsd_IsComplement(pNode) );
616  assert( pNode->nVisits >= 0 );
617 
618  if ( pNode->nVisits++ ) // if this is not the first visit, return zero
619  return;
620  if ( pNode->nDecs <= 1 )
621  return;
622 
623  // upon the first visit, go through the list of successors and call recursively
624  for ( i = 0; i < pNode->nDecs; i++ )
625  Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode->pDecs[i]), ppNodes, pnNodes );
626 
627  ppNodes[ (*pnNodes)++ ] = pNode;
628 }
629 
630 /**Function*************************************************************
631 
632  Synopsis [Prints the decompostion tree into file.]
633 
634  Description []
635 
636  SideEffects []
637 
638  SeeAlso []
639 
640 ***********************************************************************/
641 void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output )
642 {
643  Dsd_Node_t * pNode;
644  int SigCounter;
645  int i;
646  SigCounter = 1;
647 
648  if ( Output == -1 )
649  {
650  for ( i = 0; i < pDsdMan->nRoots; i++ )
651  {
652  pNode = Dsd_Regular( pDsdMan->pRoots[i] );
653  Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[i]), pInputNames, pOutputNames[i], 0, &SigCounter, fShortNames );
654  }
655  }
656  else
657  {
658  assert( Output >= 0 && Output < pDsdMan->nRoots );
659  pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
660  Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[Output]), pInputNames, pOutputNames[Output], 0, &SigCounter, fShortNames );
661  }
662 }
663 
664 /**Function*************************************************************
665 
666  Synopsis [Prints the decompostion tree into file.]
667 
668  Description []
669 
670  SideEffects []
671 
672  SeeAlso []
673 
674 ***********************************************************************/
675 void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames )
676 {
677  char Buffer[100];
678  Dsd_Node_t * pInput;
679  int * pInputNums;
680  int fCompNew, i;
681 
682  assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 ||
683  pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR );
684 
685  Extra_PrintSymbols( pFile, ' ', nOffset, 0 );
686  if ( !fComp )
687  fprintf( pFile, "%s = ", pOutputName );
688  else
689  fprintf( pFile, "NOT(%s) = ", pOutputName );
690  pInputNums = ABC_ALLOC( int, pNode->nDecs );
691  if ( pNode->Type == DSD_NODE_CONST1 )
692  {
693  fprintf( pFile, " Constant 1.\n" );
694  }
695  else if ( pNode->Type == DSD_NODE_BUF )
696  {
697  if ( fShortNames )
698  fprintf( pFile, "%d", 'a' + pNode->S->index );
699  else
700  fprintf( pFile, "%s", pInputNames[pNode->S->index] );
701  fprintf( pFile, "\n" );
702  }
703  else if ( pNode->Type == DSD_NODE_PRIME )
704  {
705  // print the line
706  fprintf( pFile, "PRIME(" );
707  for ( i = 0; i < pNode->nDecs; i++ )
708  {
709  pInput = Dsd_Regular( pNode->pDecs[i] );
710  fCompNew = (int)( pInput != pNode->pDecs[i] );
711  if ( i )
712  fprintf( pFile, "," );
713  if ( fCompNew )
714  fprintf( pFile, " NOT(" );
715  else
716  fprintf( pFile, " " );
717  if ( pInput->Type == DSD_NODE_BUF )
718  {
719  pInputNums[i] = 0;
720  if ( fShortNames )
721  fprintf( pFile, "%d", pInput->S->index );
722  else
723  fprintf( pFile, "%s", pInputNames[pInput->S->index] );
724  }
725  else
726  {
727  pInputNums[i] = (*pSigCounter)++;
728  fprintf( pFile, "<%d>", pInputNums[i] );
729  }
730  if ( fCompNew )
731  fprintf( pFile, ")" );
732  }
733  fprintf( pFile, " )\n" );
734  // call recursively for the following blocks
735  for ( i = 0; i < pNode->nDecs; i++ )
736  if ( pInputNums[i] )
737  {
738  pInput = Dsd_Regular( pNode->pDecs[i] );
739  sprintf( Buffer, "<%d>", pInputNums[i] );
740  Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
741  }
742  }
743  else if ( pNode->Type == DSD_NODE_OR )
744  {
745  // print the line
746  fprintf( pFile, "OR(" );
747  for ( i = 0; i < pNode->nDecs; i++ )
748  {
749  pInput = Dsd_Regular( pNode->pDecs[i] );
750  fCompNew = (int)( pInput != pNode->pDecs[i] );
751  if ( i )
752  fprintf( pFile, "," );
753  if ( fCompNew )
754  fprintf( pFile, " NOT(" );
755  else
756  fprintf( pFile, " " );
757  if ( pInput->Type == DSD_NODE_BUF )
758  {
759  pInputNums[i] = 0;
760  if ( fShortNames )
761  fprintf( pFile, "%c", 'a' + pInput->S->index );
762  else
763  fprintf( pFile, "%s", pInputNames[pInput->S->index] );
764  }
765  else
766  {
767  pInputNums[i] = (*pSigCounter)++;
768  fprintf( pFile, "<%d>", pInputNums[i] );
769  }
770  if ( fCompNew )
771  fprintf( pFile, ")" );
772  }
773  fprintf( pFile, " )\n" );
774  // call recursively for the following blocks
775  for ( i = 0; i < pNode->nDecs; i++ )
776  if ( pInputNums[i] )
777  {
778  pInput = Dsd_Regular( pNode->pDecs[i] );
779  sprintf( Buffer, "<%d>", pInputNums[i] );
780  Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
781  }
782  }
783  else if ( pNode->Type == DSD_NODE_EXOR )
784  {
785  // print the line
786  fprintf( pFile, "EXOR(" );
787  for ( i = 0; i < pNode->nDecs; i++ )
788  {
789  pInput = Dsd_Regular( pNode->pDecs[i] );
790  fCompNew = (int)( pInput != pNode->pDecs[i] );
791  if ( i )
792  fprintf( pFile, "," );
793  if ( fCompNew )
794  fprintf( pFile, " NOT(" );
795  else
796  fprintf( pFile, " " );
797  if ( pInput->Type == DSD_NODE_BUF )
798  {
799  pInputNums[i] = 0;
800  if ( fShortNames )
801  fprintf( pFile, "%c", 'a' + pInput->S->index );
802  else
803  fprintf( pFile, "%s", pInputNames[pInput->S->index] );
804  }
805  else
806  {
807  pInputNums[i] = (*pSigCounter)++;
808  fprintf( pFile, "<%d>", pInputNums[i] );
809  }
810  if ( fCompNew )
811  fprintf( pFile, ")" );
812  }
813  fprintf( pFile, " )\n" );
814  // call recursively for the following blocks
815  for ( i = 0; i < pNode->nDecs; i++ )
816  if ( pInputNums[i] )
817  {
818  pInput = Dsd_Regular( pNode->pDecs[i] );
819  sprintf( Buffer, "<%d>", pInputNums[i] );
820  Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
821  }
822  }
823  ABC_FREE( pInputNums );
824 }
825 
826 /**Function*************************************************************
827 
828  Synopsis [Prints the decompostion tree into file.]
829 
830  Description []
831 
832  SideEffects []
833 
834  SeeAlso []
835 
836 ***********************************************************************/
837 word Dsd_TreeFunc2Truth_rec( DdManager * dd, DdNode * bFunc )
838 {
839  word Cof0, Cof1;
840  int Level;
841  if ( bFunc == b0 )
842  return 0;
843  if ( bFunc == b1 )
844  return ~(word)0;
845  if ( Cudd_IsComplement(bFunc) )
846  return ~Dsd_TreeFunc2Truth_rec( dd, Cudd_Not(bFunc) );
847  Level = dd->perm[bFunc->index];
848  assert( Level >= 0 && Level < 6 );
849  Cof0 = Dsd_TreeFunc2Truth_rec( dd, cuddE(bFunc) );
850  Cof1 = Dsd_TreeFunc2Truth_rec( dd, cuddT(bFunc) );
851  return (s_Truths6[Level] & Cof1) | (~s_Truths6[Level] & Cof0);
852 }
853 void Dsd_TreePrint2_rec( FILE * pFile, DdManager * dd, Dsd_Node_t * pNode, int fComp, char * pInputNames[] )
854 {
855  int i;
856  if ( pNode->Type == DSD_NODE_CONST1 )
857  {
858  fprintf( pFile, "Const%d", !fComp );
859  return;
860  }
861  assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR );
862 // fprintf( pFile, "%s", (fComp ^ (pNode->Type == DSD_NODE_OR))? "!" : "" );
863  if ( pNode->Type == DSD_NODE_BUF )
864  {
865  fprintf( pFile, "%s", fComp? "!" : "" );
866  fprintf( pFile, "%s", pInputNames[pNode->S->index] );
867  }
868  else if ( pNode->Type == DSD_NODE_PRIME )
869  {
870  fprintf( pFile, " " );
871  if ( pNode->nDecs <= 6 )
872  {
873  char pCanonPerm[6]; int uCanonPhase;
874  // compute truth table
875  DdNode * bFunc = Dsd_TreeGetPrimeFunction( dd, pNode );
876  word uTruth = Dsd_TreeFunc2Truth_rec( dd, bFunc );
877  Cudd_Ref( bFunc );
878  Cudd_RecursiveDeref( dd, bFunc );
879  // canonicize truth table
880  uCanonPhase = Abc_TtCanonicize( &uTruth, pNode->nDecs, pCanonPerm );
881  fprintf( pFile, "%s", (fComp ^ ((uCanonPhase >> pNode->nDecs) & 1)) ? "!" : "" );
882  Abc_TtPrintHexRev( pFile, &uTruth, pNode->nDecs );
883  fprintf( pFile, "{" );
884  for ( i = 0; i < pNode->nDecs; i++ )
885  {
886  Dsd_Node_t * pInput = pNode->pDecs[(int)pCanonPerm[i]];
887  Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pInput), Dsd_IsComplement(pInput) ^ ((uCanonPhase>>i)&1), pInputNames );
888  }
889  fprintf( pFile, "} " );
890  }
891  else
892  {
893  fprintf( pFile, "|%d|", pNode->nDecs );
894  fprintf( pFile, "{" );
895  for ( i = 0; i < pNode->nDecs; i++ )
896  Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
897  fprintf( pFile, "} " );
898  }
899  }
900  else if ( pNode->Type == DSD_NODE_OR )
901  {
902  fprintf( pFile, "%s", !fComp? "!" : "" );
903  fprintf( pFile, "(" );
904  for ( i = 0; i < pNode->nDecs; i++ )
905  Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), !Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
906  fprintf( pFile, ")" );
907  }
908  else if ( pNode->Type == DSD_NODE_EXOR )
909  {
910  fprintf( pFile, "%s", fComp? "!" : "" );
911  fprintf( pFile, "[" );
912  for ( i = 0; i < pNode->nDecs; i++ )
913  Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
914  fprintf( pFile, "]" );
915  }
916 }
917 void Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int Output )
918 {
919  if ( Output == -1 )
920  {
921  int i;
922  for ( i = 0; i < pDsdMan->nRoots; i++ )
923  {
924  fprintf( pFile, "%8s = ", pOutputNames[i] );
925  Dsd_TreePrint2_rec( pFile, pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[i]), Dsd_IsComplement(pDsdMan->pRoots[i]), pInputNames );
926  fprintf( pFile, "\n" );
927  }
928  }
929  else
930  {
931  assert( Output >= 0 && Output < pDsdMan->nRoots );
932  fprintf( pFile, "%8s = ", pOutputNames[Output] );
933  Dsd_TreePrint2_rec( pFile, pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[Output]), Dsd_IsComplement(pDsdMan->pRoots[Output]), pInputNames );
934  fprintf( pFile, "\n" );
935  }
936 }
937 
938 /**Function*************************************************************
939 
940  Synopsis [Prints the decompostion tree into file.]
941 
942  Description []
943 
944  SideEffects []
945 
946  SeeAlso []
947 
948 ***********************************************************************/
949 void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode )
950 {
951  Dsd_Node_t * pNodeR;
952  int SigCounter = 1;
953  pNodeR = Dsd_Regular(pNode);
954  Dsd_NodePrint_rec( pFile, pNodeR, pNodeR != pNode, "F", 0, &SigCounter );
955 }
956 
957 /**Function*************************************************************
958 
959  Synopsis [Prints one node of the decomposition tree.]
960 
961  Description []
962 
963  SideEffects []
964 
965  SeeAlso []
966 
967 ***********************************************************************/
968 void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter )
969 {
970  char Buffer[100];
971  Dsd_Node_t * pInput;
972  int * pInputNums;
973  int fCompNew, i;
974 
975  assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 ||
976  pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR );
977 
978  Extra_PrintSymbols( pFile, ' ', nOffset, 0 );
979  if ( !fComp )
980  fprintf( pFile, "%s = ", pOutputName );
981  else
982  fprintf( pFile, "NOT(%s) = ", pOutputName );
983  pInputNums = ABC_ALLOC( int, pNode->nDecs );
984  if ( pNode->Type == DSD_NODE_CONST1 )
985  {
986  fprintf( pFile, " Constant 1.\n" );
987  }
988  else if ( pNode->Type == DSD_NODE_BUF )
989  {
990  fprintf( pFile, " " );
991  fprintf( pFile, "%c", 'a' + pNode->S->index );
992  fprintf( pFile, "\n" );
993  }
994  else if ( pNode->Type == DSD_NODE_PRIME )
995  {
996  // print the line
997  fprintf( pFile, "PRIME(" );
998  for ( i = 0; i < pNode->nDecs; i++ )
999  {
1000  pInput = Dsd_Regular( pNode->pDecs[i] );
1001  fCompNew = (int)( pInput != pNode->pDecs[i] );
1002  assert( fCompNew == 0 );
1003  if ( i )
1004  fprintf( pFile, "," );
1005  if ( pInput->Type == DSD_NODE_BUF )
1006  {
1007  pInputNums[i] = 0;
1008  fprintf( pFile, " %c", 'a' + pInput->S->index );
1009  }
1010  else
1011  {
1012  pInputNums[i] = (*pSigCounter)++;
1013  fprintf( pFile, " <%d>", pInputNums[i] );
1014  }
1015  if ( fCompNew )
1016  fprintf( pFile, "\'" );
1017  }
1018  fprintf( pFile, " )\n" );
1019 /*
1020  fprintf( pFile, " ) " );
1021  {
1022  DdNode * bLocal;
1023  bLocal = Dsd_TreeGetPrimeFunction( dd, pNodeDsd ); Cudd_Ref( bLocal );
1024  Extra_bddPrint( dd, bLocal );
1025  Cudd_RecursiveDeref( dd, bLocal );
1026  }
1027 */
1028  // call recursively for the following blocks
1029  for ( i = 0; i < pNode->nDecs; i++ )
1030  if ( pInputNums[i] )
1031  {
1032  pInput = Dsd_Regular( pNode->pDecs[i] );
1033  sprintf( Buffer, "<%d>", pInputNums[i] );
1034  Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
1035  }
1036  }
1037  else if ( pNode->Type == DSD_NODE_OR )
1038  {
1039  // print the line
1040  fprintf( pFile, "OR(" );
1041  for ( i = 0; i < pNode->nDecs; i++ )
1042  {
1043  pInput = Dsd_Regular( pNode->pDecs[i] );
1044  fCompNew = (int)( pInput != pNode->pDecs[i] );
1045  if ( i )
1046  fprintf( pFile, "," );
1047  if ( pInput->Type == DSD_NODE_BUF )
1048  {
1049  pInputNums[i] = 0;
1050  fprintf( pFile, " %c", 'a' + pInput->S->index );
1051  }
1052  else
1053  {
1054  pInputNums[i] = (*pSigCounter)++;
1055  fprintf( pFile, " <%d>", pInputNums[i] );
1056  }
1057  if ( fCompNew )
1058  fprintf( pFile, "\'" );
1059  }
1060  fprintf( pFile, " )\n" );
1061  // call recursively for the following blocks
1062  for ( i = 0; i < pNode->nDecs; i++ )
1063  if ( pInputNums[i] )
1064  {
1065  pInput = Dsd_Regular( pNode->pDecs[i] );
1066  sprintf( Buffer, "<%d>", pInputNums[i] );
1067  Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
1068  }
1069  }
1070  else if ( pNode->Type == DSD_NODE_EXOR )
1071  {
1072  // print the line
1073  fprintf( pFile, "EXOR(" );
1074  for ( i = 0; i < pNode->nDecs; i++ )
1075  {
1076  pInput = Dsd_Regular( pNode->pDecs[i] );
1077  fCompNew = (int)( pInput != pNode->pDecs[i] );
1078  assert( fCompNew == 0 );
1079  if ( i )
1080  fprintf( pFile, "," );
1081  if ( pInput->Type == DSD_NODE_BUF )
1082  {
1083  pInputNums[i] = 0;
1084  fprintf( pFile, " %c", 'a' + pInput->S->index );
1085  }
1086  else
1087  {
1088  pInputNums[i] = (*pSigCounter)++;
1089  fprintf( pFile, " <%d>", pInputNums[i] );
1090  }
1091  if ( fCompNew )
1092  fprintf( pFile, "\'" );
1093  }
1094  fprintf( pFile, " )\n" );
1095  // call recursively for the following blocks
1096  for ( i = 0; i < pNode->nDecs; i++ )
1097  if ( pInputNums[i] )
1098  {
1099  pInput = Dsd_Regular( pNode->pDecs[i] );
1100  sprintf( Buffer, "<%d>", pInputNums[i] );
1101  Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
1102  }
1103  }
1104  ABC_FREE( pInputNums );
1105 }
1106 
1107 
1108 /**Function*************************************************************
1109 
1110  Synopsis [Retuns the function of one node of the decomposition tree.]
1111 
1112  Description [This is the old procedure. It is now superceded by the
1113  procedure Dsd_TreeGetPrimeFunction() found in "dsdLocal.c".]
1114 
1115  SideEffects []
1116 
1117  SeeAlso []
1118 
1119 ***********************************************************************/
1120 DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap )
1121 {
1122  DdNode * bCof0, * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp;
1123  int i;
1124  static int Permute[MAXINPUTS];
1125 
1126  assert( pNode );
1127  assert( !Dsd_IsComplement( pNode ) );
1128  assert( pNode->Type == DSD_NODE_PRIME );
1129 
1130  // transform the function of this block to depend on inputs
1131  // corresponding to the formal inputs
1132 
1133  // first, substitute those inputs that have some blocks associated with them
1134  // second, remap the inputs to the top of the manager (then, it is easy to output them)
1135 
1136  // start the function
1137  bNewFunc = pNode->G; Cudd_Ref( bNewFunc );
1138  // go over all primary inputs
1139  for ( i = 0; i < pNode->nDecs; i++ )
1140  if ( pNode->pDecs[i]->Type != DSD_NODE_BUF ) // remap only if it is not the buffer
1141  {
1142  bCube0 = Extra_bddFindOneCube( dd, Cudd_Not(pNode->pDecs[i]->G) ); Cudd_Ref( bCube0 );
1143  bCof0 = Cudd_Cofactor( dd, bNewFunc, bCube0 ); Cudd_Ref( bCof0 );
1144  Cudd_RecursiveDeref( dd, bCube0 );
1145 
1146  bCube1 = Extra_bddFindOneCube( dd, pNode->pDecs[i]->G ); Cudd_Ref( bCube1 );
1147  bCof1 = Cudd_Cofactor( dd, bNewFunc, bCube1 ); Cudd_Ref( bCof1 );
1148  Cudd_RecursiveDeref( dd, bCube1 );
1149 
1150  Cudd_RecursiveDeref( dd, bNewFunc );
1151 
1152  // use the variable in the i-th level of the manager
1153 // bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 ); Cudd_Ref( bNewFunc );
1154  // use the first variale in the support of the component
1155  bNewFunc = Cudd_bddIte( dd, dd->vars[pNode->pDecs[i]->S->index],bCof1,bCof0 ); Cudd_Ref( bNewFunc );
1156  Cudd_RecursiveDeref( dd, bCof0 );
1157  Cudd_RecursiveDeref( dd, bCof1 );
1158  }
1159 
1160  if ( fRemap )
1161  {
1162  // remap the function to the top of the manager
1163  // remap the function to the first variables of the manager
1164  for ( i = 0; i < pNode->nDecs; i++ )
1165  // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
1166  Permute[ pNode->pDecs[i]->S->index ] = i;
1167 
1168  bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute ); Cudd_Ref( bNewFunc );
1169  Cudd_RecursiveDeref( dd, bTemp );
1170  }
1171 
1172  Cudd_Deref( bNewFunc );
1173  return bNewFunc;
1174 }
1175 
1176 
1177 ////////////////////////////////////////////////////////////////////////
1178 /// END OF FILE ///
1179 ////////////////////////////////////////////////////////////////////////
1180 ABC_NAMESPACE_IMPL_END
1181 
memset
char * memset()
Dsd_TreeNodeGetInfoOne
void Dsd_TreeNodeGetInfoOne(Dsd_Node_t *pNode, int *DepthMax, int *GateSizeMax)
Definition: dsdTree.c:183
Dsd_TreePrint
void Dsd_TreePrint(FILE *pFile, Dsd_Manager_t *pDsdMan, char *pInputNames[], char *pOutputNames[], int fShortNames, int Output)
Definition: dsdTree.c:641
Dsd_Node_t_::S
DdNode * S
Definition: dsdInt.h:58
Dsd_TreePrint2
void Dsd_TreePrint2(FILE *pFile, Dsd_Manager_t *pDsdMan, char *pInputNames[], char *pOutputNames[], int Output)
Definition: dsdTree.c:917
s_DepthMax
static int s_DepthMax
STATIC VARIABLES ///.
Definition: dsdTree.c:43
Dsd_Manager_t_::dd
DdManager * dd
Definition: dsdInt.h:42
s_GateSizeMax
static int s_GateSizeMax
Definition: dsdTree.c:44
Dsd_TreePrint_rec
static void Dsd_TreePrint_rec(FILE *pFile, Dsd_Node_t *pNode, int fCcmp, char *pInputNames[], char *pOutputName, int nOffset, int *pSigCounter, int fShortNames)
Definition: dsdTree.c:675
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dsd_Node_t_::G
DdNode * G
Definition: dsdInt.h:57
Dsd_TreeCountNonTerminalNodes_rec
static int Dsd_TreeCountNonTerminalNodes_rec(Dsd_Node_t *pNode)
Definition: dsdTree.c:354
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Dsd_TreeGetAigCost
int Dsd_TreeGetAigCost(Dsd_Node_t *pNode)
Definition: dsdTree.c:291
MAXINPUTS
#define MAXINPUTS
INCLUDES ///.
Definition: cas.h:38
Abc_TtPrintHexRev
static void Abc_TtPrintHexRev(FILE *pFile, word *pTruth, int nVars)
Definition: utilTruth.h:789
b1
#define b1
Definition: extraBdd.h:76
Dsd_TreeUnmark
void Dsd_TreeUnmark(Dsd_Manager_t *pDsdMan)
Definition: dsdTree.c:107
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
Dsd_Node_t_::pDecs
Dsd_Node_t ** pDecs
Definition: dsdInt.h:59
Dsd_TreeCountPrimeNodes
int Dsd_TreeCountPrimeNodes(Dsd_Manager_t *pDsdMan)
Definition: dsdTree.c:389
Dsd_TreeCollectNodesDfs_rec
static void Dsd_TreeCollectNodesDfs_rec(Dsd_Node_t *pNode, Dsd_Node_t *ppNodes[], int *pnNodes)
Definition: dsdTree.c:611
Dsd_TreeNodeCreate
Dsd_Node_t * Dsd_TreeNodeCreate(int Type, int nDecs, int BlockNum)
FUNCTION DEFINITIONS ///.
Definition: dsdTree.c:61
Extra_PrintSymbols
void Extra_PrintSymbols(FILE *pFile, char Char, int nTimes, int fPrintNewLine)
Definition: extraUtilFile.c:668
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
Dsd_NodePrint_rec
static void Dsd_NodePrint_rec(FILE *pFile, Dsd_Node_t *pNode, int fComp, char *pOutputName, int nOffset, int *pSigCounter)
Definition: dsdTree.c:968
Cudd_Cofactor
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
Dsd_TreeCountPrimeNodes_rec
static int Dsd_TreeCountPrimeNodes_rec(Dsd_Node_t *pNode)
Definition: dsdTree.c:433
Cudd_bddPermute
DdNode * Cudd_bddPermute(DdManager *manager, DdNode *node, int *permut)
Definition: cuddCompose.c:332
Dsd_TreeCollectNodesDfsOne
Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne(Dsd_Manager_t *pDsdMan, Dsd_Node_t *pNode, int *pnNodes)
Definition: dsdTree.c:585
Dsd_TreeGetPrimeFunctionOld
DdNode * Dsd_TreeGetPrimeFunctionOld(DdManager *dd, Dsd_Node_t *pNode, int fRemap)
Definition: dsdTree.c:1120
Dsd_TreeCollectDecomposableVars_rec
static int Dsd_TreeCollectDecomposableVars_rec(DdManager *dd, Dsd_Node_t *pNode, int *pVars, int *nVars)
Definition: dsdTree.c:494
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Dsd_Manager_t_
STRUCTURE DEFINITIONS ///.
Definition: dsdInt.h:40
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
Dsd_Node_t_
Definition: dsdInt.h:54
Dsd_TreeCountNonTerminalNodes
int Dsd_TreeCountNonTerminalNodes(Dsd_Manager_t *pDsdMan)
Definition: dsdTree.c:310
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
Dsd_Regular
#define Dsd_Regular(p)
Definition: dsd.h:69
Dsd_Node_t_::Type
Dsd_Type_t Type
Definition: dsdInt.h:56
Extra_bddFindOneCube
DdNode * Extra_bddFindOneCube(DdManager *dd, DdNode *bF)
Definition: extraBddMisc.c:605
Dsd_IsComplement
#define Dsd_IsComplement(p)
MACRO DEFINITIONS ///.
Definition: dsd.h:68
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Dsd_TreeGetPrimeFunction
DdNode * Dsd_TreeGetPrimeFunction(DdManager *dd, Dsd_Node_t *pNode)
FUNCTION DEFINITIONS ///.
Definition: dsdLocal.c:54
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
Dsd_TreeCountPrimeNodesOne
int Dsd_TreeCountPrimeNodesOne(Dsd_Node_t *pRoot)
Definition: dsdTree.c:410
Dsd_TreeUnmark_rec
static ABC_NAMESPACE_IMPL_START void Dsd_TreeUnmark_rec(Dsd_Node_t *pNode)
FUNCTION DECLARATIONS ///.
Definition: dsdTree.c:127
Dsd_TreeCountNonTerminalNodesOne
int Dsd_TreeCountNonTerminalNodesOne(Dsd_Node_t *pRoot)
Definition: dsdTree.c:331
Dsd_TreeCollectNodesDfs
Dsd_Node_t ** Dsd_TreeCollectNodesDfs(Dsd_Manager_t *pDsdMan, int *pnNodes)
Definition: dsdTree.c:555
b0
#define b0
Definition: extraBdd.h:75
DdNode::index
DdHalfWord index
Definition: cudd.h:279
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
Abc_TtCanonicize
unsigned Abc_TtCanonicize(word *pTruth, int nVars, char *pCanonPerm)
FUNCTION DECLARATIONS ///.
Definition: dauCanon.c:895
Dsd_TreeGetAigCost_rec
int Dsd_TreeGetAigCost_rec(Dsd_Node_t *pNode)
Definition: dsdTree.c:255
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
assert
#define assert(ex)
Definition: util_old.h:213
Dsd_Type_t
enum Dsd_Type_t_ Dsd_Type_t
Definition: dsd.h:61
Dsd_TreeNodeGetInfo
void Dsd_TreeNodeGetInfo(Dsd_Manager_t *pDsdMan, int *DepthMax, int *GateSizeMax)
Definition: dsdTree.c:156
Dsd_TreeNodeDelete
void Dsd_TreeNodeDelete(DdManager *dd, Dsd_Node_t *pNode)
Definition: dsdTree.c:87
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Dsd_TreeCollectDecomposableVars
int Dsd_TreeCollectDecomposableVars(Dsd_Manager_t *pDsdMan, int *pVars)
Definition: dsdTree.c:470
Dsd_TreeFunc2Truth_rec
word Dsd_TreeFunc2Truth_rec(DdManager *dd, DdNode *bFunc)
Definition: dsdTree.c:837
Dsd_TreeGetInfo_rec
static void Dsd_TreeGetInfo_rec(Dsd_Node_t *pNode, int RankCur)
Definition: dsdTree.c:212
Dsd_NodePrint
void Dsd_NodePrint(FILE *pFile, Dsd_Node_t *pNode)
Definition: dsdTree.c:949
Dsd_Manager_t_::nRoots
int nRoots
Definition: dsdInt.h:45
DdManager::perm
int * perm
Definition: cuddInt.h:386
Dsd_TreePrint2_rec
void Dsd_TreePrint2_rec(FILE *pFile, DdManager *dd, Dsd_Node_t *pNode, int fComp, char *pInputNames[])
Definition: dsdTree.c:853
Dsd_Node_t_::nVisits
short nVisits
Definition: dsdInt.h:62
Dsd_Manager_t_::pRoots
Dsd_Node_t ** pRoots
Definition: dsdInt.h:48
Dsd_Node_t_::nDecs
short nDecs
Definition: dsdInt.h:61