1 /**CFile****************************************************************
2
3 FileName [extraBddUnate.c]
4
5 PackageName [extra]
6
7 Synopsis [Efficient methods to compute the information about
8 unate variables using an algorithm that is conceptually similar to
9 the algorithm for two-variable symmetry computation presented in:
10 A. Mishchenko. Fast Computation of Symmetries in Boolean Functions.
11 Transactions on CAD, Nov. 2003.]
12
13 Author [Alan Mishchenko]
14
15 Affiliation [UC Berkeley]
16
17 Date [Ver. 2.0. Started - September 1, 2003.]
18
19 Revision [$Id: extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
20
21 ***********************************************************************/
22
23 #include "extraBdd.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27
28 /*---------------------------------------------------------------------------*/
29 /* Constant declarations */
30 /*---------------------------------------------------------------------------*/
31
32 /*---------------------------------------------------------------------------*/
33 /* Stucture declarations */
34 /*---------------------------------------------------------------------------*/
35
36 /*---------------------------------------------------------------------------*/
37 /* Type declarations */
38 /*---------------------------------------------------------------------------*/
39
40 /*---------------------------------------------------------------------------*/
41 /* Variable declarations */
42 /*---------------------------------------------------------------------------*/
43
44 /*---------------------------------------------------------------------------*/
45 /* Macro declarations */
46 /*---------------------------------------------------------------------------*/
47
48 /**AutomaticStart*************************************************************/
49
50 /*---------------------------------------------------------------------------*/
51 /* Static function prototypes */
52 /*---------------------------------------------------------------------------*/
53
54 /**AutomaticEnd***************************************************************/
55
56 /*---------------------------------------------------------------------------*/
57 /* Definition of exported functions */
58 /*---------------------------------------------------------------------------*/
59
60
61 /**Function********************************************************************
62
63 Synopsis [Computes the classical symmetry information for the function.]
64
65 Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.]
66
67 SideEffects [If the ZDD variables are not derived from BDD variables with
68 multiplicity 2, this function may derive them in a wrong way.]
69
70 SeeAlso []
71
72 ******************************************************************************/
Extra_UnateComputeFast(DdManager * dd,DdNode * bFunc)73 Extra_UnateInfo_t * Extra_UnateComputeFast(
74 DdManager * dd, /* the manager */
75 DdNode * bFunc) /* the function whose symmetries are computed */
76 {
77 DdNode * bSupp;
78 DdNode * zRes;
79 Extra_UnateInfo_t * p;
80
81 bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp );
82 zRes = Extra_zddUnateInfoCompute( dd, bFunc, bSupp ); Cudd_Ref( zRes );
83
84 p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp );
85
86 Cudd_RecursiveDeref( dd, bSupp );
87 Cudd_RecursiveDerefZdd( dd, zRes );
88
89 return p;
90
91 } /* end of Extra_UnateInfoCompute */
92
93
94 /**Function********************************************************************
95
96 Synopsis [Computes the classical symmetry information as a ZDD.]
97
98 Description []
99
100 SideEffects []
101
102 SeeAlso []
103
104 ******************************************************************************/
Extra_zddUnateInfoCompute(DdManager * dd,DdNode * bF,DdNode * bVars)105 DdNode * Extra_zddUnateInfoCompute(
106 DdManager * dd, /* the DD manager */
107 DdNode * bF,
108 DdNode * bVars)
109 {
110 DdNode * res;
111 do {
112 dd->reordered = 0;
113 res = extraZddUnateInfoCompute( dd, bF, bVars );
114 } while (dd->reordered == 1);
115 return(res);
116
117 } /* end of Extra_zddUnateInfoCompute */
118
119
120 /**Function********************************************************************
121
122 Synopsis [Converts a set of variables into a set of singleton subsets.]
123
124 Description []
125
126 SideEffects []
127
128 SeeAlso []
129
130 ******************************************************************************/
Extra_zddGetSingletonsBoth(DdManager * dd,DdNode * bVars)131 DdNode * Extra_zddGetSingletonsBoth(
132 DdManager * dd, /* the DD manager */
133 DdNode * bVars) /* the set of variables */
134 {
135 DdNode * res;
136 do {
137 dd->reordered = 0;
138 res = extraZddGetSingletonsBoth( dd, bVars );
139 } while (dd->reordered == 1);
140 return(res);
141
142 } /* end of Extra_zddGetSingletonsBoth */
143
144 /**Function********************************************************************
145
146 Synopsis [Allocates unateness information structure.]
147
148 Description []
149
150 SideEffects []
151
152 SeeAlso []
153
154 ******************************************************************************/
Extra_UnateInfoAllocate(int nVars)155 Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars )
156 {
157 Extra_UnateInfo_t * p;
158 // allocate and clean the storage for unateness info
159 p = ABC_ALLOC( Extra_UnateInfo_t, 1 );
160 memset( p, 0, sizeof(Extra_UnateInfo_t) );
161 p->nVars = nVars;
162 p->pVars = ABC_ALLOC( Extra_UnateVar_t, nVars );
163 memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) );
164 return p;
165 } /* end of Extra_UnateInfoAllocate */
166
167 /**Function********************************************************************
168
169 Synopsis [Deallocates symmetry information structure.]
170
171 Description []
172
173 SideEffects []
174
175 SeeAlso []
176
177 ******************************************************************************/
Extra_UnateInfoDissolve(Extra_UnateInfo_t * p)178 void Extra_UnateInfoDissolve( Extra_UnateInfo_t * p )
179 {
180 ABC_FREE( p->pVars );
181 ABC_FREE( p );
182 } /* end of Extra_UnateInfoDissolve */
183
184 /**Function********************************************************************
185
186 Synopsis [Allocates symmetry information structure.]
187
188 Description []
189
190 SideEffects []
191
192 SeeAlso []
193
194 ******************************************************************************/
Extra_UnateInfoPrint(Extra_UnateInfo_t * p)195 void Extra_UnateInfoPrint( Extra_UnateInfo_t * p )
196 {
197 char * pBuffer;
198 int i;
199 pBuffer = ABC_ALLOC( char, p->nVarsMax+1 );
200 memset( pBuffer, ' ', (size_t)p->nVarsMax );
201 pBuffer[p->nVarsMax] = 0;
202 for ( i = 0; i < p->nVars; i++ )
203 if ( p->pVars[i].Neg )
204 pBuffer[ p->pVars[i].iVar ] = 'n';
205 else if ( p->pVars[i].Pos )
206 pBuffer[ p->pVars[i].iVar ] = 'p';
207 else
208 pBuffer[ p->pVars[i].iVar ] = '.';
209 printf( "%s\n", pBuffer );
210 ABC_FREE( pBuffer );
211 } /* end of Extra_UnateInfoPrint */
212
213
214 /**Function********************************************************************
215
216 Synopsis [Creates the symmetry information structure from ZDD.]
217
218 Description [ZDD representation of symmetries is the set of cubes, each
219 of which has two variables in the positive polarity. These variables correspond
220 to the symmetric variable pair.]
221
222 SideEffects []
223
224 SeeAlso []
225
226 ******************************************************************************/
Extra_UnateInfoCreateFromZdd(DdManager * dd,DdNode * zPairs,DdNode * bSupp)227 Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp )
228 {
229 Extra_UnateInfo_t * p;
230 DdNode * bTemp, * zSet, * zCube, * zTemp;
231 int * pMapVars2Nums;
232 int i, nSuppSize;
233
234 nSuppSize = Extra_bddSuppSize( dd, bSupp );
235
236 // allocate and clean the storage for symmetry info
237 p = Extra_UnateInfoAllocate( nSuppSize );
238
239 // allocate the storage for the temporary map
240 pMapVars2Nums = ABC_ALLOC( int, dd->size );
241 memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
242
243 // assign the variables
244 p->nVarsMax = dd->size;
245 for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
246 {
247 p->pVars[i].iVar = bTemp->index;
248 pMapVars2Nums[bTemp->index] = i;
249 }
250
251 // write the symmetry info into the structure
252 zSet = zPairs; Cudd_Ref( zSet );
253 // Cudd_zddPrintCover( dd, zPairs ); printf( "\n" );
254 while ( zSet != z0 )
255 {
256 // get the next cube
257 zCube = Extra_zddSelectOneSubset( dd, zSet ); Cudd_Ref( zCube );
258
259 // add this var to the data structure
260 assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 );
261 if ( zCube->index & 1 ) // neg
262 p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1;
263 else
264 p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1;
265 // count the unate vars
266 p->nUnate++;
267
268 // update the cuver and deref the cube
269 zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube ); Cudd_Ref( zSet );
270 Cudd_RecursiveDerefZdd( dd, zTemp );
271 Cudd_RecursiveDerefZdd( dd, zCube );
272
273 } // for each cube
274 Cudd_RecursiveDerefZdd( dd, zSet );
275 ABC_FREE( pMapVars2Nums );
276 return p;
277
278 } /* end of Extra_UnateInfoCreateFromZdd */
279
280
281
282 /**Function********************************************************************
283
284 Synopsis [Computes the classical unateness information for the function.]
285
286 Description [Uses the naive way of comparing cofactors.]
287
288 SideEffects []
289
290 SeeAlso []
291
292 ******************************************************************************/
Extra_UnateComputeSlow(DdManager * dd,DdNode * bFunc)293 Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc )
294 {
295 int nSuppSize;
296 DdNode * bSupp, * bTemp;
297 Extra_UnateInfo_t * p;
298 int i, Res;
299
300 // compute the support
301 bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp );
302 nSuppSize = Extra_bddSuppSize( dd, bSupp );
303 //printf( "Support = %d. ", nSuppSize );
304 //Extra_bddPrint( dd, bSupp );
305 //printf( "%d ", nSuppSize );
306
307 // allocate the storage for symmetry info
308 p = Extra_UnateInfoAllocate( nSuppSize );
309
310 // assign the variables
311 p->nVarsMax = dd->size;
312 for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
313 {
314 Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index );
315 p->pVars[i].iVar = bTemp->index;
316 if ( Res == -1 )
317 p->pVars[i].Neg = 1;
318 else if ( Res == 1 )
319 p->pVars[i].Pos = 1;
320 p->nUnate += (Res != 0);
321 }
322 Cudd_RecursiveDeref( dd, bSupp );
323 return p;
324
325 } /* end of Extra_UnateComputeSlow */
326
327 /**Function********************************************************************
328
329 Synopsis [Checks if the two variables are symmetric.]
330
331 Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.]
332
333 SideEffects []
334
335 SeeAlso []
336
337 ******************************************************************************/
Extra_bddCheckUnateNaive(DdManager * dd,DdNode * bF,int iVar)338 int Extra_bddCheckUnateNaive(
339 DdManager * dd, /* the DD manager */
340 DdNode * bF,
341 int iVar)
342 {
343 DdNode * bCof0, * bCof1;
344 int Res;
345
346 assert( iVar < dd->size );
347
348 bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) ); Cudd_Ref( bCof0 );
349 bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) ); Cudd_Ref( bCof1 );
350
351 if ( Cudd_bddLeq( dd, bCof0, bCof1 ) )
352 Res = 1;
353 else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) )
354 Res =-1;
355 else
356 Res = 0;
357
358 Cudd_RecursiveDeref( dd, bCof0 );
359 Cudd_RecursiveDeref( dd, bCof1 );
360 return Res;
361 } /* end of Extra_bddCheckUnateNaive */
362
363
364
365 /*---------------------------------------------------------------------------*/
366 /* Definition of internal functions */
367 /*---------------------------------------------------------------------------*/
368
369 /**Function********************************************************************
370
371 Synopsis [Performs a recursive step of Extra_UnateInfoCompute.]
372
373 Description [Returns the set of symmetric variable pairs represented as a set
374 of two-literal ZDD cubes. Both variables always appear in the positive polarity
375 in the cubes. This function works without building new BDD nodes. Some relatively
376 small number of ZDD nodes may be built to ensure proper bookkeeping of the
377 symmetry information.]
378
379 SideEffects []
380
381 SeeAlso []
382
383 ******************************************************************************/
384 DdNode *
extraZddUnateInfoCompute(DdManager * dd,DdNode * bFunc,DdNode * bVars)385 extraZddUnateInfoCompute(
386 DdManager * dd, /* the manager */
387 DdNode * bFunc, /* the function whose symmetries are computed */
388 DdNode * bVars ) /* the set of variables on which this function depends */
389 {
390 DdNode * zRes;
391 DdNode * bFR = Cudd_Regular(bFunc);
392
393 if ( cuddIsConstant(bFR) )
394 {
395 if ( cuddIsConstant(bVars) )
396 return z0;
397 return extraZddGetSingletonsBoth( dd, bVars );
398 }
399 assert( bVars != b1 );
400
401 if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars)) )
402 return zRes;
403 else
404 {
405 DdNode * zRes0, * zRes1;
406 DdNode * zTemp, * zPlus;
407 DdNode * bF0, * bF1;
408 DdNode * bVarsNew;
409 int nVarsExtra;
410 int LevelF;
411 int AddVar;
412
413 // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
414 // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
415 // count how many extra vars are there in bVars
416 nVarsExtra = 0;
417 LevelF = dd->perm[bFR->index];
418 for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
419 nVarsExtra++;
420 // the indexes (level) of variables should be synchronized now
421 assert( bFR->index == bVarsNew->index );
422
423 // cofactor the function
424 if ( bFR != bFunc ) // bFunc is complemented
425 {
426 bF0 = Cudd_Not( cuddE(bFR) );
427 bF1 = Cudd_Not( cuddT(bFR) );
428 }
429 else
430 {
431 bF0 = cuddE(bFR);
432 bF1 = cuddT(bFR);
433 }
434
435 // solve subproblems
436 zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) );
437 if ( zRes0 == NULL )
438 return NULL;
439 cuddRef( zRes0 );
440
441 // if there is no symmetries in the negative cofactor
442 // there is no need to test the positive cofactor
443 if ( zRes0 == z0 )
444 zRes = zRes0; // zRes takes reference
445 else
446 {
447 zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) );
448 if ( zRes1 == NULL )
449 {
450 Cudd_RecursiveDerefZdd( dd, zRes0 );
451 return NULL;
452 }
453 cuddRef( zRes1 );
454
455 // only those variables are pair-wise symmetric
456 // that are pair-wise symmetric in both cofactors
457 // therefore, intersect the solutions
458 zRes = cuddZddIntersect( dd, zRes0, zRes1 );
459 if ( zRes == NULL )
460 {
461 Cudd_RecursiveDerefZdd( dd, zRes0 );
462 Cudd_RecursiveDerefZdd( dd, zRes1 );
463 return NULL;
464 }
465 cuddRef( zRes );
466 Cudd_RecursiveDerefZdd( dd, zRes0 );
467 Cudd_RecursiveDerefZdd( dd, zRes1 );
468 }
469
470 // consider the current top-most variable
471 AddVar = -1;
472 if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos
473 AddVar = 0;
474 else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg
475 AddVar = 1;
476 if ( AddVar >= 0 )
477 {
478 // create the singleton
479 zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 );
480 if ( zPlus == NULL )
481 {
482 Cudd_RecursiveDerefZdd( dd, zRes );
483 return NULL;
484 }
485 cuddRef( zPlus );
486
487 // add these to the result
488 zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
489 if ( zRes == NULL )
490 {
491 Cudd_RecursiveDerefZdd( dd, zTemp );
492 Cudd_RecursiveDerefZdd( dd, zPlus );
493 return NULL;
494 }
495 cuddRef( zRes );
496 Cudd_RecursiveDerefZdd( dd, zTemp );
497 Cudd_RecursiveDerefZdd( dd, zPlus );
498 }
499 // only zRes is referenced at this point
500
501 // if we skipped some variables, these variables cannot be symmetric with
502 // any variables that are currently in the support of bF, but they can be
503 // symmetric with the variables that are in bVars but not in the support of bF
504 for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
505 {
506 // create the negative singleton
507 zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 );
508 if ( zPlus == NULL )
509 {
510 Cudd_RecursiveDerefZdd( dd, zRes );
511 return NULL;
512 }
513 cuddRef( zPlus );
514
515 // add these to the result
516 zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
517 if ( zRes == NULL )
518 {
519 Cudd_RecursiveDerefZdd( dd, zTemp );
520 Cudd_RecursiveDerefZdd( dd, zPlus );
521 return NULL;
522 }
523 cuddRef( zRes );
524 Cudd_RecursiveDerefZdd( dd, zTemp );
525 Cudd_RecursiveDerefZdd( dd, zPlus );
526
527
528 // create the positive singleton
529 zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
530 if ( zPlus == NULL )
531 {
532 Cudd_RecursiveDerefZdd( dd, zRes );
533 return NULL;
534 }
535 cuddRef( zPlus );
536
537 // add these to the result
538 zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
539 if ( zRes == NULL )
540 {
541 Cudd_RecursiveDerefZdd( dd, zTemp );
542 Cudd_RecursiveDerefZdd( dd, zPlus );
543 return NULL;
544 }
545 cuddRef( zRes );
546 Cudd_RecursiveDerefZdd( dd, zTemp );
547 Cudd_RecursiveDerefZdd( dd, zPlus );
548 }
549 cuddDeref( zRes );
550
551 /* insert the result into cache */
552 cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes);
553 return zRes;
554 }
555 } /* end of extraZddUnateInfoCompute */
556
557
558 /**Function********************************************************************
559
560 Synopsis [Performs a recursive step of Extra_zddGetSingletons.]
561
562 Description [Returns the set of ZDD singletons, containing those pos/neg
563 polarity ZDD variables that correspond to the BDD variables in bVars.]
564
565 SideEffects []
566
567 SeeAlso []
568
569 ******************************************************************************/
extraZddGetSingletonsBoth(DdManager * dd,DdNode * bVars)570 DdNode * extraZddGetSingletonsBoth(
571 DdManager * dd, /* the DD manager */
572 DdNode * bVars) /* the set of variables */
573 {
574 DdNode * zRes;
575
576 if ( bVars == b1 )
577 return z1;
578
579 if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars)) )
580 return zRes;
581 else
582 {
583 DdNode * zTemp, * zPlus;
584
585 // solve subproblem
586 zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) );
587 if ( zRes == NULL )
588 return NULL;
589 cuddRef( zRes );
590
591
592 // create the negative singleton
593 zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 );
594 if ( zPlus == NULL )
595 {
596 Cudd_RecursiveDerefZdd( dd, zRes );
597 return NULL;
598 }
599 cuddRef( zPlus );
600
601 // add these to the result
602 zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
603 if ( zRes == NULL )
604 {
605 Cudd_RecursiveDerefZdd( dd, zTemp );
606 Cudd_RecursiveDerefZdd( dd, zPlus );
607 return NULL;
608 }
609 cuddRef( zRes );
610 Cudd_RecursiveDerefZdd( dd, zTemp );
611 Cudd_RecursiveDerefZdd( dd, zPlus );
612
613
614 // create the positive singleton
615 zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
616 if ( zPlus == NULL )
617 {
618 Cudd_RecursiveDerefZdd( dd, zRes );
619 return NULL;
620 }
621 cuddRef( zPlus );
622
623 // add these to the result
624 zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
625 if ( zRes == NULL )
626 {
627 Cudd_RecursiveDerefZdd( dd, zTemp );
628 Cudd_RecursiveDerefZdd( dd, zPlus );
629 return NULL;
630 }
631 cuddRef( zRes );
632 Cudd_RecursiveDerefZdd( dd, zTemp );
633 Cudd_RecursiveDerefZdd( dd, zPlus );
634
635 cuddDeref( zRes );
636 cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes );
637 return zRes;
638 }
639 } /* end of extraZddGetSingletonsBoth */
640
641
642 /*---------------------------------------------------------------------------*/
643 /* Definition of static Functions */
644 /*---------------------------------------------------------------------------*/
645 ABC_NAMESPACE_IMPL_END
646
647