abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dsdProc.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [dsdProc.c]
4 
5  PackageName [DSD: Disjoint-support decomposition package.]
6 
7  Synopsis [The core procedures of the package.]
8 
9  Author [Alan Mishchenko]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 8.0. Started - September 22, 2003.]
14 
15  Revision [$Id: dsdProc.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "dsdInt.h"
20 
22 
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// FUNCTION DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 // the most important procedures
30 void dsdKernelDecompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs );
31 static Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * F );
32 
33 // additional procedures
34 static Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity );
35 static int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH );
36 static void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor );
37 static int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall );
38 
39 // list copying
40 static void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize );
41 static void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int Skipped );
42 
43 // debugging procedures
44 static int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE );
45 
46 ////////////////////////////////////////////////////////////////////////
47 /// STATIC VARIABLES ///
48 ////////////////////////////////////////////////////////////////////////
49 
50 // the counter of marks
51 static int s_Mark;
52 
53 // debugging flag
54 //static int s_Show = 0;
55 // temporary var used for debugging
56 static int Depth = 0;
57 
58 static int s_Loops1;
59 static int s_Loops2;
60 static int s_Loops3;
61 static int s_Common;
62 static int s_CommonNo;
63 
64 static int s_Case4Calls;
66 
67 //static int s_Case5;
68 //static int s_Loops2Useless;
69 
70 // statistical variables
71 static int s_nDecBlocks;
72 static int s_nLiterals;
73 static int s_nExorGates;
74 static int s_nReusedBlocks;
75 static int s_nCascades;
76 static int s_nPrimeBlocks;
77 
78 static int HashSuccess = 0;
79 static int HashFailure = 0;
80 
81 static int s_CacheEntries;
82 
83 
84 ////////////////////////////////////////////////////////////////////////
85 /// DECOMPOSITION FUNCTIONS ///
86 ////////////////////////////////////////////////////////////////////////
87 
88 /**Function*************************************************************
89 
90  Synopsis [Performs DSD for the array of functions represented by BDDs.]
91 
92  Description [This function takes the DSD manager, which should be
93  previously allocated by the call to Dsd_ManagerStart(). The resulting
94  DSD tree is stored in the DSD manager (pDsdMan->pRoots, pDsdMan->nRoots).
95  Access to the tree is through the APIs of the manager. The resulting
96  tree is a shared DSD DAG for the functions given in the array. For one
97  function the resulting DAG is always a tree. The root node pointers can
98  be complemented, as discussed in the literature referred to in "dsd.h".
99  This procedure can be called repeatedly for different functions. There is
100  no need to remove the decomposition tree after it is returned, because
101  the next call to the DSD manager will "recycle" the tree. The user should
102  not modify or dereference any data associated with the nodes of the
103  DSD trees (the user can only change the contents of a temporary
104  mark associated with each node by the calling to Dsd_NodeSetMark()).
105  All the decomposition trees and intermediate nodes will be removed when
106  the DSD manager is deallocated at the end by calling Dsd_ManagerStop().]
107 
108  SideEffects []
109 
110  SeeAlso []
111 
112 ***********************************************************************/
113 void Dsd_Decompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs )
114 {
115  DdManager * dd = pDsdMan->dd;
116  int i;
117  abctime clk;
118  Dsd_Node_t * pTemp;
119  int SumMaxGateSize = 0;
120  int nDecOutputs = 0;
121  int nCBFOutputs = 0;
122 /*
123 s_Loops1 = 0;
124 s_Loops2 = 0;
125 s_Loops3 = 0;
126 s_Case4Calls = 0;
127 s_Case4CallsSpecial = 0;
128 s_Case5 = 0;
129 s_Loops2Useless = 0;
130 */
131  // resize the number of roots in the manager
132  if ( pDsdMan->nRootsAlloc < nFuncs )
133  {
134  if ( pDsdMan->nRootsAlloc > 0 )
135  ABC_FREE( pDsdMan->pRoots );
136  pDsdMan->nRootsAlloc = nFuncs;
137  pDsdMan->pRoots = (Dsd_Node_t **) ABC_ALLOC( char, pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
138  }
139 
140  if ( pDsdMan->fVerbose )
141  printf( "\nDecomposability statistics for individual outputs:\n" );
142 
143  // set the counter of decomposition nodes
144  s_nDecBlocks = 0;
145 
146  // perform decomposition for all outputs
147  clk = Abc_Clock();
148  pDsdMan->nRoots = 0;
149  s_nCascades = 0;
150  for ( i = 0; i < nFuncs; i++ )
151  {
152  int nLiteralsPrev;
153  int nDecBlocksPrev;
154  int nExorGatesPrev;
155  int nReusedBlocksPres;
156  int nCascades;
157  int MaxBlock;
158  int nPrimeBlocks;
159  abctime clk;
160 
161  clk = Abc_Clock();
162  nLiteralsPrev = s_nLiterals;
163  nDecBlocksPrev = s_nDecBlocks;
164  nExorGatesPrev = s_nExorGates;
165  nReusedBlocksPres = s_nReusedBlocks;
166  nPrimeBlocks = s_nPrimeBlocks;
167 
168  pDsdMan->pRoots[ pDsdMan->nRoots++ ] = dsdKernelDecompose_rec( pDsdMan, pbFuncs[i] );
169 
170  Dsd_TreeNodeGetInfoOne( pDsdMan->pRoots[i], &nCascades, &MaxBlock );
171  s_nCascades = ddMax( s_nCascades, nCascades );
172  pTemp = Dsd_Regular(pDsdMan->pRoots[i]);
173  if ( pTemp->Type != DSD_NODE_PRIME || pTemp->nDecs != Extra_bddSuppSize(dd,pTemp->S) )
174  nDecOutputs++;
175  if ( MaxBlock < 3 )
176  nCBFOutputs++;
177  SumMaxGateSize += MaxBlock;
178 
179  if ( pDsdMan->fVerbose )
180  {
181  printf("#%02d: ", i );
182  printf("Ins=%2d. ", Cudd_SupportSize(dd,pbFuncs[i]) );
183  printf("Gts=%3d. ", Dsd_TreeCountNonTerminalNodesOne( pDsdMan->pRoots[i] ) );
184  printf("Pri=%3d. ", Dsd_TreeCountPrimeNodesOne( pDsdMan->pRoots[i] ) );
185  printf("Max=%3d. ", MaxBlock );
186  printf("Reuse=%2d. ", s_nReusedBlocks-nReusedBlocksPres );
187  printf("Csc=%2d. ", nCascades );
188  printf("T= %.2f s. ", (float)(Abc_Clock()-clk)/(float)(CLOCKS_PER_SEC) ) ;
189  printf("Bdd=%2d. ", Cudd_DagSize(pbFuncs[i]) );
190  printf("\n");
191  fflush( stdout );
192  }
193  }
194  assert( pDsdMan->nRoots == nFuncs );
195 
196  if ( pDsdMan->fVerbose )
197  {
198  printf( "\n" );
199  printf( "The cumulative decomposability statistics:\n" );
200  printf( " Total outputs = %5d\n", nFuncs );
201  printf( " Decomposable outputs = %5d\n", nDecOutputs );
202  printf( " Completely decomposable outputs = %5d\n", nCBFOutputs );
203  printf( " The sum of max gate sizes = %5d\n", SumMaxGateSize );
204  printf( " Shared BDD size = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) );
205  printf( " Decomposition entries = %5d\n", st__count( pDsdMan->Table ) );
206  printf( " Pure decomposition time = %.2f sec\n", (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC) );
207  }
208 /*
209  printf( "s_Loops1 = %d.\n", s_Loops1 );
210  printf( "s_Loops2 = %d.\n", s_Loops2 );
211  printf( "s_Loops3 = %d.\n", s_Loops3 );
212  printf( "s_Case4Calls = %d.\n", s_Case4Calls );
213  printf( "s_Case4CallsSpecial = %d.\n", s_Case4CallsSpecial );
214  printf( "s_Case5 = %d.\n", s_Case5 );
215  printf( "s_Loops2Useless = %d.\n", s_Loops2Useless );
216 */
217 }
218 
219 /**Function*************************************************************
220 
221  Synopsis [Performs decomposition for one function.]
222 
223  Description []
224 
225  SideEffects []
226 
227  SeeAlso []
228 
229 ***********************************************************************/
231 {
232  return dsdKernelDecompose_rec( pDsdMan, bFunc );
233 }
234 
235 /**Function*************************************************************
236 
237  Synopsis [The main function of this module. Recursive implementation of DSD.]
238 
239  Description []
240 
241  SideEffects []
242 
243  SeeAlso []
244 
245 ***********************************************************************/
247 {
248  DdManager * dd = pDsdMan->dd;
249  DdNode * bLow;
250  DdNode * bLowR;
251  DdNode * bHigh;
252 
253  int VarInt;
254  DdNode * bVarCur;
255  Dsd_Node_t * pVarCurDE;
256  // works only if var indices start from 0!!!
257  DdNode * bSuppNew = NULL, * bTemp;
258 
259  int fContained;
260  int nSuppLH;
261  int nSuppL;
262  int nSuppH;
263 
264 
265 
266  // various decomposition nodes
267  Dsd_Node_t * pThis, * pL, * pH, * pLR, * pHR;
268 
269  Dsd_Node_t * pSmallR, * pLargeR;
270  Dsd_Node_t * pTableEntry;
271 
272 
273  // treat the complemented case
274  DdNode * bF = Cudd_Regular(bFunc0);
275  int fCompF = (int)(bF != bFunc0);
276 
277  // check cache
278  if ( st__lookup( pDsdMan->Table, (char*)bF, (char**)&pTableEntry ) )
279  { // the entry is present
280  HashSuccess++;
281  return Dsd_NotCond( pTableEntry, fCompF );
282  }
283  HashFailure++;
284  Depth++;
285 
286  // proceed to consider "four cases"
287  //////////////////////////////////////////////////////////////////////
288  // TERMINAL CASES - CASES 1 and 2
289  //////////////////////////////////////////////////////////////////////
290  bLow = cuddE(bF);
291  bLowR = Cudd_Regular(bLow);
292  bHigh = cuddT(bF);
293  VarInt = bF->index;
294  bVarCur = dd->vars[VarInt];
295  pVarCurDE = pDsdMan->pInputs[VarInt];
296  // works only if var indices start from 0!!!
297  bSuppNew = NULL;
298 
299  if ( bLowR->index == CUDD_CONST_INDEX || bHigh->index == CUDD_CONST_INDEX )
300  { // one of the cofactors in the constant
301  if ( bHigh == b1 ) // bHigh cannot be equal to b0, because then it will be complemented
302  if ( bLow == b0 ) // bLow cannot be equal to b1, because then the node will have bLow == bHigh
303  /////////////////////////////////////////////////////////////////
304  // bLow == 0, bHigh == 1, F = x'&0 + x&1 = x
305  /////////////////////////////////////////////////////////////////
306  { // create the elementary variable node
307  assert(0); // should be already in the hash table
309  pThis->pDecs[0] = NULL;
310  }
311  else // if ( bLow != constant )
312  /////////////////////////////////////////////////////////////////
313  // bLow != const, bHigh == 1, F = x'&bLow + x&1 = bLow + x --- DSD_NODE_OR(x,bLow)
314  /////////////////////////////////////////////////////////////////
315  {
316  pL = dsdKernelDecompose_rec( pDsdMan, bLow );
317  pLR = Dsd_Regular( pL );
318  bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew);
319  if ( pLR->Type == DSD_NODE_OR && pL == pLR ) // OR and no complement
320  { // add to the components
321  pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pL->nDecs+1, s_nDecBlocks++ );
322  dsdKernelCopyListPlusOne( pThis, pVarCurDE, pL->pDecs, pL->nDecs );
323  }
324  else // all other cases
325  { // create a new 2-input OR-gate
327  dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 );
328  }
329  }
330  else // if ( bHigh != const ) // meaning that bLow should be a constant
331  {
332  pH = dsdKernelDecompose_rec( pDsdMan, bHigh );
333  pHR = Dsd_Regular( pH );
334  bSuppNew = Cudd_bddAnd( dd, bVarCur, pHR->S ); Cudd_Ref(bSuppNew);
335  if ( bLow == b0 )
336  /////////////////////////////////////////////////////////////////
337  // Low == 0, High != 1, F = x'&0+x&High = (x'+High')'--- NOR(x',High')
338  /////////////////////////////////////////////////////////////////
339  if ( pHR->Type == DSD_NODE_OR && pH != pHR ) // DSD_NODE_OR and complement
340  { // add to the components
341  pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pHR->nDecs+1, s_nDecBlocks++ );
342  dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pHR->pDecs, pHR->nDecs );
343  pThis = Dsd_Not(pThis);
344  }
345  else // all other cases
346  { // create a new 2-input NOR gate
348  pH = Dsd_Not(pH);
349  dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
350  pThis = Dsd_Not(pThis);
351  }
352  else // if ( bLow == b1 )
353  /////////////////////////////////////////////////////////////////
354  // Low == 1, High != 1, F = x'&1 + x&High = x' + High --- DSD_NODE_OR(x',High)
355  /////////////////////////////////////////////////////////////////
356  if ( pHR->Type == DSD_NODE_OR && pH == pHR ) // OR and no complement
357  { // add to the components
358  pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pH->nDecs+1, s_nDecBlocks++ );
359  dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pH->pDecs, pH->nDecs );
360  }
361  else // all other cases
362  { // create a new 2-input OR-gate
364  dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
365  }
366  }
367  goto EXIT;
368  }
369  // else if ( bLow != const && bHigh != const )
370 
371  // the case of equal cofactors (up to complementation)
372  if ( bLowR == bHigh )
373  /////////////////////////////////////////////////////////////////
374  // Low == G, High == G', F = x'&G + x&G' = (x(+)G) --- EXOR(x,Low)
375  /////////////////////////////////////////////////////////////////
376  {
377  pL = dsdKernelDecompose_rec( pDsdMan, bLow );
378  pLR = Dsd_Regular( pL );
379  bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew);
380  if ( pLR->Type == DSD_NODE_EXOR ) // complemented or not - does not matter!
381  { // add to the components
382  pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, pLR->nDecs+1, s_nDecBlocks++ );
383  dsdKernelCopyListPlusOne( pThis, pVarCurDE, pLR->pDecs, pLR->nDecs );
384  if ( pL != pLR )
385  pThis = Dsd_Not( pThis );
386  }
387  else // all other cases
388  { // create a new 2-input EXOR-gate
390  if ( pL != pLR ) // complemented
391  {
392  dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pLR, 1 );
393  pThis = Dsd_Not( pThis );
394  }
395  else // non-complemented
396  dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 );
397  }
398  goto EXIT;
399  }
400 
401  //////////////////////////////////////////////////////////////////////
402  // solve subproblems
403  //////////////////////////////////////////////////////////////////////
404  pL = dsdKernelDecompose_rec( pDsdMan, bLow );
405  pH = dsdKernelDecompose_rec( pDsdMan, bHigh );
406  pLR = Dsd_Regular( pL );
407  pHR = Dsd_Regular( pH );
408 
409  assert( pLR->Type == DSD_NODE_BUF || pLR->Type == DSD_NODE_OR || pLR->Type == DSD_NODE_EXOR || pLR->Type == DSD_NODE_PRIME );
410  assert( pHR->Type == DSD_NODE_BUF || pHR->Type == DSD_NODE_OR || pHR->Type == DSD_NODE_EXOR || pHR->Type == DSD_NODE_PRIME );
411 
412 /*
413 if ( Depth == 1 )
414 {
415 // PRK(bLow,pDecTreeTotal->nInputs);
416 // PRK(bHigh,pDecTreeTotal->nInputs);
417 if ( s_Show )
418 {
419  PRD( pL );
420  PRD( pH );
421 }
422 }
423 */
424  // compute the new support
425  bTemp = Cudd_bddAnd( dd, pLR->S, pHR->S ); Cudd_Ref( bTemp );
426  nSuppL = Extra_bddSuppSize( dd, pLR->S );
427  nSuppH = Extra_bddSuppSize( dd, pHR->S );
428  nSuppLH = Extra_bddSuppSize( dd, bTemp );
429  bSuppNew = Cudd_bddAnd( dd, bTemp, bVarCur ); Cudd_Ref( bSuppNew );
430  Cudd_RecursiveDeref( dd, bTemp );
431 
432 
433  // several possibilities are possible
434  // (1) support of one component contains another
435  // (2) none of the supports is contained in another
436  fContained = dsdKernelCheckContainment( pDsdMan, pLR, pHR, &pLargeR, &pSmallR );
437 
438  //////////////////////////////////////////////////////////////////////
439  // CASE 3.b One of the cofactors in a constant (OR and EXOR)
440  //////////////////////////////////////////////////////////////////////
441  // the support of the larger component should contain the support of the smaller
442  // it is possible to have PRIME function in this role
443  // for example: F = ITE( a+b, c(+)d, e+f ), F0 = ITE( b, c(+)d, e+f ), F1 = c(+)d
444  if ( fContained )
445  {
446  Dsd_Node_t * pSmall, * pLarge;
447  int c, iCompLarge = -1; // the number of the component is Large is equal to the whole of Small; suppress "might be used uninitialized"
448  int fLowIsLarge;
449 
450  DdNode * bFTemp; // the changed input function
451  Dsd_Node_t * pDETemp, * pDENew;
452 
453  Dsd_Node_t * pComp = NULL;
454  int nComp = -1; // Suppress "might be used uninitialized"
455 
456  if ( pSmallR == pLR )
457  { // Low is Small => High is Large
458  pSmall = pL;
459  pLarge = pH;
460  fLowIsLarge = 0;
461  }
462  else
463  { // vice versa
464  pSmall = pH;
465  pLarge = pL;
466  fLowIsLarge = 1;
467  }
468 
469  // treat the situation when the larger is PRIME
470  if ( pLargeR->Type == DSD_NODE_PRIME ) //&& pLargeR->nDecs != pSmallR->nDecs )
471  {
472  // QUESTION: Is it possible for pLargeR->nDecs > 3
473  // and pSmall contained as one of input in pLarge?
474  // Yes, for example F = a'c + a & MUX(b,c',d) = a'c + abc' + ab'd is non-decomposable
475  // Consider the function H(a->xy) = F( xy, b, c, d )
476  // H0 = H(x=0) = F(0,b,c,d) = c
477  // H1 = F(x=1) = F(y,b,c,d) - non-decomposable
478  //
479  // QUESTION: Is it possible that pLarge is PRIME(3) and pSmall is OR(2),
480  // which is not contained in PRIME as one input?
481  // Yes, for example F = abcd + b'c'd' + a'c'd' = PRIME(ab, c, d)
482  // F(a=0) = c'd' = NOT(OR(a,d)) F(a=1) = bcd + b'c'd' = PRIME(b,c,d)
483  // To find decomposition, we have to prove that F(a=1)|b=0 = F(a=0)
484 
485  // Is it possible that (pLargeR->nDecs == pSmallR->nDecs) and yet this case holds?
486  // Yes, consider the function such that F(a=0) = PRIME(a,b+c,d,e) and F(a=1) = OR(b,c,d,e)
487  // They have the same number of inputs and it is possible that they will be the cofactors
488  // as discribed in the previous example.
489 
490  // find the component, which when substituted for 0 or 1, produces the desired result
491  int g, fFoundComp = -1; // {0,1} depending on whether setting cofactor to 0 or 1 worked out; suppress "might be used uninitialized"
492 
493  DdNode * bLarge, * bSmall;
494  if ( fLowIsLarge )
495  {
496  bLarge = bLow;
497  bSmall = bHigh;
498  }
499  else
500  {
501  bLarge = bHigh;
502  bSmall = bLow;
503  }
504 
505  for ( g = 0; g < pLargeR->nDecs; g++ )
506 // if ( g != c )
507  {
508  pDETemp = pLargeR->pDecs[g]; // cannot be complemented
509  if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, pDETemp->G, b1 ) )
510  {
511  fFoundComp = 1;
512  break;
513  }
514 
515  s_Loops1++;
516 
517  if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, Cudd_Not(pDETemp->G), b1 ) )
518  {
519  fFoundComp = 0;
520  break;
521  }
522 
523  s_Loops1++;
524  }
525 
526  if ( g != pLargeR->nDecs )
527  { // decomposition is found
528  if ( fFoundComp )
529  if ( fLowIsLarge )
530  bFTemp = Cudd_bddOr( dd, bVarCur, pLargeR->pDecs[g]->G );
531  else
532  bFTemp = Cudd_bddOr( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G );
533  else
534  if ( fLowIsLarge )
535  bFTemp = Cudd_bddAnd( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G );
536  else
537  bFTemp = Cudd_bddAnd( dd, bVarCur, pLargeR->pDecs[g]->G );
538  Cudd_Ref( bFTemp );
539 
540  pDENew = dsdKernelDecompose_rec( pDsdMan, bFTemp );
541  pDENew = Dsd_Regular( pDENew );
542  Cudd_RecursiveDeref( dd, bFTemp );
543 
544  // get the new gate
545  pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLargeR->nDecs, s_nDecBlocks++ );
546  dsdKernelCopyListPlusOneMinusOne( pThis, pDENew, pLargeR->pDecs, pLargeR->nDecs, g );
547  goto EXIT;
548  }
549  }
550 
551  // try to find one component in the pLarger that is equal to the whole of pSmaller
552  for ( c = 0; c < pLargeR->nDecs; c++ )
553  if ( pLargeR->pDecs[c] == pSmall || pLargeR->pDecs[c] == Dsd_Not(pSmall) )
554  {
555  iCompLarge = c;
556  break;
557  }
558 
559  // assign the equal component
560  if ( c != pLargeR->nDecs ) // the decomposition is possible!
561  {
562  pComp = pLargeR->pDecs[iCompLarge];
563  nComp = 1;
564  }
565  else // the decomposition is still possible
566  { // for example F = OR(ab,c,d), F(a=0) = OR(c,d), F(a=1) = OR(b,c,d)
567  // supp(F0) is contained in supp(F1), Polarity(F(a=0)) == Polarity(F(a=1))
568 
569  // try to find a group of common components
570  if ( pLargeR->Type == pSmallR->Type &&
571  (pLargeR->Type == DSD_NODE_EXOR || (pSmallR->Type == DSD_NODE_OR && ((pLarge==pLargeR) == (pSmall==pSmallR)))) )
572  {
573  Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL;
574  int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLargeR, pSmallR, &pCommon, &pLastDiffL, &pLastDiffH );
575  // if all the components of pSmall are contained in pLarge,
576  // then the decomposition exists
577  if ( nCommon == pSmallR->nDecs )
578  {
579  pComp = pSmallR;
580  nComp = pSmallR->nDecs;
581  }
582  }
583  }
584 
585  if ( pComp ) // the decomposition is possible!
586  {
587 // Dsd_Node_t * pComp = pLargeR->pDecs[iCompLarge];
588  Dsd_Node_t * pCompR = Dsd_Regular( pComp );
589  int fComp1 = (int)( pLarge != pLargeR );
590  int fComp2 = (int)( pComp != pCompR );
591  int fComp3 = (int)( pSmall != pSmallR );
592 
593  DdNode * bFuncComp; // the function of the given component
594  DdNode * bFuncNew; // the function of the input component
595 
596  if ( pLargeR->Type == DSD_NODE_OR ) // Figure 4 of Matsunaga's paper
597  {
598  // the decomposition exists only if the polarity assignment
599  // along the paths is the same
600  if ( (fComp1 ^ fComp2) == fComp3 )
601  { // decomposition exists = consider 4 cases
602  // consideration of cases leads to the following conclusion
603  // fComp1 gives the polarity of the resulting DSD_NODE_OR gate
604  // fComp2 gives the polarity of the common component feeding into the DSD_NODE_OR gate
605  //
606  // | fComp1 pL/ |pS
607  // <> .........<=>....... <> |
608  // | / |
609  // [OR] [OR] | fComp3
610  // / \ fComp2 / | \ |
611  // <> <> .......<=>... /..|..<> |
612  // / \ / | \|
613  // [OR] [C] S1 S2 C
614  // / \ .
615  // <> \ .
616  // / \ .
617  // [OR] [x] .
618  // / \ .
619  // S1 S2 .
620  //
621 
622 
623  // at this point we have the function F (bFTemp) and the common component C (bFuncComp)
624  // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0
625  // we compute the following R = Exist( F - C, supp(C) )
626  bFTemp = (fComp1)? Cudd_Not( bF ): bF;
627  bFuncComp = (fComp2)? Cudd_Not( pCompR->G ): pCompR->G;
628  bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bFuncComp), pCompR->S ); Cudd_Ref( bFuncNew );
629 
630  // there is no need to copy the dec entry list first, because pComp is a component
631  // which will not be destroyed by the recursive call to decomposition
632  pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
633  assert( Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
634  Cudd_RecursiveDeref( dd, bFuncNew );
635 
636  // get the new gate
637  if ( nComp == 1 )
638  {
640  pThis->pDecs[0] = pDENew;
641  pThis->pDecs[1] = pComp; // takes the complement
642  }
643  else
644  { // pComp is not complemented
645  pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nComp+1, s_nDecBlocks++ );
646  dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp );
647  }
648 
649  if ( fComp1 )
650  pThis = Dsd_Not( pThis );
651  goto EXIT;
652  }
653  }
654  else if ( pLargeR->Type == DSD_NODE_EXOR ) // Figure 5 of Matsunaga's paper (with correction)
655  { // decomposition always exists = consider 4 cases
656 
657  // consideration of cases leads to the following conclusion
658  // fComp3 gives the COMPLEMENT of the polarity of the resulting EXOR gate
659  // (if fComp3 is 0, the EXOR gate is complemented, and vice versa)
660  //
661  // | fComp1 pL/ |pS
662  // <> .........<=>....... /....| fComp3
663  // | / |
664  // [XOR] [XOR] |
665  // / \ fComp2==0 / | \ |
666  // / \ / | \ |
667  // / \ / | \|
668  // [OR] [C] S1 S2 C
669  // / \ .
670  // <> \ .
671  // / \ .
672  // [XOR] [x] .
673  // / \ .
674  // S1 S2 .
675  //
676 
677  assert( fComp2 == 0 );
678  // find the functionality of the lower gates
679  bFTemp = (fComp3)? bF: Cudd_Not( bF );
680  bFuncNew = Cudd_bddXor( dd, bFTemp, pComp->G ); Cudd_Ref( bFuncNew );
681 
682  pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
683  assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
684  Cudd_RecursiveDeref( dd, bFuncNew );
685 
686  // get the new gate
687  if ( nComp == 1 )
688  {
690  pThis->pDecs[0] = pDENew;
691  pThis->pDecs[1] = pComp;
692  }
693  else
694  { // pComp is not complemented
695  pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nComp+1, s_nDecBlocks++ );
696  dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp );
697  }
698 
699  if ( !fComp3 )
700  pThis = Dsd_Not( pThis );
701  goto EXIT;
702  }
703  }
704  }
705 
706  // this case was added to fix the trivial bug found November 4, 2002 in Japan
707  // by running the example provided by T. Sasao
708  if ( nSuppLH == nSuppL + nSuppH ) // the supports of the components are disjoint
709  {
710  // create a new component of the type ITE( a, pH, pL )
712  if ( dd->perm[pLR->S->index] < dd->perm[pHR->S->index] ) // pLR is higher in the varible order
713  {
714  pThis->pDecs[1] = pLR;
715  pThis->pDecs[2] = pHR;
716  }
717  else // pHR is higher in the varible order
718  {
719  pThis->pDecs[1] = pHR;
720  pThis->pDecs[2] = pLR;
721  }
722  // add the first component
723  pThis->pDecs[0] = pVarCurDE;
724  goto EXIT;
725  }
726 
727 
728  //////////////////////////////////////////////////////////////////////
729  // CASE 3.a Neither of the cofactors is a constant (OR, EXOR, PRIME)
730  //////////////////////////////////////////////////////////////////////
731  // the component types are identical
732  // and if they are OR, they are either both complemented or both not complemented
733  // and if they are PRIME, their dec numbers should be the same
734  if ( pLR->Type == pHR->Type &&
735  pLR->Type != DSD_NODE_BUF &&
736  (pLR->Type != DSD_NODE_OR || ( (pL == pLR && pH == pHR) || (pL != pLR && pH != pHR) ) ) &&
737  (pLR->Type != DSD_NODE_PRIME || pLR->nDecs == pHR->nDecs) )
738  {
739  // array to store common comps in pL and pH
740  Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL;
741  int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLR, pHR, &pCommon, &pLastDiffL, &pLastDiffH );
742  if ( nCommon )
743  {
744  if ( pLR->Type == DSD_NODE_OR ) // Figure 2 of Matsunaga's paper
745  { // at this point we have the function F and the group of common components C
746  // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0
747  // we compute the following R = Exist( F - C, supp(C) )
748 
749  // compute the sum total of the common components and the union of their supports
750  DdNode * bCommF, * bCommS, * bFTemp, * bFuncNew;
751  Dsd_Node_t * pDENew;
752 
753  dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, &bCommS, 0 );
754  Cudd_Ref( bCommF );
755  Cudd_Ref( bCommS );
756  bFTemp = ( pL != pLR )? Cudd_Not(bF): bF;
757 
758  bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bCommF), bCommS ); Cudd_Ref( bFuncNew );
759  Cudd_RecursiveDeref( dd, bCommF );
760  Cudd_RecursiveDeref( dd, bCommS );
761 
762  // get the new gate
763 
764  // copy the components first, then call the decomposition
765  // because decomposition will distroy the list used for copying
766  pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nCommon + 1, s_nDecBlocks++ );
767  dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
768 
769  // call the decomposition recursively
770  pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
771 // assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
772  Cudd_RecursiveDeref( dd, bFuncNew );
773 
774  // add the first component
775  pThis->pDecs[0] = pDENew;
776 
777  if ( pL != pLR )
778  pThis = Dsd_Not( pThis );
779  goto EXIT;
780  }
781  else
782  if ( pLR->Type == DSD_NODE_EXOR ) // Figure 3 of Matsunaga's paper
783  {
784  // compute the sum total of the common components and the union of their supports
785  DdNode * bCommF, * bFuncNew;
786  Dsd_Node_t * pDENew;
787  int fCompExor;
788 
789  dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, 1 );
790  Cudd_Ref( bCommF );
791 
792  bFuncNew = Cudd_bddXor( dd, bF, bCommF ); Cudd_Ref( bFuncNew );
793  Cudd_RecursiveDeref( dd, bCommF );
794 
795  // get the new gate
796 
797  // copy the components first, then call the decomposition
798  // because decomposition will distroy the list used for copying
799  pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nCommon + 1, s_nDecBlocks++ );
800  dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
801 
802  // call the decomposition recursively
803  pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
804  Cudd_RecursiveDeref( dd, bFuncNew );
805 
806  // remember the fact that it was complemented
807  fCompExor = Dsd_IsComplement(pDENew);
808  pDENew = Dsd_Regular(pDENew);
809 
810  // add the first component
811  pThis->pDecs[0] = pDENew;
812 
813 
814  if ( fCompExor )
815  pThis = Dsd_Not( pThis );
816  goto EXIT;
817  }
818  else
819  if ( pLR->Type == DSD_NODE_PRIME && (nCommon == pLR->nDecs-1 || nCommon == pLR->nDecs) )
820  {
821  // for example the function F(a,b,c,d) = ITE(b,c,a(+)d) produces
822  // two cofactors F(a=0) = PRIME(b,c,d) and F(a=1) = PRIME(b,c,d)
823  // with exactly the same list of common components
824 
825  Dsd_Node_t * pDENew;
826  DdNode * bFuncNew;
827  int fCompComp = 0; // this flag can be {0,1,2}
828  // if it is 0 there is no identity
829  // if it is 1/2, the cofactored functions are equal in the direct/complemented polarity
830 
831  if ( nCommon == pLR->nDecs )
832  { // all the components are the same
833  // find the formal input, in which pLow and pHigh differ (if such input exists)
834  int m;
835  Dsd_Node_t * pTempL, * pTempH;
836 
837  s_Common++;
838  for ( m = 0; m < pLR->nDecs; m++ )
839  {
840  pTempL = pLR->pDecs[m]; // cannot be complemented
841  pTempH = pHR->pDecs[m]; // cannot be complemented
842 
843  if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pTempL->G, Cudd_Not(pTempH->G) ) &&
844  Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pTempL->G), pTempH->G ) )
845  {
846  pLastDiffL = pTempL;
847  pLastDiffH = pTempH;
848  assert( pLastDiffL == pLastDiffH );
849  fCompComp = 2;
850  break;
851  }
852 
853  s_Loops2++;
854  s_Loops2++;
855 /*
856  if ( s_Loops2 % 10000 == 0 )
857  {
858  int i;
859  for ( i = 0; i < pLR->nDecs; i++ )
860  printf( " %d(s=%d)", pLR->pDecs[i]->Type,
861  Extra_bddSuppSize(dd, pLR->pDecs[i]->S) );
862  printf( "\n" );
863  }
864 */
865 
866  }
867 // if ( pLR->nDecs == Extra_bddSuppSize(dd, pLR->S) )
868 // s_Loops2Useless += pLR->nDecs * 2;
869 
870  if ( fCompComp )
871  { // put the equal components into pCommon, so that they could be copied into the new dec entry
872  nCommon = 0;
873  for ( m = 0; m < pLR->nDecs; m++ )
874  if ( pLR->pDecs[m] != pLastDiffL )
875  pCommon[nCommon++] = pLR->pDecs[m];
876  assert( nCommon = pLR->nDecs-1 );
877  }
878  }
879  else
880  { // the differing components are known - check that they have compatible PRIME function
881 
882  s_CommonNo++;
883 
884  // find the numbers of different components
885  assert( pLastDiffL );
886  assert( pLastDiffH );
887  // also, they cannot be complemented, because the decomposition type is PRIME
888 
889  if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), Cudd_Not(pLastDiffH->G) ) &&
890  Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pLastDiffL->G, pLastDiffH->G ) )
891  fCompComp = 1;
892  else if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pLastDiffL->G, Cudd_Not(pLastDiffH->G) ) &&
893  Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), pLastDiffH->G ) )
894  fCompComp = 2;
895 
896  s_Loops3 += 4;
897  }
898 
899  if ( fCompComp )
900  {
901  if ( fCompComp == 1 ) // it is true that bLow(G=0) == bHigh(H=0) && bLow(G=1) == bHigh(H=1)
902  bFuncNew = Cudd_bddIte( dd, bVarCur, pLastDiffH->G, pLastDiffL->G );
903  else // it is true that bLow(G=0) == bHigh(H=1) && bLow(G=1) == bHigh(H=0)
904  bFuncNew = Cudd_bddIte( dd, bVarCur, Cudd_Not(pLastDiffH->G), pLastDiffL->G );
905  Cudd_Ref( bFuncNew );
906 
907  // get the new gate
908 
909  // copy the components first, then call the decomposition
910  // because decomposition will distroy the list used for copying
912  dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
913 
914  // create a new component
915  pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
916  Cudd_RecursiveDeref( dd, bFuncNew );
917  // the BDD of the argument function in PRIME decomposition, should be regular
918  pDENew = Dsd_Regular(pDENew);
919 
920  // add the first component
921  pThis->pDecs[0] = pDENew;
922  goto EXIT;
923  }
924  } // end of PRIME type
925  } // end of existing common components
926  } // end of CASE 3.a
927 
928 // if ( Depth != 1)
929 // {
930 
931 //CASE4:
932  //////////////////////////////////////////////////////////////////////
933  // CASE 4
934  //////////////////////////////////////////////////////////////////////
935  {
936  // estimate the number of entries in the list
937  int nEntriesMax = pDsdMan->nInputs - dd->perm[VarInt];
938 
939  // create the new decomposition entry
940  int nEntries = 0;
941 
942  DdNode * SuppL, * SuppH, * SuppL_init, * SuppH_init;
943  Dsd_Node_t *pHigher = NULL; // Suppress "might be used uninitialized"
944  Dsd_Node_t *pLower, * pTemp, * pDENew;
945 
946 
947  int levTopSuppL;
948  int levTopSuppH;
949  int levTop;
950 
951  pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, nEntriesMax, s_nDecBlocks++ );
952  pThis->pDecs[ nEntries++ ] = pVarCurDE;
953  // other entries will be added to this list one-by-one during analysis
954 
955  // count how many times does it happen that the decomposition entries are
956  s_Case4Calls++;
957 
958  // consider the simplest case: when the supports are equal
959  // and at least one of the components
960  // is the PRIME without decompositions, or
961  // when both of them are without decomposition
962  if ( (((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) || (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) && pLR->S == pHR->S) ||
963  ((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) && (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) )
964  {
965 
967  // walk through both supports and create the decomposition list composed of simple entries
968  SuppL = pLR->S;
969  SuppH = pHR->S;
970  do
971  {
972  // determine levels
973  levTopSuppL = cuddI(dd,SuppL->index);
974  levTopSuppH = cuddI(dd,SuppH->index);
975 
976  // skip the topmost variable in both supports
977  if ( levTopSuppL <= levTopSuppH )
978  {
979  levTop = levTopSuppL;
980  SuppL = cuddT(SuppL);
981  }
982  else
983  levTop = levTopSuppH;
984 
985  if ( levTopSuppH <= levTopSuppL )
986  SuppH = cuddT(SuppH);
987 
988  // set the new decomposition entry
989  pThis->pDecs[ nEntries++ ] = pDsdMan->pInputs[ dd->invperm[levTop] ];
990  }
991  while ( SuppL != b1 || SuppH != b1 );
992  }
993  else
994  {
995 
996  // compare two different decomposition lists
997  SuppL_init = pLR->S;
998  SuppH_init = pHR->S;
999  // start references (because these supports will change)
1000  SuppL = pLR->S; Cudd_Ref( SuppL );
1001  SuppH = pHR->S; Cudd_Ref( SuppH );
1002  while ( SuppL != b1 || SuppH != b1 )
1003  {
1004  // determine the top level in cofactors and
1005  // whether they have the same top level
1006  int TopLevL = cuddI(dd,SuppL->index);
1007  int TopLevH = cuddI(dd,SuppH->index);
1008  int TopLevel = TopLevH;
1009  int fEqualLevel = 0;
1010 
1011  DdNode * bVarTop;
1012  DdNode * bSuppSubract;
1013 
1014 
1015  if ( TopLevL < TopLevH )
1016  {
1017  pHigher = pLR;
1018  pLower = pHR;
1019  TopLevel = TopLevL;
1020  }
1021  else if ( TopLevL > TopLevH )
1022  {
1023  pHigher = pHR;
1024  pLower = pLR;
1025  }
1026  else
1027  fEqualLevel = 1;
1028  assert( TopLevel != CUDD_CONST_INDEX );
1029 
1030 
1031  // find the currently top variable in the decomposition lists
1032  bVarTop = dd->vars[dd->invperm[TopLevel]];
1033 
1034  if ( !fEqualLevel )
1035  {
1036  // find the lower support
1037  DdNode * bSuppLower = (TopLevL < TopLevH)? SuppH_init: SuppL_init;
1038 
1039  // find the first component in pHigher
1040  // whose support does not overlap with supp(Lower)
1041  // and remember the previous component
1042  int fPolarity;
1043  Dsd_Node_t * pPrev = NULL; // the pointer to the component proceeding pCur
1044  Dsd_Node_t * pCur = pHigher; // the first component not contained in supp(Lower)
1045  while ( Extra_bddSuppOverlapping( dd, pCur->S, bSuppLower ) )
1046  { // get the next component
1047  pPrev = pCur;
1048  pCur = dsdKernelFindContainingComponent( pDsdMan, pCur, bVarTop, &fPolarity );
1049  };
1050 
1051  // look for the possibility to subtract more than one component
1052  if ( pPrev == NULL || pPrev->Type == DSD_NODE_PRIME )
1053  { // if there is no previous component, or if the previous component is PRIME
1054  // there is no way to subtract more than one component
1055 
1056  // add the new decomposition entry (it is already regular)
1057  pThis->pDecs[ nEntries++ ] = pCur;
1058  // assign the support to be subtracted from both components
1059  bSuppSubract = pCur->S;
1060  }
1061  else // all other types
1062  {
1063  // go through the decomposition list of pPrev and find components
1064  // whose support does not overlap with supp(Lower)
1065 
1066  static Dsd_Node_t * pNonOverlap[MAXINPUTS];
1067  int i, nNonOverlap = 0;
1068  for ( i = 0; i < pPrev->nDecs; i++ )
1069  {
1070  pTemp = Dsd_Regular( pPrev->pDecs[i] );
1071  if ( !Extra_bddSuppOverlapping( dd, pTemp->S, bSuppLower ) )
1072  pNonOverlap[ nNonOverlap++ ] = pPrev->pDecs[i];
1073  }
1074  assert( nNonOverlap > 0 );
1075 
1076  if ( nNonOverlap == 1 )
1077  { // one one component was found, which is the original one
1078  assert( Dsd_Regular(pNonOverlap[0]) == pCur);
1079  // add the new decomposition entry
1080  pThis->pDecs[ nEntries++ ] = pCur;
1081  // assign the support to be subtracted from both components
1082  bSuppSubract = pCur->S;
1083  }
1084  else // more than one components was found
1085  {
1086  // find the OR (EXOR) of the non-overlapping components
1087  DdNode * bCommF;
1088  dsdKernelComputeSumOfComponents( pDsdMan, pNonOverlap, nNonOverlap, &bCommF, NULL, (int)(pPrev->Type==DSD_NODE_EXOR) );
1089  Cudd_Ref( bCommF );
1090 
1091  // create a new gated
1092  pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF );
1093  Cudd_RecursiveDeref(dd, bCommF);
1094  // make it regular... it must be regular already
1095  assert( !Dsd_IsComplement(pDENew) );
1096 
1097  // add the new decomposition entry
1098  pThis->pDecs[ nEntries++ ] = pDENew;
1099  // assign the support to be subtracted from both components
1100  bSuppSubract = pDENew->S;
1101  }
1102  }
1103 
1104  // subtract its support from the support of upper component
1105  if ( TopLevL < TopLevH )
1106  {
1107  SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ); Cudd_Ref( SuppL );
1108  Cudd_RecursiveDeref(dd, bTemp);
1109  }
1110  else
1111  {
1112  SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ); Cudd_Ref( SuppH );
1113  Cudd_RecursiveDeref(dd, bTemp);
1114  }
1115  } // end of if ( !fEqualLevel )
1116  else // if ( fEqualLevel ) -- they have the same top level var
1117  {
1118  static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks
1119  static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks
1120  int nMarkedLeft = 0;
1121 
1122  int fPolarity = 0;
1123  Dsd_Node_t * pTempL = pLR;
1124 
1125  int fPolarityCurH = 0;
1126  Dsd_Node_t * pPrevH = NULL, * pCurH = pHR;
1127 
1128  int fPolarityCurL = 0;
1129  Dsd_Node_t * pPrevL = NULL, * pCurL = pLR; // = pMarkedLeft[0];
1130  int index = 1;
1131 
1132  // set the new mark
1133  s_Mark++;
1134 
1135  // go over the dec list of pL, mark all components that contain the given variable
1136  assert( Extra_bddSuppContainVar( dd, pLR->S, bVarTop ) );
1137  assert( Extra_bddSuppContainVar( dd, pHR->S, bVarTop ) );
1138  do {
1139  pTempL->Mark = s_Mark;
1140  pMarkedLeft[ nMarkedLeft ] = pTempL;
1141  pMarkedPols[ nMarkedLeft ] = fPolarity;
1142  nMarkedLeft++;
1143  } while ( (pTempL = dsdKernelFindContainingComponent( pDsdMan, pTempL, bVarTop, &fPolarity )) );
1144 
1145  // go over the dec list of pH, and find the component that is marked and the previos one
1146  // (such component always exists, because they have common variables)
1147  while ( pCurH->Mark != s_Mark )
1148  {
1149  pPrevH = pCurH;
1150  pCurH = dsdKernelFindContainingComponent( pDsdMan, pCurH, bVarTop, &fPolarityCurH );
1151  assert( pCurH );
1152  }
1153 
1154  // go through the first list once again and find
1155  // the component proceeding the one marked found in the second list
1156  while ( pCurL != pCurH )
1157  {
1158  pPrevL = pCurL;
1159  pCurL = pMarkedLeft[index];
1160  fPolarityCurL = pMarkedPols[index];
1161  index++;
1162  }
1163 
1164  // look for the possibility to subtract more than one component
1165  if ( !pPrevL || !pPrevH || pPrevL->Type != pPrevH->Type || pPrevL->Type == DSD_NODE_PRIME || fPolarityCurL != fPolarityCurH )
1166  { // there is no way to extract more than one
1167  pThis->pDecs[ nEntries++ ] = pCurH;
1168  // assign the support to be subtracted from both components
1169  bSuppSubract = pCurH->S;
1170  }
1171  else
1172  {
1173  // find the equal components in two decomposition lists
1174  Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL;
1175  int nCommon = dsdKernelFindCommonComponents( pDsdMan, pPrevL, pPrevH, &pCommon, &pLastDiffL, &pLastDiffH );
1176 
1177  if ( nCommon == 0 || nCommon == 1 )
1178  { // one one component was found, which is the original one
1179  // assert( Dsd_Regular(pCommon[0]) == pCurL);
1180  // add the new decomposition entry
1181  pThis->pDecs[ nEntries++ ] = pCurL;
1182  // assign the support to be subtracted from both components
1183  bSuppSubract = pCurL->S;
1184  }
1185  else // more than one components was found
1186  {
1187  // find the OR (EXOR) of the non-overlapping components
1188  DdNode * bCommF;
1189  dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, (int)(pPrevL->Type==DSD_NODE_EXOR) );
1190  Cudd_Ref( bCommF );
1191 
1192  pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF );
1193  assert( !Dsd_IsComplement(pDENew) ); // cannot be complemented because of construction
1194  Cudd_RecursiveDeref( dd, bCommF );
1195 
1196  // add the new decomposition entry
1197  pThis->pDecs[ nEntries++ ] = pDENew;
1198 
1199  // assign the support to be subtracted from both components
1200  bSuppSubract = pDENew->S;
1201  }
1202  }
1203 
1204  SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ), Cudd_Ref( SuppL );
1205  Cudd_RecursiveDeref(dd, bTemp);
1206 
1207  SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH );
1208  Cudd_RecursiveDeref(dd, bTemp);
1209 
1210  } // end of if ( fEqualLevel )
1211 
1212  } // end of decomposition list comparison
1213  Cudd_RecursiveDeref( dd, SuppL );
1214  Cudd_RecursiveDeref( dd, SuppH );
1215 
1216  }
1217 
1218  // check that the estimation of the number of entries was okay
1219  assert( nEntries <= nEntriesMax );
1220 
1221 // if ( nEntries != Extra_bddSuppSize(dd, bSuppNew) )
1222 // s_Case5++;
1223 
1224  // update the number of entries in the new decomposition list
1225  pThis->nDecs = nEntries;
1226  }
1227 //}
1228 EXIT:
1229 
1230  {
1231  // if the component created is complemented, it represents a function without complement
1232  // therefore, as it is, without complement, it should recieve the complemented function
1233  Dsd_Node_t * pThisR = Dsd_Regular( pThis );
1234  assert( pThisR->G == NULL );
1235  assert( pThisR->S == NULL );
1236 
1237  if ( pThisR == pThis ) // set regular function
1238  pThisR->G = bF;
1239  else // set complemented function
1240  pThisR->G = Cudd_Not(bF);
1241  Cudd_Ref(bF); // reference the function in the component
1242 
1243  assert( bSuppNew );
1244  pThisR->S = bSuppNew; // takes the reference from the new support
1245  if ( st__insert( pDsdMan->Table, (char*)bF, (char*)pThis ) )
1246  {
1247  assert( 0 );
1248  }
1249  s_CacheEntries++;
1250 
1251 
1252 /*
1253  if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 )
1254  {
1255  // write the function, for which verification does not work
1256  cout << endl << "Internal verification failed!"" );
1257 
1258  // create the variable mask
1259  static int s_pVarMask[MAXINPUTS];
1260  int nInputCounter = 0;
1261 
1262  Cudd_SupportArray( dd, bF, s_pVarMask );
1263  int k;
1264  for ( k = 0; k < dd->size; k++ )
1265  if ( s_pVarMask[k] )
1266  nInputCounter++;
1267 
1268  cout << endl << "The problem function is "" );
1269 
1270  DdNode * zNewFunc = Cudd_zddIsopCover( dd, bF, bF ); Cudd_Ref( zNewFunc );
1271  cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask );
1272  Cudd_RecursiveDerefZdd( dd, zNewFunc );
1273  }
1274 */
1275 
1276  }
1277 
1278  Depth--;
1279  return Dsd_NotCond( pThis, fCompF );
1280 }
1281 
1282 
1283 ////////////////////////////////////////////////////////////////////////
1284 /// OTHER FUNCTIONS ///
1285 ////////////////////////////////////////////////////////////////////////
1286 
1287 /**Function*************************************************************
1288 
1289  Synopsis [Finds the corresponding decomposition entry.]
1290 
1291  Description [This function returns the non-complemented pointer to the
1292  DecEntry of that component which contains the given variable in its
1293  support, or NULL if no such component exists]
1294 
1295  SideEffects []
1296 
1297  SeeAlso []
1298 
1299 ***********************************************************************/
1301 
1302 {
1303  Dsd_Node_t * pTemp;
1304  int i;
1305 
1306 // assert( !Dsd_IsComplement( pWhere ) );
1307 // assert( Extra_bddSuppContainVar( pDsdMan->dd, pWhere->S, Var ) );
1308 
1309  if ( pWhere->nDecs == 1 )
1310  return NULL;
1311 
1312  for( i = 0; i < pWhere->nDecs; i++ )
1313  {
1314  pTemp = Dsd_Regular( pWhere->pDecs[i] );
1315  if ( Extra_bddSuppContainVar( pDsdMan->dd, pTemp->S, Var ) )
1316  {
1317  *fPolarity = (int)( pTemp != pWhere->pDecs[i] );
1318  return pTemp;
1319  }
1320  }
1321  assert( 0 );
1322  return NULL;
1323 }
1324 
1325 /**Function*************************************************************
1326 
1327  Synopsis [Find the common decomposition components.]
1328 
1329  Description [This function determines the common components. It counts
1330  the number of common components in the decomposition lists of pL and pH
1331  and returns their number and the lists of common components. It assumes
1332  that pL and pH are regular pointers. It retuns also the pointers to the
1333  last different components encountered in pL and pH.]
1334 
1335  SideEffects []
1336 
1337  SeeAlso []
1338 
1339 ***********************************************************************/
1340 int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH )
1341 {
1342  static Dsd_Node_t * Common[MAXINPUTS];
1343  int nCommon = 0;
1344 
1345  // pointers to the current decomposition entries
1346  Dsd_Node_t * pLcur;
1347  Dsd_Node_t * pHcur;
1348 
1349  // the pointers to their supports
1350  DdNode * bSLcur;
1351  DdNode * bSHcur;
1352 
1353  // the top variable in the supports
1354  int TopVar;
1355 
1356  // the indices running through the components
1357  int iCurL = 0;
1358  int iCurH = 0;
1359  while ( iCurL < pL->nDecs && iCurH < pH->nDecs )
1360  { // both did not run out
1361 
1362  pLcur = Dsd_Regular(pL->pDecs[iCurL]);
1363  pHcur = Dsd_Regular(pH->pDecs[iCurH]);
1364 
1365  bSLcur = pLcur->S;
1366  bSHcur = pHcur->S;
1367 
1368  // find out what component is higher in the BDD
1369  if ( pDsdMan->dd->perm[bSLcur->index] < pDsdMan->dd->perm[bSHcur->index] )
1370  TopVar = bSLcur->index;
1371  else
1372  TopVar = bSHcur->index;
1373 
1374  if ( TopVar == bSLcur->index && TopVar == bSHcur->index )
1375  {
1376  // the components may be equal - should match exactly!
1377  if ( pL->pDecs[iCurL] == pH->pDecs[iCurH] )
1378  Common[nCommon++] = pL->pDecs[iCurL];
1379  else
1380  {
1381  *pLastDiffL = pL->pDecs[iCurL];
1382  *pLastDiffH = pH->pDecs[iCurH];
1383  }
1384 
1385  // skip both
1386  iCurL++;
1387  iCurH++;
1388  }
1389  else if ( TopVar == bSLcur->index )
1390  { // the components cannot be equal
1391  // skip the top-most one
1392  *pLastDiffL = pL->pDecs[iCurL++];
1393  }
1394  else // if ( TopVar == bSHcur->index )
1395  { // the components cannot be equal
1396  // skip the top-most one
1397  *pLastDiffH = pH->pDecs[iCurH++];
1398  }
1399  }
1400 
1401  // if one of the lists still has components, write the first one down
1402  if ( iCurL < pL->nDecs )
1403  *pLastDiffL = pL->pDecs[iCurL];
1404 
1405  if ( iCurH < pH->nDecs )
1406  *pLastDiffH = pH->pDecs[iCurH];
1407 
1408  // return the pointer to the array
1409  *pCommon = Common;
1410  // return the number of common components
1411  return nCommon;
1412 }
1413 
1414 /**Function*************************************************************
1415 
1416  Synopsis [Computes the sum (OR or EXOR) of the functions of the components.]
1417 
1418  Description []
1419 
1420  SideEffects []
1421 
1422  SeeAlso []
1423 
1424 ***********************************************************************/
1425 void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor )
1426 {
1427  DdManager * dd = pDsdMan->dd;
1428  DdNode * bF, * bFadd, * bTemp;
1429  DdNode * bS = NULL; // Suppress "might be used uninitialized"
1430  Dsd_Node_t * pDE, * pDER;
1431  int i;
1432 
1433  // start the function
1434  bF = b0; Cudd_Ref( bF );
1435  // start the support
1436  if ( pCompS )
1437  bS = b1, Cudd_Ref( bS );
1438 
1439  assert( nCommon > 0 );
1440  for ( i = 0; i < nCommon; i++ )
1441  {
1442  pDE = pCommon[i];
1443  pDER = Dsd_Regular( pDE );
1444  bFadd = (pDE != pDER)? Cudd_Not(pDER->G): pDER->G;
1445  // add to the function
1446  if ( fExor )
1447  bF = Cudd_bddXor( dd, bTemp = bF, bFadd );
1448  else
1449  bF = Cudd_bddOr( dd, bTemp = bF, bFadd );
1450  Cudd_Ref( bF );
1451  Cudd_RecursiveDeref( dd, bTemp );
1452  if ( pCompS )
1453  {
1454  // add to the support
1455  bS = Cudd_bddAnd( dd, bTemp = bS, pDER->S ); Cudd_Ref( bS );
1456  Cudd_RecursiveDeref( dd, bTemp );
1457  }
1458  }
1459  // return the function
1460  Cudd_Deref( bF );
1461  *pCompF = bF;
1462 
1463  // return the support
1464  if ( pCompS )
1465  Cudd_Deref( bS ), *pCompS = bS;
1466 }
1467 
1468 /**Function*************************************************************
1469 
1470  Synopsis [Checks support containment of the decomposition components.]
1471 
1472  Description [This function returns 1 if support of one component is contained
1473  in that of another. In this case, pLarge (pSmall) is assigned to point to the
1474  larger (smaller) support. If the supports are identical return 0, and does not
1475  assign the components.]
1476 ]
1477 
1478  SideEffects []
1479 
1480  SeeAlso []
1481 
1482 ***********************************************************************/
1483 int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall )
1484 {
1485  DdManager * dd = pDsdMan->dd;
1486  DdNode * bSuppLarge, * bSuppSmall;
1487  int RetValue;
1488 
1489  RetValue = Extra_bddSuppCheckContainment( dd, pL->S, pH->S, &bSuppLarge, &bSuppSmall );
1490 
1491  if ( RetValue == 0 )
1492  return 0;
1493 
1494  if ( pH->S == bSuppLarge )
1495  {
1496  *pLarge = pH;
1497  *pSmall = pL;
1498  }
1499  else // if ( pL->S == bSuppLarge )
1500  {
1501  *pLarge = pL;
1502  *pSmall = pH;
1503  }
1504  return 1;
1505 }
1506 
1507 /**Function*************************************************************
1508 
1509  Synopsis [Copies the list of components plus one.]
1510 
1511  Description []
1512 
1513  SideEffects []
1514 
1515  SeeAlso []
1516 
1517 ***********************************************************************/
1518 void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize )
1519 {
1520  int i;
1521  assert( nListSize+1 == p->nDecs );
1522  p->pDecs[0] = First;
1523  for( i = 0; i < nListSize; i++ )
1524  p->pDecs[i+1] = ppList[i];
1525 }
1526 
1527 /**Function*************************************************************
1528 
1529  Synopsis [Copies the list of components plus one, and skips one.]
1530 
1531  Description []
1532 
1533  SideEffects []
1534 
1535  SeeAlso []
1536 
1537 ***********************************************************************/
1538 void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int iSkipped )
1539 {
1540  int i, Counter;
1541  assert( nListSize == p->nDecs );
1542  p->pDecs[0] = First;
1543  for( i = 0, Counter = 1; i < nListSize; i++ )
1544  if ( i != iSkipped )
1545  p->pDecs[Counter++] = ppList[i];
1546 }
1547 
1548 /**Function*************************************************************
1549 
1550  Synopsis [Debugging procedure to compute the functionality of the decomposed structure.]
1551 
1552  Description []
1553 
1554  SideEffects []
1555 
1556  SeeAlso []
1557 
1558 ***********************************************************************/
1560 {
1561  DdManager * dd = pDsdMan->dd;
1562  Dsd_Node_t * pR = Dsd_Regular(pDE);
1563  int RetValue;
1564 
1565  DdNode * bRes;
1566  if ( pR->Type == DSD_NODE_CONST1 )
1567  bRes = b1;
1568  else if ( pR->Type == DSD_NODE_BUF )
1569  bRes = pR->G;
1570  else if ( pR->Type == DSD_NODE_OR || pR->Type == DSD_NODE_EXOR )
1571  dsdKernelComputeSumOfComponents( pDsdMan, pR->pDecs, pR->nDecs, &bRes, NULL, (int)(pR->Type == DSD_NODE_EXOR) );
1572  else if ( pR->Type == DSD_NODE_PRIME )
1573  {
1574  int i;
1575  static DdNode * bGVars[MAXINPUTS];
1576  // transform the function of this block, so that it depended on inputs
1577  // corresponding to the formal inputs
1578  DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 ); Cudd_Ref( bNewFunc );
1579 
1580  // compose this function with the inputs
1581  // create the elementary permutation
1582  for ( i = 0; i < dd->size; i++ )
1583  bGVars[i] = dd->vars[i];
1584 
1585  // assign functions to be composed
1586  for ( i = 0; i < pR->nDecs; i++ )
1587  bGVars[dd->invperm[i]] = pR->pDecs[i]->G;
1588 
1589  // perform the composition
1590  bRes = Cudd_bddVectorCompose( dd, bNewFunc, bGVars ); Cudd_Ref( bRes );
1591  Cudd_RecursiveDeref( dd, bNewFunc );
1592 
1593  /////////////////////////////////////////////////////////
1594  RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
1595  /////////////////////////////////////////////////////////
1596  Cudd_Deref( bRes );
1597  }
1598  else
1599  {
1600  assert(0);
1601  }
1602 
1603  Cudd_Ref( bRes );
1604  RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
1605  Cudd_RecursiveDeref( dd, bRes );
1606  return RetValue;
1607 }
1608 
1609 ////////////////////////////////////////////////////////////////////////
1610 /// END OF FILE ///
1611 ////////////////////////////////////////////////////////////////////////
1613 
static int s_nReusedBlocks
Definition: dsdProc.c:74
static int s_nCascades
Definition: dsdProc.c:75
DdNode * S
Definition: dsdInt.h:58
static void dsdKernelCopyListPlusOne(Dsd_Node_t *p, Dsd_Node_t *First, Dsd_Node_t **ppList, int nListSize)
Definition: dsdProc.c:1518
int Extra_bddSuppContainVar(DdManager *dd, DdNode *bS, DdNode *bVar)
Definition: extraBddMisc.c:346
DdManager * dd
Definition: dsdInt.h:42
int Extra_bddSuppSize(DdManager *dd, DdNode *bSupp)
Definition: extraBddMisc.c:321
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
static int HashSuccess
Definition: dsdProc.c:78
static Llb_Mgr_t * p
Definition: llb3Image.c:950
DdNode * G
Definition: dsdInt.h:57
int fVerbose
Definition: dsdInt.h:50
st__table * Table
Definition: dsdInt.h:43
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
int size
Definition: cuddInt.h:361
#define MAXINPUTS
INCLUDES ///.
Definition: cas.h:38
#define b1
Definition: extraBdd.h:76
static int s_Loops3
Definition: dsdProc.c:60
#define Cudd_Regular(node)
Definition: cudd.h:397
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:130
static int dsdKernelFindCommonComponents(Dsd_Manager_t *pDsdMan, Dsd_Node_t *pL, Dsd_Node_t *pH, Dsd_Node_t ***pCommon, Dsd_Node_t **pLastDiffL, Dsd_Node_t **pLastDiffH)
Definition: dsdProc.c:1340
static Dsd_Node_t * dsdKernelDecompose_rec(Dsd_Manager_t *pDsdMan, DdNode *F)
Definition: dsdProc.c:246
static int s_Loops2
Definition: dsdProc.c:59
static int s_Loops1
Definition: dsdProc.c:58
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
static abctime Abc_Clock()
Definition: abc_global.h:279
static int dsdKernelCheckContainment(Dsd_Manager_t *pDsdMan, Dsd_Node_t *pL, Dsd_Node_t *pH, Dsd_Node_t **pLarge, Dsd_Node_t **pSmall)
Definition: dsdProc.c:1483
int Dsd_CheckRootFunctionIdentity(DdManager *dd, DdNode *bF1, DdNode *bF2, DdNode *bC1, DdNode *bC2)
Definition: dsdCheck.c:133
Dsd_Node_t ** pDecs
Definition: dsdInt.h:59
for(p=first;p->value< newval;p=p->next)
static int s_nLiterals
Definition: dsdProc.c:72
int Dsd_TreeCountPrimeNodesOne(Dsd_Node_t *pRoot)
Definition: dsdTree.c:410
static Dsd_Node_t * dsdKernelFindContainingComponent(Dsd_Manager_t *pDsdMan, Dsd_Node_t *pWhere, DdNode *Var, int *fPolarity)
OTHER FUNCTIONS ///.
Definition: dsdProc.c:1300
DdNode * Cudd_bddVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:791
#define st__count(table)
Definition: st.h:71
static int s_nPrimeBlocks
Definition: dsdProc.c:76
static int s_CacheEntries
Definition: dsdProc.c:81
static int s_nExorGates
Definition: dsdProc.c:73
static int s_Case4CallsSpecial
Definition: dsdProc.c:65
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define ddMax(x, y)
Definition: cuddInt.h:832
int Extra_bddSuppCheckContainment(DdManager *dd, DdNode *bL, DdNode *bH, DdNode **bLarge, DdNode **bSmall)
Definition: extraBddMisc.c:443
#define CUDD_CONST_INDEX
Definition: cudd.h:117
int Extra_bddSuppOverlapping(DdManager *dd, DdNode *S1, DdNode *S2)
Definition: extraBddMisc.c:365
static int s_Mark
STATIC VARIABLES ///.
Definition: dsdProc.c:51
static int s_Case4Calls
Definition: dsdProc.c:64
ABC_NAMESPACE_IMPL_START void dsdKernelDecompose(Dsd_Manager_t *pDsdMan, DdNode **pbFuncs, int nFuncs)
FUNCTION DECLARATIONS ///.
void Dsd_Decompose(Dsd_Manager_t *pDsdMan, DdNode **pbFuncs, int nFuncs)
DECOMPOSITION FUNCTIONS ///.
Definition: dsdProc.c:113
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddAndAbs.c:124
STRUCTURE DEFINITIONS ///.
Definition: dsdInt.h:40
static int Counter
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
static int s_CommonNo
Definition: dsdProc.c:62
#define cuddT(node)
Definition: cuddInt.h:636
#define Dsd_Regular(p)
Definition: dsd.h:69
int nRootsAlloc
Definition: dsdInt.h:46
DdNode * Dsd_TreeGetPrimeFunctionOld(DdManager *dd, Dsd_Node_t *pNode, int fRemap)
Definition: dsdTree.c:1120
Dsd_Type_t Type
Definition: dsdInt.h:56
static int HashFailure
Definition: dsdProc.c:79
int Mark
Definition: dsdInt.h:60
#define Dsd_IsComplement(p)
MACRO DEFINITIONS ///.
Definition: dsd.h:68
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static void dsdKernelCopyListPlusOneMinusOne(Dsd_Node_t *p, Dsd_Node_t *First, Dsd_Node_t **ppList, int nListSize, int Skipped)
Definition: dsdProc.c:1538
int nInputs
Definition: dsdInt.h:44
#define cuddI(dd, index)
Definition: cuddInt.h:686
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
Dsd_Node_t * Dsd_TreeNodeCreate(int Type, int nDecs, int BlockNum)
FUNCTION DEFINITIONS ///.
Definition: dsdTree.c:61
#define b0
Definition: extraBdd.h:75
Dsd_Node_t ** pInputs
Definition: dsdInt.h:47
DdHalfWord index
Definition: cudd.h:279
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdNode ** vars
Definition: cuddInt.h:390
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:476
int Var
Definition: SolverTypes.h:42
#define cuddE(node)
Definition: cuddInt.h:652
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
static int dsdKernelVerifyDecomposition(Dsd_Manager_t *pDsdMan, Dsd_Node_t *pDE)
Definition: dsdProc.c:1559
#define assert(ex)
Definition: util_old.h:213
int * invperm
Definition: cuddInt.h:388
static int s_Common
Definition: dsdProc.c:61
#define Dsd_Not(p)
Definition: dsd.h:70
int Dsd_TreeCountNonTerminalNodesOne(Dsd_Node_t *pRoot)
Definition: dsdTree.c:331
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
static void dsdKernelComputeSumOfComponents(Dsd_Manager_t *pDsdMan, Dsd_Node_t **pCommon, int nCommon, DdNode **pCompF, DdNode **pCompS, int fExor)
Definition: dsdProc.c:1425
ABC_INT64_T abctime
Definition: abc_global.h:278
Dsd_Node_t * Dsd_DecomposeOne(Dsd_Manager_t *pDsdMan, DdNode *bFunc)
Definition: dsdProc.c:230
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
int nRoots
Definition: dsdInt.h:45
int Cudd_SharingSize(DdNode **nodeArray, int n)
Definition: cuddUtil.c:544
#define Dsd_NotCond(p, c)
Definition: dsd.h:71
int * perm
Definition: cuddInt.h:386
void Dsd_TreeNodeGetInfoOne(Dsd_Node_t *pNode, int *DepthMax, int *GateSizeMax)
Definition: dsdTree.c:183
Dsd_Node_t ** pRoots
Definition: dsdInt.h:48
static int s_nDecBlocks
Definition: dsdProc.c:71
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
static int Depth
Definition: dsdProc.c:56
short nDecs
Definition: dsdInt.h:61