abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraBddImage.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [extraBddImage.c]
4 
5  PackageName [extra]
6 
7  Synopsis [Various reusable software utilities.]
8 
9  Author [Alan Mishchenko]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 1.0. Started - September 1, 2003.]
14 
15  Revision [$Id: extraBddImage.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "extraBdd.h"
20 
21 ABC_NAMESPACE_IMPL_START
22 
23 
24 /*
25  The ideas implemented in this file are inspired by the paper:
26  Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple,
27  Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in
28  Image Computation. ICCAD, 2001.
29 */
30 
31 /*---------------------------------------------------------------------------*/
32 /* Constant declarations */
33 /*---------------------------------------------------------------------------*/
34 
35 /*---------------------------------------------------------------------------*/
36 /* Stucture declarations */
37 /*---------------------------------------------------------------------------*/
38 
39 typedef struct Extra_ImageNode_t_ Extra_ImageNode_t;
40 typedef struct Extra_ImagePart_t_ Extra_ImagePart_t;
41 typedef struct Extra_ImageVar_t_ Extra_ImageVar_t;
42 
43 struct Extra_ImageTree_t_
44 {
45  Extra_ImageNode_t * pRoot; // the root of quantification tree
46  Extra_ImageNode_t * pCare; // the leaf node with the care set
47  DdNode * bCareSupp; // the cube to quantify from the care
48  int fVerbose; // the verbosity flag
49  int nNodesMax; // the max number of nodes in one iter
50  int nNodesMaxT; // the overall max number of nodes
51  int nIter; // the number of iterations with this tree
52 };
53 
54 struct Extra_ImageNode_t_
55 {
56  DdManager * dd; // the manager
57  DdNode * bCube; // the cube to quantify
58  DdNode * bImage; // the partial image
59  Extra_ImageNode_t * pNode1; // the first branch
60  Extra_ImageNode_t * pNode2; // the second branch
61  Extra_ImagePart_t * pPart; // the partition (temporary)
62 };
63 
64 struct Extra_ImagePart_t_
65 {
66  DdNode * bFunc; // the partition
67  DdNode * bSupp; // the support of this partition
68  int nNodes; // the number of BDD nodes
69  short nSupp; // the number of support variables
70  short iPart; // the number of this partition
71 };
72 
73 struct Extra_ImageVar_t_
74 {
75  int iNum; // the BDD index of this variable
76  DdNode * bParts; // the partition numbers
77  int nParts; // the number of partitions
78 };
79 
80 /*---------------------------------------------------------------------------*/
81 /* Type declarations */
82 /*---------------------------------------------------------------------------*/
83 
84 /*---------------------------------------------------------------------------*/
85 /* Variable declarations */
86 /*---------------------------------------------------------------------------*/
87 
88 /*---------------------------------------------------------------------------*/
89 /* Macro declarations */
90 /*---------------------------------------------------------------------------*/
91 
92 /**AutomaticStart*************************************************************/
93 
94 
95 /*---------------------------------------------------------------------------*/
96 /* Static function prototypes */
97 /*---------------------------------------------------------------------------*/
98 
99 static Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
100  int nParts, DdNode ** pbParts, DdNode * bCare );
101 static Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
102  int nParts, Extra_ImagePart_t ** pParts,
103  int nVars, DdNode ** pbVarsNs );
104 static Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
105  int nParts, Extra_ImagePart_t ** pParts,
106  int nVars, Extra_ImageVar_t ** pVars );
107 static void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode );
108 static int Extra_BuildTreeNode( DdManager * dd,
109  int nNodes, Extra_ImageNode_t ** pNodes,
110  int nVars, Extra_ImageVar_t ** pVars );
111 static Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd,
112  int nNodes, Extra_ImageNode_t ** pNodes );
113 static void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode );
114 static void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode );
115 static int Extra_FindBestVariable( DdManager * dd,
116  int nNodes, Extra_ImageNode_t ** pNodes,
117  int nVars, Extra_ImageVar_t ** pVars );
118 static void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts,
119  int nNodes, Extra_ImageNode_t ** pNodes,
120  int * piNode1, int * piNode2 );
121 static Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
122  Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 );
123 
124 static void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
125  int nParts, DdNode ** pbParts,
126  int nVars, DdNode ** pbVars );
127 static void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc,
128  DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
129 
130 static void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree );
131 static void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int nOffset );
132 
133 
134 /**AutomaticEnd***************************************************************/
135 
136 
137 /*---------------------------------------------------------------------------*/
138 /* Definition of exported functions */
139 /*---------------------------------------------------------------------------*/
140 
141 /**Function*************************************************************
142 
143  Synopsis [Starts the image computation using tree-based scheduling.]
144 
145  Description [This procedure starts the image computation. It uses
146  the given care set to test-run the image computation and creates the
147  quantification tree by scheduling variable quantifications. The tree can
148  be used to compute images for other care sets without rescheduling.
149  In this case, Extra_bddImageCompute() should be called.]
150 
151  SideEffects []
152 
153  SeeAlso []
154 
155 ***********************************************************************/
156 Extra_ImageTree_t * Extra_bddImageStart(
157  DdManager * dd, DdNode * bCare, // the care set
158  int nParts, DdNode ** pbParts, // the partitions for image computation
159  int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!)
160 {
161  Extra_ImageTree_t * pTree;
162  Extra_ImagePart_t ** pParts;
163  Extra_ImageVar_t ** pVars;
164  Extra_ImageNode_t ** pNodes;
165  int v;
166 
167  if ( fVerbose && dd->size <= 80 )
168  Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
169 
170  // create variables, partitions and leaf nodes
171  pParts = Extra_CreateParts( dd, nParts, pbParts, bCare );
172  pVars = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
173  pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
174 
175  // create the tree
176  pTree = ABC_ALLOC( Extra_ImageTree_t, 1 );
177  memset( pTree, 0, sizeof(Extra_ImageTree_t) );
178  pTree->pCare = pNodes[nParts];
179  pTree->fVerbose = fVerbose;
180 
181  // process the nodes
182  while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) );
183 
184  // make sure the variables are gone
185  for ( v = 0; v < dd->size; v++ )
186  assert( pVars[v] == NULL );
187  ABC_FREE( pVars );
188 
189  // merge the topmost nodes
190  while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
191 
192  // make sure the nodes are gone
193  for ( v = 0; v < nParts + 1; v++ )
194  assert( pNodes[v] == NULL );
195  ABC_FREE( pNodes );
196 
197 // if ( fVerbose )
198 // Extra_bddImagePrintTree( pTree );
199 
200  // set the support of the care set
201  pTree->bCareSupp = Cudd_Support( dd, bCare ); Cudd_Ref( pTree->bCareSupp );
202 
203  // clean the partitions
204  Extra_DeleteParts_rec( pTree->pRoot );
205  ABC_FREE( pParts );
206  return pTree;
207 }
208 
209 /**Function*************************************************************
210 
211  Synopsis [Compute the image.]
212 
213  Description []
214 
215  SideEffects []
216 
217  SeeAlso []
218 
219 ***********************************************************************/
220 DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare )
221 {
222  DdManager * dd = pTree->pCare->dd;
223  DdNode * bSupp, * bRem;
224 
225  pTree->nIter++;
226 
227  // make sure the supports are okay
228  bSupp = Cudd_Support( dd, bCare ); Cudd_Ref( bSupp );
229  if ( bSupp != pTree->bCareSupp )
230  {
231  bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp ); Cudd_Ref( bRem );
232  if ( bRem != b1 )
233  {
234 printf( "Original care set support: " );
235 ABC_PRB( dd, pTree->bCareSupp );
236 printf( "Current care set support: " );
237 ABC_PRB( dd, bSupp );
238  Cudd_RecursiveDeref( dd, bSupp );
239  Cudd_RecursiveDeref( dd, bRem );
240  printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
241  return NULL;
242  }
243  Cudd_RecursiveDeref( dd, bRem );
244  }
245  Cudd_RecursiveDeref( dd, bSupp );
246 
247  // remove the previous image
248  Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
249  pTree->pCare->bImage = bCare; Cudd_Ref( bCare );
250 
251  // compute the image
252  pTree->nNodesMax = 0;
253  Extra_bddImageCompute_rec( pTree, pTree->pRoot );
254  if ( pTree->nNodesMaxT < pTree->nNodesMax )
255  pTree->nNodesMaxT = pTree->nNodesMax;
256 
257 // if ( pTree->fVerbose )
258 // printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
259  return pTree->pRoot->bImage;
260 }
261 
262 /**Function*************************************************************
263 
264  Synopsis [Delete the tree.]
265 
266  Description []
267 
268  SideEffects []
269 
270  SeeAlso []
271 
272 ***********************************************************************/
273 void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree )
274 {
275  if ( pTree->bCareSupp )
276  Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
277  Extra_bddImageTreeDelete_rec( pTree->pRoot );
278  ABC_FREE( pTree );
279 }
280 
281 /**Function*************************************************************
282 
283  Synopsis [Reads the image from the tree.]
284 
285  Description []
286 
287  SideEffects []
288 
289  SeeAlso []
290 
291 ***********************************************************************/
292 DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree )
293 {
294  return pTree->pRoot->bImage;
295 }
296 
297 /*---------------------------------------------------------------------------*/
298 /* Definition of internal functions */
299 /*---------------------------------------------------------------------------*/
300 
301 /*---------------------------------------------------------------------------*/
302 /* Definition of static Functions */
303 /*---------------------------------------------------------------------------*/
304 
305 /**Function*************************************************************
306 
307  Synopsis [Creates partitions.]
308 
309  Description []
310 
311  SideEffects []
312 
313  SeeAlso []
314 
315 ***********************************************************************/
316 Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
317  int nParts, DdNode ** pbParts, DdNode * bCare )
318 {
319  Extra_ImagePart_t ** pParts;
320  int i;
321 
322  // start the partitions
323  pParts = ABC_ALLOC( Extra_ImagePart_t *, nParts + 1 );
324  // create structures for each variable
325  for ( i = 0; i < nParts; i++ )
326  {
327  pParts[i] = ABC_ALLOC( Extra_ImagePart_t, 1 );
328  pParts[i]->bFunc = pbParts[i]; Cudd_Ref( pParts[i]->bFunc );
329  pParts[i]->bSupp = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
330  pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp );
331  pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
332  pParts[i]->iPart = i;
333  }
334  // add the care set as the last partition
335  pParts[nParts] = ABC_ALLOC( Extra_ImagePart_t, 1 );
336  pParts[nParts]->bFunc = bCare; Cudd_Ref( pParts[nParts]->bFunc );
337  pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
338  pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp );
339  pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
340  pParts[nParts]->iPart = nParts;
341  return pParts;
342 }
343 
344 /**Function*************************************************************
345 
346  Synopsis [Creates variables.]
347 
348  Description []
349 
350  SideEffects []
351 
352  SeeAlso []
353 
354 ***********************************************************************/
355 Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
356  int nParts, Extra_ImagePart_t ** pParts,
357  int nVars, DdNode ** pbVars )
358 {
359  Extra_ImageVar_t ** pVars;
360  DdNode ** pbFuncs;
361  DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
362  int nVarsTotal, iVar, p, Counter;
363 
364  // put all the functions into one array
365  pbFuncs = ABC_ALLOC( DdNode *, nParts );
366  for ( p = 0; p < nParts; p++ )
367  pbFuncs[p] = pParts[p]->bSupp;
368  bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts ); Cudd_Ref( bSupp );
369  ABC_FREE( pbFuncs );
370 
371  // remove the NS vars
372  bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bCubeNs );
373  bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs ); Cudd_Ref( bSupp );
374  Cudd_RecursiveDeref( dd, bTemp );
375  Cudd_RecursiveDeref( dd, bCubeNs );
376 
377  // get the number of I and CS variables to be quantified
378  nVarsTotal = Extra_bddSuppSize( dd, bSupp );
379 
380  // start the variables
381  pVars = ABC_ALLOC( Extra_ImageVar_t *, dd->size );
382  memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size );
383  // create structures for each variable
384  for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
385  {
386  iVar = bSuppTemp->index;
387  pVars[iVar] = ABC_ALLOC( Extra_ImageVar_t, 1 );
388  pVars[iVar]->iNum = iVar;
389  // collect all the parts this var belongs to
390  Counter = 0;
391  bParts = b1; Cudd_Ref( bParts );
392  for ( p = 0; p < nParts; p++ )
393  if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
394  {
395  bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] ); Cudd_Ref( bParts );
396  Cudd_RecursiveDeref( dd, bTemp );
397  Counter++;
398  }
399  pVars[iVar]->bParts = bParts; // takes ref
400  pVars[iVar]->nParts = Counter;
401  }
402  Cudd_RecursiveDeref( dd, bSupp );
403  return pVars;
404 }
405 
406 /**Function*************************************************************
407 
408  Synopsis [Creates variables.]
409 
410  Description []
411 
412  SideEffects []
413 
414  SeeAlso []
415 
416 ***********************************************************************/
417 Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
418  int nParts, Extra_ImagePart_t ** pParts,
419  int nVars, Extra_ImageVar_t ** pVars )
420 {
421  Extra_ImageNode_t ** pNodes;
422  Extra_ImageNode_t * pNode;
423  DdNode * bTemp;
424  int i, v, iPart;
425 /*
426  DdManager * dd; // the manager
427  DdNode * bCube; // the cube to quantify
428  DdNode * bImage; // the partial image
429  Extra_ImageNode_t * pNode1; // the first branch
430  Extra_ImageNode_t * pNode2; // the second branch
431  Extra_ImagePart_t * pPart; // the partition (temporary)
432 */
433  // start the partitions
434  pNodes = ABC_ALLOC( Extra_ImageNode_t *, nParts );
435  // create structures for each leaf nodes
436  for ( i = 0; i < nParts; i++ )
437  {
438  pNodes[i] = ABC_ALLOC( Extra_ImageNode_t, 1 );
439  memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) );
440  pNodes[i]->dd = dd;
441  pNodes[i]->pPart = pParts[i];
442  }
443  // find the quantification cubes for each leaf node
444  for ( v = 0; v < nVars; v++ )
445  {
446  if ( pVars[v] == NULL )
447  continue;
448  assert( pVars[v]->nParts > 0 );
449  if ( pVars[v]->nParts > 1 )
450  continue;
451  iPart = pVars[v]->bParts->index;
452  if ( pNodes[iPart]->bCube == NULL )
453  {
454  pNodes[iPart]->bCube = dd->vars[v];
455  Cudd_Ref( dd->vars[v] );
456  }
457  else
458  {
459  pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );
460  Cudd_Ref( pNodes[iPart]->bCube );
461  Cudd_RecursiveDeref( dd, bTemp );
462  }
463  // remove these variables
464  Cudd_RecursiveDeref( dd, pVars[v]->bParts );
465  ABC_FREE( pVars[v] );
466  }
467 
468  // assign the leaf node images
469  for ( i = 0; i < nParts; i++ )
470  {
471  pNode = pNodes[i];
472  if ( pNode->bCube )
473  {
474  // update the partition
475  pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
476  Cudd_Ref( pParts[i]->bFunc );
477  Cudd_RecursiveDeref( dd, bTemp );
478  // update the support the partition
479  pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube );
480  Cudd_Ref( pParts[i]->bSupp );
481  Cudd_RecursiveDeref( dd, bTemp );
482  // update the numbers
483  pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp );
484  pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
485  // get rid of the cube
486  // save the last (care set) quantification cube
487  if ( i < nParts - 1 )
488  {
489  Cudd_RecursiveDeref( dd, pNode->bCube );
490  pNode->bCube = NULL;
491  }
492  }
493  // copy the function
494  pNode->bImage = pParts[i]->bFunc; Cudd_Ref( pNode->bImage );
495  }
496 /*
497  for ( i = 0; i < nParts; i++ )
498  {
499  pNode = pNodes[i];
500 ABC_PRB( dd, pNode->bCube );
501 ABC_PRB( dd, pNode->pPart->bFunc );
502 ABC_PRB( dd, pNode->pPart->bSupp );
503 printf( "\n" );
504  }
505 */
506  return pNodes;
507 }
508 
509 
510 /**Function*************************************************************
511 
512  Synopsis [Delete the partitions from the nodes.]
513 
514  Description []
515 
516  SideEffects []
517 
518  SeeAlso []
519 
520 ***********************************************************************/
521 void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode )
522 {
523  Extra_ImagePart_t * pPart;
524  if ( pNode->pNode1 )
525  Extra_DeleteParts_rec( pNode->pNode1 );
526  if ( pNode->pNode2 )
527  Extra_DeleteParts_rec( pNode->pNode2 );
528  pPart = pNode->pPart;
529  Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
530  Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
531  ABC_FREE( pNode->pPart );
532 }
533 
534 /**Function*************************************************************
535 
536  Synopsis [Delete the partitions from the nodes.]
537 
538  Description []
539 
540  SideEffects []
541 
542  SeeAlso []
543 
544 ***********************************************************************/
545 void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode )
546 {
547  if ( pNode->pNode1 )
548  Extra_bddImageTreeDelete_rec( pNode->pNode1 );
549  if ( pNode->pNode2 )
550  Extra_bddImageTreeDelete_rec( pNode->pNode2 );
551  if ( pNode->bCube )
552  Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
553  if ( pNode->bImage )
554  Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
555  assert( pNode->pPart == NULL );
556  ABC_FREE( pNode );
557 }
558 
559 /**Function*************************************************************
560 
561  Synopsis [Recompute the image.]
562 
563  Description []
564 
565  SideEffects []
566 
567  SeeAlso []
568 
569 ***********************************************************************/
570 void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode )
571 {
572  DdManager * dd = pNode->dd;
573  DdNode * bTemp;
574  int nNodes;
575 
576  // trivial case
577  if ( pNode->pNode1 == NULL )
578  {
579  if ( pNode->bCube )
580  {
581  pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube );
582  Cudd_Ref( pNode->bImage );
583  Cudd_RecursiveDeref( dd, bTemp );
584  }
585  return;
586  }
587 
588  // compute the children
589  if ( pNode->pNode1 )
590  Extra_bddImageCompute_rec( pTree, pNode->pNode1 );
591  if ( pNode->pNode2 )
592  Extra_bddImageCompute_rec( pTree, pNode->pNode2 );
593 
594  // clean the old image
595  if ( pNode->bImage )
596  Cudd_RecursiveDeref( dd, pNode->bImage );
597  pNode->bImage = NULL;
598 
599  // compute the new image
600  if ( pNode->bCube )
601  pNode->bImage = Cudd_bddAndAbstract( dd,
602  pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
603  else
604  pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
605  Cudd_Ref( pNode->bImage );
606 
607  if ( pTree->fVerbose )
608  {
609  nNodes = Cudd_DagSize( pNode->bImage );
610  if ( pTree->nNodesMax < nNodes )
611  pTree->nNodesMax = nNodes;
612  }
613 }
614 
615 /**Function*************************************************************
616 
617  Synopsis [Builds the tree.]
618 
619  Description []
620 
621  SideEffects []
622 
623  SeeAlso []
624 
625 ***********************************************************************/
626 int Extra_BuildTreeNode( DdManager * dd,
627  int nNodes, Extra_ImageNode_t ** pNodes,
628  int nVars, Extra_ImageVar_t ** pVars )
629 {
630  Extra_ImageNode_t * pNode1, * pNode2;
631  Extra_ImageVar_t * pVar;
632  Extra_ImageNode_t * pNode;
633  DdNode * bCube, * bTemp, * bSuppTemp, * bParts;
634  int iNode1, iNode2;
635  int iVarBest, nSupp, v;
636 
637  // find the best variable
638  iVarBest = Extra_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
639  if ( iVarBest == -1 )
640  return 0;
641 
642  pVar = pVars[iVarBest];
643 
644  // this var cannot appear in one partition only
645  nSupp = Extra_bddSuppSize( dd, pVar->bParts );
646  assert( nSupp == pVar->nParts );
647  assert( nSupp != 1 );
648 
649  // if it appears in only two partitions, quantify it
650  if ( pVar->nParts == 2 )
651  {
652  // get the nodes
653  iNode1 = pVar->bParts->index;
654  iNode2 = cuddT(pVar->bParts)->index;
655  pNode1 = pNodes[iNode1];
656  pNode2 = pNodes[iNode2];
657 
658  // get the quantification cube
659  bCube = dd->vars[pVar->iNum]; Cudd_Ref( bCube );
660  // add the variables that appear only in these partitions
661  for ( v = 0; v < nVars; v++ )
662  if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
663  {
664  // add this var
665  bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] ); Cudd_Ref( bCube );
666  Cudd_RecursiveDeref( dd, bTemp );
667  // clean this var
668  Cudd_RecursiveDeref( dd, pVars[v]->bParts );
669  ABC_FREE( pVars[v] );
670  }
671  // clean the best var
672  Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
673  ABC_FREE( pVars[iVarBest] );
674 
675  // combines two nodes
676  pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
677  Cudd_RecursiveDeref( dd, bCube );
678  }
679  else // if ( pVar->nParts > 2 )
680  {
681  // find two smallest BDDs that have this var
682  Extra_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
683  pNode1 = pNodes[iNode1];
684  pNode2 = pNodes[iNode2];
685 
686  // it is not possible that a var appears only in these two
687  // otherwise, it would have a different cost
688  bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
689  for ( v = 0; v < nVars; v++ )
690  if ( pVars[v] && pVars[v]->bParts == bParts )
691  assert( 0 );
692  Cudd_RecursiveDeref( dd, bParts );
693 
694  // combines two nodes
695  pNode = Extra_CombineTwoNodes( dd, b1, pNode1, pNode2 );
696  }
697 
698  // clean the old nodes
699  pNodes[iNode1] = pNode;
700  pNodes[iNode2] = NULL;
701 
702  // update the variables that appear in pNode[iNode2]
703  for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
704  {
705  pVar = pVars[bSuppTemp->index];
706  if ( pVar == NULL ) // this variable is not be quantified
707  continue;
708  // quantify this var
709  assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
710  pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
711  Cudd_RecursiveDeref( dd, bTemp );
712  // add the new var
713  pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
714  Cudd_RecursiveDeref( dd, bTemp );
715  // update the score
716  pVar->nParts = Extra_bddSuppSize( dd, pVar->bParts );
717  }
718  return 1;
719 }
720 
721 
722 /**Function*************************************************************
723 
724  Synopsis [Merges the nodes.]
725 
726  Description []
727 
728  SideEffects []
729 
730  SeeAlso []
731 
732 ***********************************************************************/
733 Extra_ImageNode_t * Extra_MergeTopNodes(
734  DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes )
735 {
736  Extra_ImageNode_t * pNode;
737  int n1 = -1, n2 = -1, n;
738 
739  // find the first and the second non-empty spots
740  for ( n = 0; n < nNodes; n++ )
741  if ( pNodes[n] )
742  {
743  if ( n1 == -1 )
744  n1 = n;
745  else if ( n2 == -1 )
746  {
747  n2 = n;
748  break;
749  }
750  }
751  assert( n1 != -1 );
752  // check the situation when only one such node is detected
753  if ( n2 == -1 )
754  {
755  // save the node
756  pNode = pNodes[n1];
757  // clean the node
758  pNodes[n1] = NULL;
759  return pNode;
760  }
761 
762  // combines two nodes
763  pNode = Extra_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
764 
765  // clean the old nodes
766  pNodes[n1] = pNode;
767  pNodes[n2] = NULL;
768  return NULL;
769 }
770 
771 /**Function*************************************************************
772 
773  Synopsis [Merges two nodes.]
774 
775  Description []
776 
777  SideEffects []
778 
779  SeeAlso []
780 
781 ***********************************************************************/
782 Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
783  Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 )
784 {
785  Extra_ImageNode_t * pNode;
786  Extra_ImagePart_t * pPart;
787 
788  // create a new partition
789  pPart = ABC_ALLOC( Extra_ImagePart_t, 1 );
790  memset( pPart, 0, sizeof(Extra_ImagePart_t) );
791  // create the function
792  pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
793  Cudd_Ref( pPart->bFunc );
794  // update the support the partition
795  pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
796  Cudd_Ref( pPart->bSupp );
797  // update the numbers
798  pPart->nSupp = Extra_bddSuppSize( dd, pPart->bSupp );
799  pPart->nNodes = Cudd_DagSize( pPart->bFunc );
800  pPart->iPart = -1;
801 /*
802 ABC_PRB( dd, pNode1->pPart->bSupp );
803 ABC_PRB( dd, pNode2->pPart->bSupp );
804 ABC_PRB( dd, pPart->bSupp );
805 */
806  // create a new node
807  pNode = ABC_ALLOC( Extra_ImageNode_t, 1 );
808  memset( pNode, 0, sizeof(Extra_ImageNode_t) );
809  pNode->dd = dd;
810  pNode->pPart = pPart;
811  pNode->pNode1 = pNode1;
812  pNode->pNode2 = pNode2;
813  // compute the image
814  pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube );
815  Cudd_Ref( pNode->bImage );
816  // save the cube
817  if ( bCube != b1 )
818  {
819  pNode->bCube = bCube; Cudd_Ref( bCube );
820  }
821  return pNode;
822 }
823 
824 /**Function*************************************************************
825 
826  Synopsis [Computes the best variable.]
827 
828  Description [The variables is the best if the sum of squares of the
829  BDD sizes of the partitions, in which it participates, is the minimum.]
830 
831  SideEffects []
832 
833  SeeAlso []
834 
835 ***********************************************************************/
836 int Extra_FindBestVariable( DdManager * dd,
837  int nNodes, Extra_ImageNode_t ** pNodes,
838  int nVars, Extra_ImageVar_t ** pVars )
839 {
840  DdNode * bTemp;
841  int iVarBest, v;
842  double CostBest, CostCur;
843 
844  CostBest = 100000000000000.0;
845  iVarBest = -1;
846  for ( v = 0; v < nVars; v++ )
847  if ( pVars[v] )
848  {
849  CostCur = 0;
850  for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
851  CostCur += pNodes[bTemp->index]->pPart->nNodes *
852  pNodes[bTemp->index]->pPart->nNodes;
853  if ( CostBest > CostCur )
854  {
855  CostBest = CostCur;
856  iVarBest = v;
857  }
858  }
859  return iVarBest;
860 }
861 
862 /**Function*************************************************************
863 
864  Synopsis [Computes two smallest partions that have this var.]
865 
866  Description []
867 
868  SideEffects []
869 
870  SeeAlso []
871 
872 ***********************************************************************/
873 void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts,
874  int nNodes, Extra_ImageNode_t ** pNodes,
875  int * piNode1, int * piNode2 )
876 {
877  DdNode * bTemp;
878  int iPart1, iPart2;
879  int CostMin1, CostMin2, Cost;
880 
881  // go through the partitions
882  iPart1 = iPart2 = -1;
883  CostMin1 = CostMin2 = 1000000;
884  for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
885  {
886  Cost = pNodes[bTemp->index]->pPart->nNodes;
887  if ( CostMin1 > Cost )
888  {
889  CostMin2 = CostMin1; iPart2 = iPart1;
890  CostMin1 = Cost; iPart1 = bTemp->index;
891  }
892  else if ( CostMin2 > Cost )
893  {
894  CostMin2 = Cost; iPart2 = bTemp->index;
895  }
896  }
897 
898  *piNode1 = iPart1;
899  *piNode2 = iPart2;
900 }
901 
902 /**Function*************************************************************
903 
904  Synopsis [Prints the latch dependency matrix.]
905 
906  Description []
907 
908  SideEffects []
909 
910  SeeAlso []
911 
912 ***********************************************************************/
913 void Extra_bddImagePrintLatchDependency(
914  DdManager * dd, DdNode * bCare, // the care set
915  int nParts, DdNode ** pbParts, // the partitions for image computation
916  int nVars, DdNode ** pbVars ) // the NS and parameter variables (not quantified!)
917 {
918  int i;
919  DdNode * bVarsCs, * bVarsNs;
920 
921  bVarsCs = Cudd_Support( dd, bCare ); Cudd_Ref( bVarsCs );
922  bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bVarsNs );
923 
924  printf( "The latch dependency matrix:\n" );
925  printf( "Partitions = %d Variables: total = %d non-quantifiable = %d\n",
926  nParts, dd->size, nVars );
927  printf( " : " );
928  for ( i = 0; i < dd->size; i++ )
929  printf( "%d", i % 10 );
930  printf( "\n" );
931 
932  for ( i = 0; i < nParts; i++ )
933  Extra_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
934  Extra_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
935 
936  Cudd_RecursiveDeref( dd, bVarsCs );
937  Cudd_RecursiveDeref( dd, bVarsNs );
938 }
939 
940 /**Function*************************************************************
941 
942  Synopsis [Prints one row of the latch dependency matrix.]
943 
944  Description []
945 
946  SideEffects []
947 
948  SeeAlso []
949 
950 ***********************************************************************/
951 void Extra_bddImagePrintLatchDependencyOne(
952  DdManager * dd, DdNode * bFunc, // the function
953  DdNode * bVarsCs, DdNode * bVarsNs, // the current/next state vars
954  int iPart )
955 {
956  DdNode * bSupport;
957  int v;
958  bSupport = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupport );
959  printf( " %3d : ", iPart );
960  for ( v = 0; v < dd->size; v++ )
961  {
962  if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
963  {
964  if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
965  printf( "c" );
966  else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) )
967  printf( "n" );
968  else
969  printf( "i" );
970  }
971  else
972  printf( "." );
973  }
974  printf( "\n" );
975  Cudd_RecursiveDeref( dd, bSupport );
976 }
977 
978 
979 /**Function*************************************************************
980 
981  Synopsis [Prints the tree for quenstification scheduling.]
982 
983  Description []
984 
985  SideEffects []
986 
987  SeeAlso []
988 
989 ***********************************************************************/
990 void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree )
991 {
992  printf( "The quantification scheduling tree:\n" );
993  Extra_bddImagePrintTree_rec( pTree->pRoot, 1 );
994 }
995 
996 /**Function*************************************************************
997 
998  Synopsis [Prints the tree for quenstification scheduling.]
999 
1000  Description []
1001 
1002  SideEffects []
1003 
1004  SeeAlso []
1005 
1006 ***********************************************************************/
1007 void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
1008 {
1009  DdNode * Cube;
1010  int i;
1011 
1012  Cube = pNode->bCube;
1013 
1014  if ( pNode->pNode1 == NULL )
1015  {
1016  printf( "<%d> ", pNode->pPart->iPart );
1017  if ( Cube != NULL )
1018  {
1019  ABC_PRB( pNode->dd, Cube );
1020  }
1021  else
1022  printf( "\n" );
1023  return;
1024  }
1025 
1026  printf( "<*> " );
1027  if ( Cube != NULL )
1028  {
1029  ABC_PRB( pNode->dd, Cube );
1030  }
1031  else
1032  printf( "\n" );
1033 
1034  for ( i = 0; i < Offset; i++ )
1035  printf( " " );
1036  Extra_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
1037 
1038  for ( i = 0; i < Offset; i++ )
1039  printf( " " );
1040  Extra_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
1041 }
1042 
1043 
1044 
1045 
1046 
1047 struct Extra_ImageTree2_t_
1048 {
1049  DdManager * dd;
1050  DdNode * bRel;
1051  DdNode * bCube;
1052  DdNode * bImage;
1053 };
1054 
1055 /**Function*************************************************************
1056 
1057  Synopsis [Starts the monolithic image computation.]
1058 
1059  Description []
1060 
1061  SideEffects []
1062 
1063  SeeAlso []
1064 
1065 ***********************************************************************/
1066 Extra_ImageTree2_t * Extra_bddImageStart2(
1067  DdManager * dd, DdNode * bCare,
1068  int nParts, DdNode ** pbParts,
1069  int nVars, DdNode ** pbVars, int fVerbose )
1070 {
1071  Extra_ImageTree2_t * pTree;
1072  DdNode * bCubeAll, * bCubeNot, * bTemp;
1073  int i;
1074 
1075  pTree = ABC_ALLOC( Extra_ImageTree2_t, 1 );
1076  pTree->dd = dd;
1077  pTree->bImage = NULL;
1078 
1079  bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size ); Cudd_Ref( bCubeAll );
1080  bCubeNot = Extra_bddComputeCube( dd, pbVars, nVars ); Cudd_Ref( bCubeNot );
1081  pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
1082  Cudd_RecursiveDeref( dd, bCubeAll );
1083  Cudd_RecursiveDeref( dd, bCubeNot );
1084 
1085  // derive the monolithic relation
1086  pTree->bRel = b1; Cudd_Ref( pTree->bRel );
1087  for ( i = 0; i < nParts; i++ )
1088  {
1089  pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
1090  Cudd_RecursiveDeref( dd, bTemp );
1091  }
1092  Extra_bddImageCompute2( pTree, bCare );
1093  return pTree;
1094 }
1095 
1096 
1097 /**Function*************************************************************
1098 
1099  Synopsis []
1100 
1101  Description []
1102 
1103  SideEffects []
1104 
1105  SeeAlso []
1106 
1107 ***********************************************************************/
1108 DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare )
1109 {
1110  if ( pTree->bImage )
1111  Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
1112  pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube );
1113  Cudd_Ref( pTree->bImage );
1114  return pTree->bImage;
1115 }
1116 
1117 /**Function*************************************************************
1118 
1119  Synopsis []
1120 
1121  Description []
1122 
1123  SideEffects []
1124 
1125  SeeAlso []
1126 
1127 ***********************************************************************/
1128 void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree )
1129 {
1130  if ( pTree->bRel )
1131  Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
1132  if ( pTree->bCube )
1133  Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
1134  if ( pTree->bImage )
1135  Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
1136  ABC_FREE( pTree );
1137 }
1138 
1139 /**Function*************************************************************
1140 
1141  Synopsis [Returns the previously computed image.]
1142 
1143  Description []
1144 
1145  SideEffects []
1146 
1147  SeeAlso []
1148 
1149 ***********************************************************************/
1150 DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree )
1151 {
1152  return pTree->bImage;
1153 }
1154 
1155 
1156 ////////////////////////////////////////////////////////////////////////
1157 /// END OF FILE ///
1158 ////////////////////////////////////////////////////////////////////////
1159 
1160 
1161 ABC_NAMESPACE_IMPL_END
1162 
memset
char * memset()
Extra_ImagePart_t_::bSupp
DdNode * bSupp
Definition: extraBddImage.c:67
Extra_FindBestPartitions
static void Extra_FindBestPartitions(DdManager *dd, DdNode *bParts, int nNodes, Extra_ImageNode_t **pNodes, int *piNode1, int *piNode2)
Definition: extraBddImage.c:873
Extra_bddImagePrintLatchDependencyOne
static void Extra_bddImagePrintLatchDependencyOne(DdManager *dd, DdNode *bFunc, DdNode *bVarsCs, DdNode *bVarsNs, int iPart)
Definition: extraBddImage.c:951
Extra_bddSuppSize
int Extra_bddSuppSize(DdManager *dd, DdNode *bSupp)
Definition: extraBddMisc.c:321
Cudd_bddComputeCube
DdNode * Cudd_bddComputeCube(DdManager *dd, DdNode **vars, int *phase, int n)
Definition: cuddUtil.c:2196
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Extra_ImageTree_t_::fVerbose
int fVerbose
Definition: extraBddImage.c:48
Extra_ImageVar_t_::nParts
int nParts
Definition: extraBddImage.c:77
DdNode
Definition: cudd.h:278
Extra_bddImagePrintTree_rec
static void Extra_bddImagePrintTree_rec(Extra_ImageNode_t *pNode, int nOffset)
Definition: extraBddImage.c:1007
Extra_ImageNode_t_
Definition: extraBddImage.c:54
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
Extra_ImageNode_t_::dd
DdManager * dd
Definition: extraBddImage.c:56
DdManager::size
int size
Definition: cuddInt.h:361
Extra_ImagePart_t_
Definition: extraBddImage.c:64
b1
#define b1
Definition: extraBdd.h:76
Extra_ImagePart_t_::bFunc
DdNode * bFunc
Definition: extraBddImage.c:66
Extra_ImageNode_t_::pNode1
Extra_ImageNode_t * pNode1
Definition: extraBddImage.c:59
Extra_ImageTree_t_
Definition: extraBddImage.c:43
Cudd_bddExistAbstract
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:130
Extra_bddImageTreeDelete_rec
static void Extra_bddImageTreeDelete_rec(Extra_ImageNode_t *pNode)
Definition: extraBddImage.c:545
Extra_bddImageCompute
DdNode * Extra_bddImageCompute(Extra_ImageTree_t *pTree, DdNode *bCare)
Definition: extraBddImage.c:220
Extra_bddComputeCube
DdNode * Extra_bddComputeCube(DdManager *dd, DdNode **bXVars, int nVars)
Definition: extraBddMisc.c:1001
Extra_ImageNode_t
typedefABC_NAMESPACE_IMPL_START struct Extra_ImageNode_t_ Extra_ImageNode_t
Definition: extraBddImage.c:39
Extra_ImageTree2_t_::bCube
DdNode * bCube
Definition: extraBddImage.c:1051
DdManager::bFunc
DdNode * bFunc
Definition: cuddInt.h:487
Extra_ImageNode_t_::pPart
Extra_ImagePart_t * pPart
Definition: extraBddImage.c:61
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Extra_ImageNode_t_::bCube
DdNode * bCube
Definition: extraBddImage.c:57
Extra_bddImageRead2
DdNode * Extra_bddImageRead2(Extra_ImageTree2_t *pTree)
Definition: extraBddImage.c:1150
Extra_ImageTree2_t_::bImage
DdNode * bImage
Definition: extraBddImage.c:1052
Extra_bddImageTreeDelete2
void Extra_bddImageTreeDelete2(Extra_ImageTree2_t *pTree)
Definition: extraBddImage.c:1128
Extra_ImageTree2_t_
Definition: extraBddImage.c:1047
Extra_ImageTree_t_::pCare
Extra_ImageNode_t * pCare
Definition: extraBddImage.c:46
Extra_ImageVar_t_::bParts
DdNode * bParts
Definition: extraBddImage.c:76
Extra_bddImageCompute_rec
static void Extra_bddImageCompute_rec(Extra_ImageTree_t *pTree, Extra_ImageNode_t *pNode)
Definition: extraBddImage.c:570
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
if
if(last==0)
Definition: sparse_int.h:34
Extra_ImageTree_t_::nNodesMax
int nNodesMax
Definition: extraBddImage.c:49
Extra_bddImageRead
DdNode * Extra_bddImageRead(Extra_ImageTree_t *pTree)
Definition: extraBddImage.c:292
Extra_bddImageTreeDelete
void Extra_bddImageTreeDelete(Extra_ImageTree_t *pTree)
Definition: extraBddImage.c:273
Extra_ImageNode_t_::pNode2
Extra_ImageNode_t * pNode2
Definition: extraBddImage.c:60
Cudd_bddAndAbstract
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddAndAbs.c:124
Extra_CombineTwoNodes
static Extra_ImageNode_t * Extra_CombineTwoNodes(DdManager *dd, DdNode *bCube, Extra_ImageNode_t *pNode1, Extra_ImageNode_t *pNode2)
Definition: extraBddImage.c:782
Counter
static int Counter
Definition: extraBddMisc.c:1877
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
Extra_CreateNodes
static Extra_ImageNode_t ** Extra_CreateNodes(DdManager *dd, int nParts, Extra_ImagePart_t **pParts, int nVars, Extra_ImageVar_t **pVars)
Definition: extraBddImage.c:417
Extra_ImageVar_t_
Definition: extraBddImage.c:73
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Extra_ImageTree2_t_::dd
DdManager * dd
Definition: extraBddImage.c:1049
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
Extra_MergeTopNodes
static Extra_ImageNode_t * Extra_MergeTopNodes(DdManager *dd, int nNodes, Extra_ImageNode_t **pNodes)
Definition: extraBddImage.c:733
Extra_ImageTree_t_::bCareSupp
DdNode * bCareSupp
Definition: extraBddImage.c:47
Extra_ImageVar_t_::iNum
int iNum
Definition: extraBddImage.c:75
Extra_bddImagePrintLatchDependency
static void Extra_bddImagePrintLatchDependency(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars)
Definition: extraBddImage.c:913
Extra_bddImagePrintTree
static void Extra_bddImagePrintTree(Extra_ImageTree_t *pTree)
Definition: extraBddImage.c:990
Extra_ImageTree_t_::nIter
int nIter
Definition: extraBddImage.c:51
Extra_bddImageCompute2
DdNode * Extra_bddImageCompute2(Extra_ImageTree2_t *pTree, DdNode *bCare)
Definition: extraBddImage.c:1108
Extra_CreateVars
static Extra_ImageVar_t ** Extra_CreateVars(DdManager *dd, int nParts, Extra_ImagePart_t **pParts, int nVars, DdNode **pbVarsNs)
Definition: extraBddImage.c:355
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
Extra_BuildTreeNode
static int Extra_BuildTreeNode(DdManager *dd, int nNodes, Extra_ImageNode_t **pNodes, int nVars, Extra_ImageVar_t **pVars)
Definition: extraBddImage.c:626
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Extra_ImageNode_t_::bImage
DdNode * bImage
Definition: extraBddImage.c:58
Extra_DeleteParts_rec
static void Extra_DeleteParts_rec(Extra_ImageNode_t *pNode)
Definition: extraBddImage.c:521
assert
#define assert(ex)
Definition: util_old.h:213
Extra_FindBestVariable
static int Extra_FindBestVariable(DdManager *dd, int nNodes, Extra_ImageNode_t **pNodes, int nVars, Extra_ImageVar_t **pVars)
Definition: extraBddImage.c:836
Extra_ImageTree_t_::pRoot
Extra_ImageNode_t * pRoot
Definition: extraBddImage.c:45
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Extra_ImagePart_t_::nSupp
short nSupp
Definition: extraBddImage.c:69
Extra_ImageTree_t_::nNodesMaxT
int nNodesMaxT
Definition: extraBddImage.c:50
Extra_bddImageStart
Extra_ImageTree_t * Extra_bddImageStart(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
Definition: extraBddImage.c:156
ABC_PRB
#define ABC_PRB(dd, f)
Definition: extraBdd.h:200
Extra_bddImageStart2
Extra_ImageTree2_t * Extra_bddImageStart2(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
Definition: extraBddImage.c:1066
Extra_ImageTree2_t_::bRel
DdNode * bRel
Definition: extraBddImage.c:1050
Extra_CreateParts
static Extra_ImagePart_t ** Extra_CreateParts(DdManager *dd, int nParts, DdNode **pbParts, DdNode *bCare)
Definition: extraBddImage.c:316
Cudd_VectorSupport
DdNode * Cudd_VectorSupport(DdManager *dd, DdNode **F, int n)
Definition: cuddUtil.c:908
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Extra_ImagePart_t_::nNodes
int nNodes
Definition: extraBddImage.c:68
Extra_ImagePart_t_::iPart
short iPart
Definition: extraBddImage.c:70