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