1 /**CFile****************************************************************
2
3 FileName [cloudCore.c]
4
5 PackageName [Fast application-specific BDD package.]
6
7 Synopsis [The package core.]
8
9 Author [Alan Mishchenko <alanmi@ece.pdx.edu>]
10
11 Affiliation [ECE Department. Portland State University, Portland, Oregon.]
12
13 Date [Ver. 1.0. Started - June 10, 2002.]
14
15 Revision [$Id: cloudCore.c,v 1.0 2002/06/10 03:00:00 alanmi Exp $]
16
17 ***********************************************************************/
18
19 #include <string.h>
20 #include "cloud.h"
21
22 ABC_NAMESPACE_IMPL_START
23
24
25 // the number of operators using cache
26 static int CacheOperNum = 4;
27
28 // the ratio of cache size to the unique table size for each operator
29 static int CacheLogRatioDefault[4] = {
30 2, // CLOUD_OPER_AND,
31 8, // CLOUD_OPER_XOR,
32 8, // CLOUD_OPER_BDIFF,
33 8 // CLOUD_OPER_LEQ
34 };
35
36 // the ratio of cache size to the unique table size for each operator
37 static int CacheSize[4] = {
38 2, // CLOUD_OPER_AND,
39 2, // CLOUD_OPER_XOR,
40 2, // CLOUD_OPER_BDIFF,
41 2 // CLOUD_OPER_LEQ
42 };
43
44 ////////////////////////////////////////////////////////////////////////
45 /// FUNCTION DECLARATIONS ///
46 ////////////////////////////////////////////////////////////////////////
47
48 // static functions
49 static CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e );
50 static void cloudCacheAllocate( CloudManager * dd, CloudOper oper );
51
52 ////////////////////////////////////////////////////////////////////////
53 /// FUNCTION DEFINITIONS ///
54 ////////////////////////////////////////////////////////////////////////
55
56 /**Function********************************************************************
57
58 Synopsis [Starts the cloud manager.]
59
60 Description [The first arguments is the number of elementary variables used.
61 The second arguments is the number of bits of the unsigned integer used to
62 represent nodes in the unique table. If the second argument is 0, the package
63 assumes 23 to represent nodes, which is equivalent to 2^23 = 8,388,608 nodes.]
64
65 SideEffects []
66
67 SeeAlso []
68
69 ******************************************************************************/
Cloud_Init(int nVars,int nBits)70 CloudManager * Cloud_Init( int nVars, int nBits )
71 {
72 CloudManager * dd;
73 int i;
74 abctime clk1, clk2;
75
76 assert( nVars <= 100000 );
77 assert( nBits < 32 );
78
79 // assign the defaults
80 if ( nBits == 0 )
81 nBits = CLOUD_NODE_BITS;
82
83 // start the manager
84 dd = ABC_CALLOC( CloudManager, 1 );
85 dd->nMemUsed += sizeof(CloudManager);
86
87 // variables
88 dd->nVars = nVars; // the number of variables allocated
89 // bits
90 dd->bitsNode = nBits; // the number of bits used for the node
91 for ( i = 0; i < CacheOperNum; i++ )
92 dd->bitsCache[i] = nBits - CacheLogRatioDefault[i];
93 // shifts
94 dd->shiftUnique = 8*sizeof(unsigned) - (nBits + 1); // gets node index in the hash table
95 for ( i = 0; i < CacheOperNum; i++ )
96 dd->shiftCache[i] = 8*sizeof(unsigned) - dd->bitsCache[i];
97 // nodes
98 dd->nNodesAlloc = (1 << (nBits + 1)); // 2 ^ (nBits + 1)
99 dd->nNodesLimit = (1 << nBits); // 2 ^ nBits
100
101 // unique table
102 clk1 = Abc_Clock();
103 dd->tUnique = ABC_CALLOC( CloudNode, dd->nNodesAlloc );
104 dd->nMemUsed += sizeof(CloudNode) * dd->nNodesAlloc;
105 clk2 = Abc_Clock();
106 //ABC_PRT( "calloc() time", clk2 - clk1 );
107
108 // set up the constant node (the only node that is not in the hash table)
109 dd->nSignCur = 1;
110 dd->tUnique[0].s = dd->nSignCur;
111 dd->tUnique[0].v = CLOUD_CONST_INDEX;
112 dd->tUnique[0].e = NULL;
113 dd->tUnique[0].t = NULL;
114 dd->one = dd->tUnique;
115 dd->zero = Cloud_Not(dd->one);
116 dd->nNodesCur = 1;
117
118 // special nodes
119 dd->pNodeStart = dd->tUnique + 1;
120 dd->pNodeEnd = dd->tUnique + dd->nNodesAlloc;
121
122 // set up the elementary variables
123 dd->vars = ABC_ALLOC( CloudNode *, dd->nVars );
124 dd->nMemUsed += sizeof(CloudNode *) * dd->nVars;
125 for ( i = 0; i < dd->nVars; i++ )
126 dd->vars[i] = cloudMakeNode( dd, i, dd->one, dd->zero );
127
128 return dd;
129 };
130
131 /**Function********************************************************************
132
133 Synopsis [Stops the cloud manager.]
134
135 Description [The first arguments tells show many elementary variables are used.
136 The second arguments tells how many bits of the unsigned integer are used
137 to represent regular nodes in the unique table.]
138
139 SideEffects []
140
141 SeeAlso []
142
143 ******************************************************************************/
Cloud_Quit(CloudManager * dd)144 void Cloud_Quit( CloudManager * dd )
145 {
146 int i;
147 ABC_FREE( dd->ppNodes );
148 ABC_FREE( dd->tUnique );
149 ABC_FREE( dd->vars );
150 for ( i = 0; i < 4; i++ )
151 ABC_FREE( dd->tCaches[i] );
152 ABC_FREE( dd );
153 }
154
155 /**Function********************************************************************
156
157 Synopsis [Prepares the manager for another run.]
158
159 Description []
160
161 SideEffects []
162
163 SeeAlso []
164
165 ******************************************************************************/
Cloud_Restart(CloudManager * dd)166 void Cloud_Restart( CloudManager * dd )
167 {
168 int i;
169 assert( dd->one->s == dd->nSignCur );
170 dd->nSignCur++;
171 dd->one->s++;
172 for ( i = 0; i < dd->nVars; i++ )
173 dd->vars[i]->s++;
174 dd->nNodesCur = 1 + dd->nVars;
175 }
176
177 /**Function********************************************************************
178
179 Synopsis [This optional function allocates operation cache of the given size.]
180
181 Description [Cache for each operation is allocated independently when the first
182 operation of the given type is performed. The user can allocate cache of his/her
183 preferred size by calling Cloud_CacheAllocate before the first operation of the
184 given type is performed, but this call is optional. Argument "logratio" gives
185 the binary logarithm of the ratio of the size of the unique table to that of cache.
186 For example, if "logratio" is equal to 3, and the unique table will be 2^3=8 times
187 larger than cache; so, if unique table is 2^23 = 8,388,608 nodes, the cache size
188 will be 2^3=8 times smaller and equal to 2^20 = 1,048,576 entries.]
189
190 SideEffects []
191
192 SeeAlso []
193
194 ******************************************************************************/
Cloud_CacheAllocate(CloudManager * dd,CloudOper oper,int logratio)195 void Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int logratio )
196 {
197 assert( logratio > 0 ); // cache cannot be larger than the unique table
198 assert( logratio < dd->bitsNode ); // cache cannot be smaller than 2 entries
199
200 if ( logratio )
201 {
202 dd->bitsCache[oper] = dd->bitsNode - logratio;
203 dd->shiftCache[oper] = 8*sizeof(unsigned) - dd->bitsCache[oper];
204 }
205 cloudCacheAllocate( dd, oper );
206 }
207
208 /**Function********************************************************************
209
210 Synopsis [Internal cache allocation.]
211
212 Description []
213
214 SideEffects []
215
216 SeeAlso []
217
218 ******************************************************************************/
cloudCacheAllocate(CloudManager * dd,CloudOper oper)219 void cloudCacheAllocate( CloudManager * dd, CloudOper oper )
220 {
221 int nCacheEntries = (1 << dd->bitsCache[oper]);
222
223 if ( CacheSize[oper] == 1 )
224 {
225 dd->tCaches[oper] = (CloudCacheEntry2 *)ABC_CALLOC( CloudCacheEntry1, nCacheEntries );
226 dd->nMemUsed += sizeof(CloudCacheEntry1) * nCacheEntries;
227 }
228 else if ( CacheSize[oper] == 2 )
229 {
230 dd->tCaches[oper] = (CloudCacheEntry2 *)ABC_CALLOC( CloudCacheEntry2, nCacheEntries );
231 dd->nMemUsed += sizeof(CloudCacheEntry2) * nCacheEntries;
232 }
233 else if ( CacheSize[oper] == 3 )
234 {
235 dd->tCaches[oper] = (CloudCacheEntry2 *)ABC_CALLOC( CloudCacheEntry3, nCacheEntries );
236 dd->nMemUsed += sizeof(CloudCacheEntry3) * nCacheEntries;
237 }
238 }
239
240
241
242 /**Function********************************************************************
243
244 Synopsis [Returns or creates a new node]
245
246 Description [Checks the unique table for the existance of the node. If the node is
247 present, returns the node. If the node is absent, creates a new node.]
248
249 SideEffects []
250
251 SeeAlso []
252
253 ******************************************************************************/
Cloud_MakeNode(CloudManager * dd,CloudVar v,CloudNode * t,CloudNode * e)254 CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e )
255 {
256 CloudNode * pRes;
257 CLOUD_ASSERT(t);
258 CLOUD_ASSERT(e);
259 assert( v < Cloud_V(t) && v < Cloud_V(e) ); // variable should be above in the order
260 if ( Cloud_IsComplement(t) )
261 {
262 pRes = cloudMakeNode( dd, v, Cloud_Not(t), Cloud_Not(e) );
263 if ( pRes != NULL )
264 pRes = Cloud_Not(pRes);
265 }
266 else
267 pRes = cloudMakeNode( dd, v, t, e );
268 return pRes;
269 }
270
271 /**Function********************************************************************
272
273 Synopsis [Returns or creates a new node]
274
275 Description [Checks the unique table for the existance of the node. If the node is
276 present, returns the node. If the node is absent, creates a new node.]
277
278 SideEffects []
279
280 SeeAlso []
281
282 ******************************************************************************/
cloudMakeNode(CloudManager * dd,CloudVar v,CloudNode * t,CloudNode * e)283 CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e )
284 {
285 CloudNode * entryUnique;
286
287 CLOUD_ASSERT(t);
288 CLOUD_ASSERT(e);
289
290 assert( ((int)v) >= 0 && ((int)v) < dd->nVars ); // the variable must be in the range
291 assert( v < Cloud_V(t) && v < Cloud_V(e) ); // variable should be above in the order
292 assert( !Cloud_IsComplement(t) ); // the THEN edge must not be complemented
293
294 // make sure we are not searching for the constant node
295 assert( t && e );
296
297 // get the unique entry
298 entryUnique = dd->tUnique + cloudHashCudd3(v, t, e, dd->shiftUnique);
299 while ( entryUnique->s == dd->nSignCur )
300 {
301 // compare the node
302 if ( entryUnique->v == v && entryUnique->t == t && entryUnique->e == e )
303 { // the node is found
304 dd->nUniqueHits++;
305 return entryUnique; // returns the node
306 }
307 // increment the hash value modulus the hash table size
308 if ( ++entryUnique - dd->tUnique == dd->nNodesAlloc )
309 entryUnique = dd->tUnique + 1;
310 // increment the number of steps through the table
311 dd->nUniqueSteps++;
312 }
313 dd->nUniqueMisses++;
314
315 // check if the new node can be created
316 if ( ++dd->nNodesCur == dd->nNodesLimit )
317 { // initiate the restart
318 printf( "Cloud needs restart!\n" );
319 // fflush( stdout );
320 // exit(1);
321 return NULL;
322 }
323 // create the node
324 entryUnique->s = dd->nSignCur;
325 entryUnique->v = v;
326 entryUnique->t = t;
327 entryUnique->e = e;
328 return entryUnique; // returns the node
329 }
330
331
332 /**Function********************************************************************
333
334 Synopsis [Performs the AND or two BDDs]
335
336 Description []
337
338 SideEffects []
339
340 SeeAlso []
341
342 ******************************************************************************/
cloudBddAnd(CloudManager * dd,CloudNode * f,CloudNode * g)343 CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
344 {
345 CloudNode * F, * G, * r;
346 CloudCacheEntry2 * cacheEntry;
347 CloudNode * fv, * fnv, * gv, * gnv, * t, * e;
348 CloudVar var;
349
350 assert( f <= g );
351
352 // terminal cases
353 F = Cloud_Regular(f);
354 G = Cloud_Regular(g);
355 if ( F == G )
356 {
357 if ( f == g )
358 return f;
359 else
360 return dd->zero;
361 }
362 if ( F == dd->one )
363 {
364 if ( f == dd->one )
365 return g;
366 else
367 return f;
368 }
369
370 // check cache
371 cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashCudd2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
372 // cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashBuddy2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
373 r = cloudCacheLookup2( cacheEntry, dd->nSignCur, f, g );
374 if ( r != NULL )
375 {
376 dd->nCacheHits++;
377 return r;
378 }
379 dd->nCacheMisses++;
380
381
382 // compute cofactors
383 if ( cloudV(F) <= cloudV(G) )
384 {
385 var = cloudV(F);
386 if ( Cloud_IsComplement(f) )
387 {
388 fnv = Cloud_Not(cloudE(F));
389 fv = Cloud_Not(cloudT(F));
390 }
391 else
392 {
393 fnv = cloudE(F);
394 fv = cloudT(F);
395 }
396 }
397 else
398 {
399 var = cloudV(G);
400 fv = fnv = f;
401 }
402
403 if ( cloudV(G) <= cloudV(F) )
404 {
405 if ( Cloud_IsComplement(g) )
406 {
407 gnv = Cloud_Not(cloudE(G));
408 gv = Cloud_Not(cloudT(G));
409 }
410 else
411 {
412 gnv = cloudE(G);
413 gv = cloudT(G);
414 }
415 }
416 else
417 {
418 gv = gnv = g;
419 }
420
421 if ( fv <= gv )
422 t = cloudBddAnd( dd, fv, gv );
423 else
424 t = cloudBddAnd( dd, gv, fv );
425
426 if ( t == NULL )
427 return NULL;
428
429 if ( fnv <= gnv )
430 e = cloudBddAnd( dd, fnv, gnv );
431 else
432 e = cloudBddAnd( dd, gnv, fnv );
433
434 if ( e == NULL )
435 return NULL;
436
437 if ( t == e )
438 r = t;
439 else
440 {
441 if ( Cloud_IsComplement(t) )
442 {
443 r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) );
444 if ( r == NULL )
445 return NULL;
446 r = Cloud_Not(r);
447 }
448 else
449 {
450 r = cloudMakeNode( dd, var, t, e );
451 if ( r == NULL )
452 return NULL;
453 }
454 }
455 cloudCacheInsert2( cacheEntry, dd->nSignCur, f, g, r );
456 return r;
457 }
458
459 /**Function********************************************************************
460
461 Synopsis [Performs the AND or two BDDs]
462
463 Description []
464
465 SideEffects []
466
467 SeeAlso []
468
469 ******************************************************************************/
cloudBddAnd_gate(CloudManager * dd,CloudNode * f,CloudNode * g)470 static inline CloudNode * cloudBddAnd_gate( CloudManager * dd, CloudNode * f, CloudNode * g )
471 {
472 if ( f <= g )
473 return cloudBddAnd(dd,f,g);
474 else
475 return cloudBddAnd(dd,g,f);
476 }
477
478 /**Function********************************************************************
479
480 Synopsis [Performs the AND or two BDDs]
481
482 Description []
483
484 SideEffects []
485
486 SeeAlso []
487
488 ******************************************************************************/
Cloud_bddAnd(CloudManager * dd,CloudNode * f,CloudNode * g)489 CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
490 {
491 if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
492 return NULL;
493 CLOUD_ASSERT(f);
494 CLOUD_ASSERT(g);
495 if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
496 cloudCacheAllocate( dd, CLOUD_OPER_AND );
497 return cloudBddAnd_gate( dd, f, g );
498 }
499
500 /**Function********************************************************************
501
502 Synopsis [Performs the OR or two BDDs]
503
504 Description []
505
506 SideEffects []
507
508 SeeAlso []
509
510 ******************************************************************************/
Cloud_bddOr(CloudManager * dd,CloudNode * f,CloudNode * g)511 CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g )
512 {
513 CloudNode * res;
514 if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
515 return NULL;
516 CLOUD_ASSERT(f);
517 CLOUD_ASSERT(g);
518 if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
519 cloudCacheAllocate( dd, CLOUD_OPER_AND );
520 res = cloudBddAnd_gate( dd, Cloud_Not(f), Cloud_Not(g) );
521 res = Cloud_NotCond( res, res != NULL );
522 return res;
523 }
524
525 /**Function********************************************************************
526
527 Synopsis [Performs the XOR or two BDDs]
528
529 Description []
530
531 SideEffects []
532
533 SeeAlso []
534
535 ******************************************************************************/
Cloud_bddXor(CloudManager * dd,CloudNode * f,CloudNode * g)536 CloudNode * Cloud_bddXor( CloudManager * dd, CloudNode * f, CloudNode * g )
537 {
538 CloudNode * t0, * t1, * r;
539 if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
540 return NULL;
541 CLOUD_ASSERT(f);
542 CLOUD_ASSERT(g);
543 if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
544 cloudCacheAllocate( dd, CLOUD_OPER_AND );
545 t0 = cloudBddAnd_gate( dd, f, Cloud_Not(g) );
546 if ( t0 == NULL )
547 return NULL;
548 t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g );
549 if ( t1 == NULL )
550 return NULL;
551 r = Cloud_bddOr( dd, t0, t1 );
552 return r;
553 }
554
555
556
557 /**Function********************************************************************
558
559 Synopsis [Performs a DFS from f, clearing the LSB of the next
560 pointers.]
561
562 Description []
563
564 SideEffects [None]
565
566 SeeAlso [cloudSupport cloudDagSize]
567
568 ******************************************************************************/
cloudClearMark(CloudManager * dd,CloudNode * n)569 static void cloudClearMark( CloudManager * dd, CloudNode * n )
570 {
571 if ( !cloudNodeIsMarked(n) )
572 return;
573 // clear visited flag
574 cloudNodeUnmark(n);
575 if ( cloudIsConstant(n) )
576 return;
577 cloudClearMark( dd, cloudT(n) );
578 cloudClearMark( dd, Cloud_Regular(cloudE(n)) );
579 }
580
581 /**Function********************************************************************
582
583 Synopsis [Performs the recursive step of Cloud_Support.]
584
585 Description [Performs the recursive step of Cloud_Support. Performs a
586 DFS from f. The support is accumulated in supp as a side effect. Uses
587 the LSB of the then pointer as visited flag.]
588
589 SideEffects [None]
590
591 SeeAlso []
592
593 ******************************************************************************/
cloudSupport(CloudManager * dd,CloudNode * n,int * support)594 static void cloudSupport( CloudManager * dd, CloudNode * n, int * support )
595 {
596 if ( cloudIsConstant(n) || cloudNodeIsMarked(n) )
597 return;
598 // set visited flag
599 cloudNodeMark(n);
600 support[cloudV(n)] = 1;
601 cloudSupport( dd, cloudT(n), support );
602 cloudSupport( dd, Cloud_Regular(cloudE(n)), support );
603 }
604
605 /**Function********************************************************************
606
607 Synopsis [Finds the variables on which a DD depends.]
608
609 Description [Finds the variables on which a DD depends.
610 Returns a BDD consisting of the product of the variables if
611 successful; NULL otherwise.]
612
613 SideEffects [None]
614
615 SeeAlso []
616
617 ******************************************************************************/
Cloud_Support(CloudManager * dd,CloudNode * n)618 CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n )
619 {
620 CloudNode * res;
621 int * support, i;
622
623 CLOUD_ASSERT(n);
624
625 // allocate and initialize support array for cloudSupport
626 support = ABC_CALLOC( int, dd->nVars );
627
628 // compute support and clean up markers
629 cloudSupport( dd, Cloud_Regular(n), support );
630 cloudClearMark( dd, Cloud_Regular(n) );
631
632 // transform support from array to cube
633 res = dd->one;
634 for ( i = dd->nVars - 1; i >= 0; i-- ) // for each level bottom-up
635 if ( support[i] == 1 )
636 {
637 res = Cloud_bddAnd( dd, res, dd->vars[i] );
638 if ( res == NULL )
639 break;
640 }
641 ABC_FREE( support );
642 return res;
643 }
644
645 /**Function********************************************************************
646
647 Synopsis [Counts the variables on which a DD depends.]
648
649 Description [Counts the variables on which a DD depends.
650 Returns the number of the variables if successful; Cloud_OUT_OF_MEM
651 otherwise.]
652
653 SideEffects [None]
654
655 SeeAlso []
656
657 ******************************************************************************/
Cloud_SupportSize(CloudManager * dd,CloudNode * n)658 int Cloud_SupportSize( CloudManager * dd, CloudNode * n )
659 {
660 int * support, i, count;
661
662 CLOUD_ASSERT(n);
663
664 // allocate and initialize support array for cloudSupport
665 support = ABC_CALLOC( int, dd->nVars );
666
667 // compute support and clean up markers
668 cloudSupport( dd, Cloud_Regular(n), support );
669 cloudClearMark( dd, Cloud_Regular(n) );
670
671 // count support variables
672 count = 0;
673 for ( i = 0; i < dd->nVars; i++ )
674 {
675 if ( support[i] == 1 )
676 count++;
677 }
678
679 ABC_FREE( support );
680 return count;
681 }
682
683
684 /**Function********************************************************************
685
686 Synopsis [Performs the recursive step of Cloud_DagSize.]
687
688 Description [Performs the recursive step of Cloud_DagSize. Returns the
689 number of nodes in the graph rooted at n.]
690
691 SideEffects [None]
692
693 ******************************************************************************/
cloudDagSize(CloudManager * dd,CloudNode * n)694 static int cloudDagSize( CloudManager * dd, CloudNode * n )
695 {
696 int tval, eval;
697 if ( cloudNodeIsMarked(n) )
698 return 0;
699 // set visited flag
700 cloudNodeMark(n);
701 if ( cloudIsConstant(n) )
702 return 1;
703 tval = cloudDagSize( dd, cloudT(n) );
704 eval = cloudDagSize( dd, Cloud_Regular(cloudE(n)) );
705 return tval + eval + 1;
706
707 }
708
709 /**Function********************************************************************
710
711 Synopsis [Counts the number of nodes in a DD.]
712
713 Description [Counts the number of nodes in a DD. Returns the number
714 of nodes in the graph rooted at node.]
715
716 SideEffects []
717
718 SeeAlso []
719
720 ******************************************************************************/
Cloud_DagSize(CloudManager * dd,CloudNode * n)721 int Cloud_DagSize( CloudManager * dd, CloudNode * n )
722 {
723 int res;
724 res = cloudDagSize( dd, Cloud_Regular( n ) );
725 cloudClearMark( dd, Cloud_Regular( n ) );
726 return res;
727
728 }
729
730
731 /**Function********************************************************************
732
733 Synopsis [Performs the recursive step of Cloud_DagSize.]
734
735 Description [Performs the recursive step of Cloud_DagSize. Returns the
736 number of nodes in the graph rooted at n.]
737
738 SideEffects [None]
739
740 ******************************************************************************/
Cloud_DagCollect_rec(CloudManager * dd,CloudNode * n,int * pCounter)741 static int Cloud_DagCollect_rec( CloudManager * dd, CloudNode * n, int * pCounter )
742 {
743 int tval, eval;
744 if ( cloudNodeIsMarked(n) )
745 return 0;
746 // set visited flag
747 cloudNodeMark(n);
748 if ( cloudIsConstant(n) )
749 {
750 dd->ppNodes[(*pCounter)++] = n;
751 return 1;
752 }
753 tval = Cloud_DagCollect_rec( dd, cloudT(n), pCounter );
754 eval = Cloud_DagCollect_rec( dd, Cloud_Regular(cloudE(n)), pCounter );
755 dd->ppNodes[(*pCounter)++] = n;
756 return tval + eval + 1;
757
758 }
759
760 /**Function********************************************************************
761
762 Synopsis [Counts the number of nodes in a DD.]
763
764 Description [Counts the number of nodes in a DD. Returns the number
765 of nodes in the graph rooted at node.]
766
767 SideEffects []
768
769 SeeAlso []
770
771 ******************************************************************************/
Cloud_DagCollect(CloudManager * dd,CloudNode * n)772 int Cloud_DagCollect( CloudManager * dd, CloudNode * n )
773 {
774 int res, Counter = 0;
775 if ( dd->ppNodes == NULL )
776 dd->ppNodes = ABC_ALLOC( CloudNode *, dd->nNodesLimit );
777 res = Cloud_DagCollect_rec( dd, Cloud_Regular( n ), &Counter );
778 cloudClearMark( dd, Cloud_Regular( n ) );
779 assert( res == Counter );
780 return res;
781
782 }
783
784 /**Function********************************************************************
785
786 Synopsis [Counts the number of nodes in an array of DDs.]
787
788 Description [Counts the number of nodes in a DD. Returns the number
789 of nodes in the graph rooted at node.]
790
791 SideEffects []
792
793 SeeAlso []
794
795 ******************************************************************************/
Cloud_SharingSize(CloudManager * dd,CloudNode ** pn,int nn)796 int Cloud_SharingSize( CloudManager * dd, CloudNode ** pn, int nn )
797 {
798 int res, i;
799 res = 0;
800 for ( i = 0; i < nn; i++ )
801 res += cloudDagSize( dd, Cloud_Regular( pn[i] ) );
802 for ( i = 0; i < nn; i++ )
803 cloudClearMark( dd, Cloud_Regular( pn[i] ) );
804 return res;
805 }
806
807
808 /**Function********************************************************************
809
810 Synopsis [Returns one cube contained in the given BDD.]
811
812 Description []
813
814 SideEffects []
815
816 ******************************************************************************/
Cloud_GetOneCube(CloudManager * dd,CloudNode * bFunc)817 CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc )
818 {
819 CloudNode * bFunc0, * bFunc1, * res;
820
821 if ( Cloud_IsConstant(bFunc) )
822 return bFunc;
823
824 // cofactor
825 if ( Cloud_IsComplement(bFunc) )
826 {
827 bFunc0 = Cloud_Not( cloudE(bFunc) );
828 bFunc1 = Cloud_Not( cloudT(bFunc) );
829 }
830 else
831 {
832 bFunc0 = cloudE(bFunc);
833 bFunc1 = cloudT(bFunc);
834 }
835
836 // try to find the cube with the negative literal
837 res = Cloud_GetOneCube( dd, bFunc0 );
838 if ( res == NULL )
839 return NULL;
840
841 if ( res != dd->zero )
842 {
843 res = Cloud_bddAnd( dd, res, Cloud_Not(dd->vars[Cloud_V(bFunc)]) );
844 }
845 else
846 {
847 // try to find the cube with the positive literal
848 res = Cloud_GetOneCube( dd, bFunc1 );
849 if ( res == NULL )
850 return NULL;
851 assert( res != dd->zero );
852 res = Cloud_bddAnd( dd, res, dd->vars[Cloud_V(bFunc)] );
853 }
854 return res;
855 }
856
857 /**Function********************************************************************
858
859 Synopsis [Prints the BDD as a set of disjoint cubes to the standard output.]
860
861 Description []
862
863 SideEffects []
864
865 ******************************************************************************/
Cloud_bddPrint(CloudManager * dd,CloudNode * Func)866 void Cloud_bddPrint( CloudManager * dd, CloudNode * Func )
867 {
868 CloudNode * Cube;
869 int fFirst = 1;
870
871 if ( Func == dd->zero )
872 printf( "Constant 0." );
873 else if ( Func == dd->one )
874 printf( "Constant 1." );
875 else
876 {
877 while ( 1 )
878 {
879 Cube = Cloud_GetOneCube( dd, Func );
880 if ( Cube == NULL || Cube == dd->zero )
881 break;
882 if ( fFirst ) fFirst = 0;
883 else printf( " + " );
884 Cloud_bddPrintCube( dd, Cube );
885 Func = Cloud_bddAnd( dd, Func, Cloud_Not(Cube) );
886 }
887 }
888 printf( "\n" );
889 }
890
891 /**Function********************************************************************
892
893 Synopsis [Prints one cube.]
894
895 Description []
896
897 SideEffects []
898
899 ******************************************************************************/
Cloud_bddPrintCube(CloudManager * dd,CloudNode * bCube)900 void Cloud_bddPrintCube( CloudManager * dd, CloudNode * bCube )
901 {
902 CloudNode * bCube0, * bCube1;
903
904 assert( !Cloud_IsConstant(bCube) );
905 while ( 1 )
906 {
907 // get the node structure
908 if ( Cloud_IsConstant(bCube) )
909 break;
910
911 // cofactor the cube
912 if ( Cloud_IsComplement(bCube) )
913 {
914 bCube0 = Cloud_Not( cloudE(bCube) );
915 bCube1 = Cloud_Not( cloudT(bCube) );
916 }
917 else
918 {
919 bCube0 = cloudE(bCube);
920 bCube1 = cloudT(bCube);
921 }
922
923 if ( bCube0 != dd->zero )
924 {
925 assert( bCube1 == dd->zero );
926 printf( "[%d]'", cloudV(bCube) );
927 bCube = bCube0;
928 }
929 else
930 {
931 assert( bCube1 != dd->zero );
932 printf( "[%d]", cloudV(bCube) );
933 bCube = bCube1;
934 }
935 }
936 }
937
938
939 /**Function********************************************************************
940
941 Synopsis [Prints info.]
942
943 Description []
944
945 SideEffects []
946
947 SeeAlso []
948
949 ******************************************************************************/
Cloud_PrintInfo(CloudManager * dd)950 void Cloud_PrintInfo( CloudManager * dd )
951 {
952 if ( dd == NULL ) return;
953 printf( "The number of unique table nodes allocated = %12d.\n", dd->nNodesAlloc );
954 printf( "The number of unique table nodes present = %12d.\n", dd->nNodesCur );
955 printf( "The number of unique table hits = %12d.\n", dd->nUniqueHits );
956 printf( "The number of unique table misses = %12d.\n", dd->nUniqueMisses );
957 printf( "The number of unique table steps = %12d.\n", dd->nUniqueSteps );
958 printf( "The number of cache hits = %12d.\n", dd->nCacheHits );
959 printf( "The number of cache misses = %12d.\n", dd->nCacheMisses );
960 printf( "The current signature = %12d.\n", dd->nSignCur );
961 printf( "The total memory in use = %12d.\n", dd->nMemUsed );
962 }
963
964 /**Function********************************************************************
965
966 Synopsis [Prints the state of the hash table.]
967
968 Description []
969
970 SideEffects []
971
972 SeeAlso []
973
974 ******************************************************************************/
Cloud_PrintHashTable(CloudManager * dd)975 void Cloud_PrintHashTable( CloudManager * dd )
976 {
977 int i;
978
979 for ( i = 0; i < dd->nNodesAlloc; i++ )
980 if ( dd->tUnique[i].v == CLOUD_CONST_INDEX )
981 printf( "-" );
982 else
983 printf( "+" );
984 printf( "\n" );
985 }
986
987
988 ////////////////////////////////////////////////////////////////////////
989 /// END OF FILE ///
990 ////////////////////////////////////////////////////////////////////////
991
992 ABC_NAMESPACE_IMPL_END
993
994