1 /**CFile****************************************************************
2
3 FileName [extraBddAuto.c]
4
5 PackageName [extra]
6
7 Synopsis [Computation of autosymmetries.]
8
9 Author [Alan Mishchenko]
10
11 Affiliation [UC Berkeley]
12
13 Date [Ver. 2.0. Started - September 1, 2003.]
14
15 Revision [$Id: extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
16
17 ***********************************************************************/
18
19 #include "extraBdd.h"
20
21 ABC_NAMESPACE_IMPL_START
22
23
24 /*---------------------------------------------------------------------------*/
25 /* Constant declarations */
26 /*---------------------------------------------------------------------------*/
27
28 /*---------------------------------------------------------------------------*/
29 /* Stucture declarations */
30 /*---------------------------------------------------------------------------*/
31
32 /*---------------------------------------------------------------------------*/
33 /* Type declarations */
34 /*---------------------------------------------------------------------------*/
35
36 /*---------------------------------------------------------------------------*/
37 /* Variable declarations */
38 /*---------------------------------------------------------------------------*/
39
40 /*---------------------------------------------------------------------------*/
41 /* Macro declarations */
42 /*---------------------------------------------------------------------------*/
43
44
45 /**AutomaticStart*************************************************************/
46
47 /*---------------------------------------------------------------------------*/
48 /* Static function prototypes */
49 /*---------------------------------------------------------------------------*/
50
51 /**AutomaticEnd***************************************************************/
52
53
54 /*
55 LinearSpace(f) = Space(f,f)
56
57 Space(f,g)
58 {
59 if ( f = const )
60 {
61 if ( f = g ) return 1;
62 else return 0;
63 }
64 if ( g = const ) return 0;
65 return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx');
66 }
67
68 Equations(s) = Pos(s) + Neg(s);
69
70 Pos(s)
71 {
72 if ( s = 0 ) return 1;
73 if ( s = 1 ) return 0;
74 if ( sx'= 0 ) return Pos(sx) + x;
75 if ( sx = 0 ) return Pos(sx');
76 return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)];
77 }
78
79 Neg(s)
80 {
81 if ( s = 0 ) return 1;
82 if ( s = 1 ) return 0;
83 if ( sx'= 0 ) return Neg(sx);
84 if ( sx = 0 ) return Neg(sx') + x;
85 return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)];
86 }
87
88
89 SpaceP(A)
90 {
91 if ( A = 0 ) return 1;
92 if ( A = 1 ) return 1;
93 return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax);
94 }
95
96 SpaceN(A)
97 {
98 if ( A = 0 ) return 1;
99 if ( A = 1 ) return 0;
100 return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax);
101 }
102
103
104 LinInd(A)
105 {
106 if ( A = const ) return 1;
107 if ( !LinInd(Ax') ) return 0;
108 if ( !LinInd(Ax) ) return 0;
109 if ( LinSumOdd(Ax') & LinSumEven(Ax) != 0 ) return 0;
110 if ( LinSumEven(Ax') & LinSumEven(Ax) != 0 ) return 0;
111 return 1;
112 }
113
114 LinSumOdd(A)
115 {
116 if ( A = 0 ) return 0; // Odd0 ---e-- Odd1
117 if ( A = 1 ) return 1; // \ o
118 Odd0 = LinSumOdd(Ax'); // x is absent // \
119 Even0 = LinSumEven(Ax'); // x is absent // / o
120 Odd1 = LinSumOdd(Ax); // x is present // Even0 ---e-- Even1
121 Even1 = LinSumEven(Ax); // x is absent
122 return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)];
123 }
124
125 LinSumEven(A)
126 {
127 if ( A = 0 ) return 0;
128 if ( A = 1 ) return 0;
129 Odd0 = LinSumOdd(Ax'); // x is absent
130 Even0 = LinSumEven(Ax'); // x is absent
131 Odd1 = LinSumOdd(Ax); // x is present
132 Even1 = LinSumEven(Ax); // x is absent
133 return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)];
134 }
135
136 */
137
138 /*---------------------------------------------------------------------------*/
139 /* Definition of exported functions */
140 /*---------------------------------------------------------------------------*/
141
142 /**Function*************************************************************
143
144 Synopsis []
145
146 Description []
147
148 SideEffects []
149
150 SeeAlso []
151
152 ***********************************************************************/
Extra_bddSpaceFromFunctionFast(DdManager * dd,DdNode * bFunc)153 DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
154 {
155 int * pSupport;
156 int * pPermute;
157 int * pPermuteBack;
158 DdNode ** pCompose;
159 DdNode * bCube, * bTemp;
160 DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift;
161 int nSupp, Counter;
162 int i, lev;
163
164 // get the support
165 pSupport = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
166 Extra_SupportArray( dd, bFunc, pSupport );
167 nSupp = 0;
168 for ( i = 0; i < dd->size; i++ )
169 if ( pSupport[i] )
170 nSupp++;
171
172 // make sure the manager has enough variables
173 if ( 2*nSupp > dd->size )
174 {
175 printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" );
176 fflush( stdout );
177 ABC_FREE( pSupport );
178 return NULL;
179 }
180
181 // create the permutation arrays
182 pPermute = ABC_ALLOC( int, dd->size );
183 pPermuteBack = ABC_ALLOC( int, dd->size );
184 pCompose = ABC_ALLOC( DdNode *, dd->size );
185 for ( i = 0; i < dd->size; i++ )
186 {
187 pPermute[i] = i;
188 pPermuteBack[i] = i;
189 pCompose[i] = dd->vars[i]; Cudd_Ref( pCompose[i] );
190 }
191
192 // remap the function in such a way that the variables are interleaved
193 Counter = 0;
194 bCube = b1; Cudd_Ref( bCube );
195 for ( lev = 0; lev < dd->size; lev++ )
196 if ( pSupport[ dd->invperm[lev] ] )
197 { // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter;
198 pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter];
199 // var from level 2*Counter+1 should go back to the place of this var
200 pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev];
201 // the permutation should be defined in such a way that variable
202 // on level 2*Counter is replaced by an EXOR of itself and var on the next level
203 Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] );
204 pCompose[ dd->invperm[2*Counter] ] =
205 Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] );
206 Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] );
207 // add this variable to the cube
208 bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] ); Cudd_Ref( bCube );
209 Cudd_RecursiveDeref( dd, bTemp );
210 // increment the counter
211 Counter ++;
212 }
213
214 // permute the functions
215 bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute ); Cudd_Ref( bFunc1 );
216 // compose to gate the function depending on both vars
217 bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose ); Cudd_Ref( bFunc2 );
218 // gate the vector space
219 // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] )
220 bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube ); Cudd_Ref( bSpaceShift );
221 bSpaceShift = Cudd_Not( bSpaceShift );
222 // permute the space back into the original mapping
223 bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace );
224 Cudd_RecursiveDeref( dd, bFunc1 );
225 Cudd_RecursiveDeref( dd, bFunc2 );
226 Cudd_RecursiveDeref( dd, bSpaceShift );
227 Cudd_RecursiveDeref( dd, bCube );
228
229 for ( i = 0; i < dd->size; i++ )
230 Cudd_RecursiveDeref( dd, pCompose[i] );
231 ABC_FREE( pPermute );
232 ABC_FREE( pPermuteBack );
233 ABC_FREE( pCompose );
234 ABC_FREE( pSupport );
235
236 Cudd_Deref( bSpace );
237 return bSpace;
238 }
239
240
241
242 /**Function*************************************************************
243
244 Synopsis []
245
246 Description []
247
248 SideEffects []
249
250 SeeAlso []
251
252 ***********************************************************************/
Extra_bddSpaceFromFunction(DdManager * dd,DdNode * bF,DdNode * bG)253 DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
254 {
255 DdNode * bRes;
256 do {
257 dd->reordered = 0;
258 bRes = extraBddSpaceFromFunction( dd, bF, bG );
259 } while (dd->reordered == 1);
260 return bRes;
261 }
262
263 /**Function*************************************************************
264
265 Synopsis []
266
267 Description []
268
269 SideEffects []
270
271 SeeAlso []
272
273 ***********************************************************************/
Extra_bddSpaceFromFunctionPos(DdManager * dd,DdNode * bFunc)274 DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc )
275 {
276 DdNode * bRes;
277 do {
278 dd->reordered = 0;
279 bRes = extraBddSpaceFromFunctionPos( dd, bFunc );
280 } while (dd->reordered == 1);
281 return bRes;
282 }
283
284 /**Function*************************************************************
285
286 Synopsis []
287
288 Description []
289
290 SideEffects []
291
292 SeeAlso []
293
294 ***********************************************************************/
Extra_bddSpaceFromFunctionNeg(DdManager * dd,DdNode * bFunc)295 DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc )
296 {
297 DdNode * bRes;
298 do {
299 dd->reordered = 0;
300 bRes = extraBddSpaceFromFunctionNeg( dd, bFunc );
301 } while (dd->reordered == 1);
302 return bRes;
303 }
304
305 /**Function*************************************************************
306
307 Synopsis []
308
309 Description []
310
311 SideEffects []
312
313 SeeAlso []
314
315 ***********************************************************************/
Extra_bddSpaceCanonVars(DdManager * dd,DdNode * bSpace)316 DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace )
317 {
318 DdNode * bRes;
319 do {
320 dd->reordered = 0;
321 bRes = extraBddSpaceCanonVars( dd, bSpace );
322 } while (dd->reordered == 1);
323 return bRes;
324 }
325
326 /**Function*************************************************************
327
328 Synopsis []
329
330 Description []
331
332 SideEffects []
333
334 SeeAlso []
335
336 ***********************************************************************/
Extra_bddSpaceReduce(DdManager * dd,DdNode * bFunc,DdNode * bCanonVars)337 DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars )
338 {
339 DdNode * bNegCube;
340 DdNode * bResult;
341 bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars ); Cudd_Ref( bNegCube );
342 bResult = Cudd_Cofactor( dd, bFunc, bNegCube ); Cudd_Ref( bResult );
343 Cudd_RecursiveDeref( dd, bNegCube );
344 Cudd_Deref( bResult );
345 return bResult;
346 }
347
348
349
350 /**Function*************************************************************
351
352 Synopsis []
353
354 Description []
355
356 SideEffects []
357
358 SeeAlso []
359
360 ***********************************************************************/
Extra_bddSpaceEquations(DdManager * dd,DdNode * bSpace)361 DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace )
362 {
363 DdNode * zRes;
364 DdNode * zEquPos;
365 DdNode * zEquNeg;
366 zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace ); Cudd_Ref( zEquPos );
367 zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace ); Cudd_Ref( zEquNeg );
368 zRes = Cudd_zddUnion( dd, zEquPos, zEquNeg ); Cudd_Ref( zRes );
369 Cudd_RecursiveDerefZdd( dd, zEquPos );
370 Cudd_RecursiveDerefZdd( dd, zEquNeg );
371 Cudd_Deref( zRes );
372 return zRes;
373 }
374
375
376 /**Function*************************************************************
377
378 Synopsis []
379
380 Description []
381
382 SideEffects []
383
384 SeeAlso []
385
386 ***********************************************************************/
Extra_bddSpaceEquationsPos(DdManager * dd,DdNode * bSpace)387 DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace )
388 {
389 DdNode * zRes;
390 do {
391 dd->reordered = 0;
392 zRes = extraBddSpaceEquationsPos( dd, bSpace );
393 } while (dd->reordered == 1);
394 return zRes;
395 }
396
397
398 /**Function*************************************************************
399
400 Synopsis []
401
402 Description []
403
404 SideEffects []
405
406 SeeAlso []
407
408 ***********************************************************************/
Extra_bddSpaceEquationsNeg(DdManager * dd,DdNode * bSpace)409 DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace )
410 {
411 DdNode * zRes;
412 do {
413 dd->reordered = 0;
414 zRes = extraBddSpaceEquationsNeg( dd, bSpace );
415 } while (dd->reordered == 1);
416 return zRes;
417 }
418
419
420 /**Function*************************************************************
421
422 Synopsis []
423
424 Description []
425
426 SideEffects []
427
428 SeeAlso []
429
430 ***********************************************************************/
Extra_bddSpaceFromMatrixPos(DdManager * dd,DdNode * zA)431 DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
432 {
433 DdNode * bRes;
434 do {
435 dd->reordered = 0;
436 bRes = extraBddSpaceFromMatrixPos( dd, zA );
437 } while (dd->reordered == 1);
438 return bRes;
439 }
440
441 /**Function*************************************************************
442
443 Synopsis []
444
445 Description []
446
447 SideEffects []
448
449 SeeAlso []
450
451 ***********************************************************************/
Extra_bddSpaceFromMatrixNeg(DdManager * dd,DdNode * zA)452 DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
453 {
454 DdNode * bRes;
455 do {
456 dd->reordered = 0;
457 bRes = extraBddSpaceFromMatrixNeg( dd, zA );
458 } while (dd->reordered == 1);
459 return bRes;
460 }
461
462 /**Function*************************************************************
463
464 Synopsis [Counts the number of literals in one combination.]
465
466 Description []
467
468 SideEffects []
469
470 SeeAlso []
471
472 ***********************************************************************/
Extra_zddLitCountComb(DdManager * dd,DdNode * zComb)473 int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb )
474 {
475 int Counter;
476 if ( zComb == z0 )
477 return 0;
478 Counter = 0;
479 for ( ; zComb != z1; zComb = cuddT(zComb) )
480 Counter++;
481 return Counter;
482 }
483
484 /**Function*************************************************************
485
486 Synopsis []
487
488 Description [Returns the array of ZDDs with the number equal to the number of
489 vars in the DD manager. If the given var is non-canonical, this array contains
490 the referenced ZDD representing literals in the corresponding EXOR equation.]
491
492 SideEffects []
493
494 SeeAlso []
495
496 ***********************************************************************/
Extra_bddSpaceExorGates(DdManager * dd,DdNode * bFuncRed,DdNode * zEquations)497 DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations )
498 {
499 DdNode ** pzRes;
500 int * pVarsNonCan;
501 DdNode * zEquRem;
502 int iVarNonCan;
503 DdNode * zExor, * zTemp;
504
505 // get the set of non-canonical variables
506 pVarsNonCan = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
507 Extra_SupportArray( dd, bFuncRed, pVarsNonCan );
508
509 // allocate storage for the EXOR sets
510 pzRes = ABC_ALLOC( DdNode *, dd->size );
511 memset( pzRes, 0, sizeof(DdNode *) * dd->size );
512
513 // go through all the equations
514 zEquRem = zEquations; Cudd_Ref( zEquRem );
515 while ( zEquRem != z0 )
516 {
517 // extract one product
518 zExor = Extra_zddSelectOneSubset( dd, zEquRem ); Cudd_Ref( zExor );
519 // remove it from the set
520 zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor ); Cudd_Ref( zEquRem );
521 Cudd_RecursiveDerefZdd( dd, zTemp );
522
523 // locate the non-canonical variable
524 iVarNonCan = -1;
525 for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) )
526 {
527 if ( pVarsNonCan[zTemp->index/2] == 1 )
528 {
529 assert( iVarNonCan == -1 );
530 iVarNonCan = zTemp->index/2;
531 }
532 }
533 assert( iVarNonCan != -1 );
534
535 if ( Extra_zddLitCountComb( dd, zExor ) > 1 )
536 pzRes[ iVarNonCan ] = zExor; // takes ref
537 else
538 Cudd_RecursiveDerefZdd( dd, zExor );
539 }
540 Cudd_RecursiveDerefZdd( dd, zEquRem );
541
542 ABC_FREE( pVarsNonCan );
543 return pzRes;
544 }
545
546
547 /*---------------------------------------------------------------------------*/
548 /* Definition of internal functions */
549 /*---------------------------------------------------------------------------*/
550
551 /**Function********************************************************************
552
553 Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.]
554
555 Description []
556
557 SideEffects []
558
559 SeeAlso []
560
561 ******************************************************************************/
extraBddSpaceFromFunction(DdManager * dd,DdNode * bF,DdNode * bG)562 DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
563 {
564 DdNode * bRes;
565 DdNode * bFR, * bGR;
566
567 bFR = Cudd_Regular( bF );
568 bGR = Cudd_Regular( bG );
569 if ( cuddIsConstant(bFR) )
570 {
571 if ( bF == bG )
572 return b1;
573 else
574 return b0;
575 }
576 if ( cuddIsConstant(bGR) )
577 return b0;
578 // both bFunc and bCore are not constants
579
580 // the operation is commutative - normalize the problem
581 if ( (unsigned)(ABC_PTRUINT_T)bF > (unsigned)(ABC_PTRUINT_T)bG )
582 return extraBddSpaceFromFunction(dd, bG, bF);
583
584
585 if ( (bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG)) )
586 return bRes;
587 else
588 {
589 DdNode * bF0, * bF1;
590 DdNode * bG0, * bG1;
591 DdNode * bTemp1, * bTemp2;
592 DdNode * bRes0, * bRes1;
593 int LevelF, LevelG;
594 int index;
595
596 LevelF = dd->perm[bFR->index];
597 LevelG = dd->perm[bGR->index];
598 if ( LevelF <= LevelG )
599 {
600 index = dd->invperm[LevelF];
601 if ( bFR != bF )
602 {
603 bF0 = Cudd_Not( cuddE(bFR) );
604 bF1 = Cudd_Not( cuddT(bFR) );
605 }
606 else
607 {
608 bF0 = cuddE(bFR);
609 bF1 = cuddT(bFR);
610 }
611 }
612 else
613 {
614 index = dd->invperm[LevelG];
615 bF0 = bF1 = bF;
616 }
617
618 if ( LevelG <= LevelF )
619 {
620 if ( bGR != bG )
621 {
622 bG0 = Cudd_Not( cuddE(bGR) );
623 bG1 = Cudd_Not( cuddT(bGR) );
624 }
625 else
626 {
627 bG0 = cuddE(bGR);
628 bG1 = cuddT(bGR);
629 }
630 }
631 else
632 bG0 = bG1 = bG;
633
634 bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 );
635 if ( bTemp1 == NULL )
636 return NULL;
637 cuddRef( bTemp1 );
638
639 bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 );
640 if ( bTemp2 == NULL )
641 {
642 Cudd_RecursiveDeref( dd, bTemp1 );
643 return NULL;
644 }
645 cuddRef( bTemp2 );
646
647
648 bRes0 = cuddBddAndRecur( dd, bTemp1, bTemp2 );
649 if ( bRes0 == NULL )
650 {
651 Cudd_RecursiveDeref( dd, bTemp1 );
652 Cudd_RecursiveDeref( dd, bTemp2 );
653 return NULL;
654 }
655 cuddRef( bRes0 );
656 Cudd_RecursiveDeref( dd, bTemp1 );
657 Cudd_RecursiveDeref( dd, bTemp2 );
658
659
660 bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG1 );
661 if ( bTemp1 == NULL )
662 {
663 Cudd_RecursiveDeref( dd, bRes0 );
664 return NULL;
665 }
666 cuddRef( bTemp1 );
667
668 bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG0 );
669 if ( bTemp2 == NULL )
670 {
671 Cudd_RecursiveDeref( dd, bRes0 );
672 Cudd_RecursiveDeref( dd, bTemp1 );
673 return NULL;
674 }
675 cuddRef( bTemp2 );
676
677 bRes1 = cuddBddAndRecur( dd, bTemp1, bTemp2 );
678 if ( bRes1 == NULL )
679 {
680 Cudd_RecursiveDeref( dd, bRes0 );
681 Cudd_RecursiveDeref( dd, bTemp1 );
682 Cudd_RecursiveDeref( dd, bTemp2 );
683 return NULL;
684 }
685 cuddRef( bRes1 );
686 Cudd_RecursiveDeref( dd, bTemp1 );
687 Cudd_RecursiveDeref( dd, bTemp2 );
688
689
690
691 // consider the case when Res0 and Res1 are the same node
692 if ( bRes0 == bRes1 )
693 bRes = bRes1;
694 // consider the case when Res1 is complemented
695 else if ( Cudd_IsComplement(bRes1) )
696 {
697 bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0));
698 if ( bRes == NULL )
699 {
700 Cudd_RecursiveDeref(dd,bRes0);
701 Cudd_RecursiveDeref(dd,bRes1);
702 return NULL;
703 }
704 bRes = Cudd_Not(bRes);
705 }
706 else
707 {
708 bRes = cuddUniqueInter( dd, index, bRes1, bRes0 );
709 if ( bRes == NULL )
710 {
711 Cudd_RecursiveDeref(dd,bRes0);
712 Cudd_RecursiveDeref(dd,bRes1);
713 return NULL;
714 }
715 }
716 cuddDeref( bRes0 );
717 cuddDeref( bRes1 );
718
719 // insert the result into cache
720 cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes);
721 return bRes;
722 }
723 } /* end of extraBddSpaceFromFunction */
724
725
726
727 /**Function*************************************************************
728
729 Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
730
731 Description []
732
733 SideEffects []
734
735 SeeAlso []
736
737 ***********************************************************************/
extraBddSpaceFromFunctionPos(DdManager * dd,DdNode * bF)738 DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF )
739 {
740 DdNode * bRes, * bFR;
741 statLine( dd );
742
743 bFR = Cudd_Regular(bF);
744 if ( cuddIsConstant(bFR) )
745 return b1;
746
747 if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF)) )
748 return bRes;
749 else
750 {
751 DdNode * bF0, * bF1;
752 DdNode * bPos0, * bPos1;
753 DdNode * bNeg0, * bNeg1;
754 DdNode * bRes0, * bRes1;
755
756 if ( bFR != bF ) // bF is complemented
757 {
758 bF0 = Cudd_Not( cuddE(bFR) );
759 bF1 = Cudd_Not( cuddT(bFR) );
760 }
761 else
762 {
763 bF0 = cuddE(bFR);
764 bF1 = cuddT(bFR);
765 }
766
767
768 bPos0 = extraBddSpaceFromFunctionPos( dd, bF0 );
769 if ( bPos0 == NULL )
770 return NULL;
771 cuddRef( bPos0 );
772
773 bPos1 = extraBddSpaceFromFunctionPos( dd, bF1 );
774 if ( bPos1 == NULL )
775 {
776 Cudd_RecursiveDeref( dd, bPos0 );
777 return NULL;
778 }
779 cuddRef( bPos1 );
780
781 bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 );
782 if ( bRes0 == NULL )
783 {
784 Cudd_RecursiveDeref( dd, bPos0 );
785 Cudd_RecursiveDeref( dd, bPos1 );
786 return NULL;
787 }
788 cuddRef( bRes0 );
789 Cudd_RecursiveDeref( dd, bPos0 );
790 Cudd_RecursiveDeref( dd, bPos1 );
791
792
793 bNeg0 = extraBddSpaceFromFunctionNeg( dd, bF0 );
794 if ( bNeg0 == NULL )
795 {
796 Cudd_RecursiveDeref( dd, bRes0 );
797 return NULL;
798 }
799 cuddRef( bNeg0 );
800
801 bNeg1 = extraBddSpaceFromFunctionNeg( dd, bF1 );
802 if ( bNeg1 == NULL )
803 {
804 Cudd_RecursiveDeref( dd, bRes0 );
805 Cudd_RecursiveDeref( dd, bNeg0 );
806 return NULL;
807 }
808 cuddRef( bNeg1 );
809
810 bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 );
811 if ( bRes1 == NULL )
812 {
813 Cudd_RecursiveDeref( dd, bRes0 );
814 Cudd_RecursiveDeref( dd, bNeg0 );
815 Cudd_RecursiveDeref( dd, bNeg1 );
816 return NULL;
817 }
818 cuddRef( bRes1 );
819 Cudd_RecursiveDeref( dd, bNeg0 );
820 Cudd_RecursiveDeref( dd, bNeg1 );
821
822
823 // consider the case when Res0 and Res1 are the same node
824 if ( bRes0 == bRes1 )
825 bRes = bRes1;
826 // consider the case when Res1 is complemented
827 else if ( Cudd_IsComplement(bRes1) )
828 {
829 bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
830 if ( bRes == NULL )
831 {
832 Cudd_RecursiveDeref(dd,bRes0);
833 Cudd_RecursiveDeref(dd,bRes1);
834 return NULL;
835 }
836 bRes = Cudd_Not(bRes);
837 }
838 else
839 {
840 bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
841 if ( bRes == NULL )
842 {
843 Cudd_RecursiveDeref(dd,bRes0);
844 Cudd_RecursiveDeref(dd,bRes1);
845 return NULL;
846 }
847 }
848 cuddDeref( bRes0 );
849 cuddDeref( bRes1 );
850
851 cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes );
852 return bRes;
853 }
854 }
855
856
857
858 /**Function*************************************************************
859
860 Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
861
862 Description []
863
864 SideEffects []
865
866 SeeAlso []
867
868 ***********************************************************************/
extraBddSpaceFromFunctionNeg(DdManager * dd,DdNode * bF)869 DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF )
870 {
871 DdNode * bRes, * bFR;
872 statLine( dd );
873
874 bFR = Cudd_Regular(bF);
875 if ( cuddIsConstant(bFR) )
876 return b0;
877
878 if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF)) )
879 return bRes;
880 else
881 {
882 DdNode * bF0, * bF1;
883 DdNode * bPos0, * bPos1;
884 DdNode * bNeg0, * bNeg1;
885 DdNode * bRes0, * bRes1;
886
887 if ( bFR != bF ) // bF is complemented
888 {
889 bF0 = Cudd_Not( cuddE(bFR) );
890 bF1 = Cudd_Not( cuddT(bFR) );
891 }
892 else
893 {
894 bF0 = cuddE(bFR);
895 bF1 = cuddT(bFR);
896 }
897
898
899 bPos0 = extraBddSpaceFromFunctionNeg( dd, bF0 );
900 if ( bPos0 == NULL )
901 return NULL;
902 cuddRef( bPos0 );
903
904 bPos1 = extraBddSpaceFromFunctionNeg( dd, bF1 );
905 if ( bPos1 == NULL )
906 {
907 Cudd_RecursiveDeref( dd, bPos0 );
908 return NULL;
909 }
910 cuddRef( bPos1 );
911
912 bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 );
913 if ( bRes0 == NULL )
914 {
915 Cudd_RecursiveDeref( dd, bPos0 );
916 Cudd_RecursiveDeref( dd, bPos1 );
917 return NULL;
918 }
919 cuddRef( bRes0 );
920 Cudd_RecursiveDeref( dd, bPos0 );
921 Cudd_RecursiveDeref( dd, bPos1 );
922
923
924 bNeg0 = extraBddSpaceFromFunctionPos( dd, bF0 );
925 if ( bNeg0 == NULL )
926 {
927 Cudd_RecursiveDeref( dd, bRes0 );
928 return NULL;
929 }
930 cuddRef( bNeg0 );
931
932 bNeg1 = extraBddSpaceFromFunctionPos( dd, bF1 );
933 if ( bNeg1 == NULL )
934 {
935 Cudd_RecursiveDeref( dd, bRes0 );
936 Cudd_RecursiveDeref( dd, bNeg0 );
937 return NULL;
938 }
939 cuddRef( bNeg1 );
940
941 bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 );
942 if ( bRes1 == NULL )
943 {
944 Cudd_RecursiveDeref( dd, bRes0 );
945 Cudd_RecursiveDeref( dd, bNeg0 );
946 Cudd_RecursiveDeref( dd, bNeg1 );
947 return NULL;
948 }
949 cuddRef( bRes1 );
950 Cudd_RecursiveDeref( dd, bNeg0 );
951 Cudd_RecursiveDeref( dd, bNeg1 );
952
953
954 // consider the case when Res0 and Res1 are the same node
955 if ( bRes0 == bRes1 )
956 bRes = bRes1;
957 // consider the case when Res1 is complemented
958 else if ( Cudd_IsComplement(bRes1) )
959 {
960 bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
961 if ( bRes == NULL )
962 {
963 Cudd_RecursiveDeref(dd,bRes0);
964 Cudd_RecursiveDeref(dd,bRes1);
965 return NULL;
966 }
967 bRes = Cudd_Not(bRes);
968 }
969 else
970 {
971 bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
972 if ( bRes == NULL )
973 {
974 Cudd_RecursiveDeref(dd,bRes0);
975 Cudd_RecursiveDeref(dd,bRes1);
976 return NULL;
977 }
978 }
979 cuddDeref( bRes0 );
980 cuddDeref( bRes1 );
981
982 cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes );
983 return bRes;
984 }
985 }
986
987
988
989 /**Function*************************************************************
990
991 Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().]
992
993 Description []
994
995 SideEffects []
996
997 SeeAlso []
998
999 ***********************************************************************/
extraBddSpaceCanonVars(DdManager * dd,DdNode * bF)1000 DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF )
1001 {
1002 DdNode * bRes, * bFR;
1003 statLine( dd );
1004
1005 bFR = Cudd_Regular(bF);
1006 if ( cuddIsConstant(bFR) )
1007 return bF;
1008
1009 if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF)) )
1010 return bRes;
1011 else
1012 {
1013 DdNode * bF0, * bF1;
1014 DdNode * bRes, * bRes0;
1015
1016 if ( bFR != bF ) // bF is complemented
1017 {
1018 bF0 = Cudd_Not( cuddE(bFR) );
1019 bF1 = Cudd_Not( cuddT(bFR) );
1020 }
1021 else
1022 {
1023 bF0 = cuddE(bFR);
1024 bF1 = cuddT(bFR);
1025 }
1026
1027 if ( bF0 == b0 )
1028 {
1029 bRes = extraBddSpaceCanonVars( dd, bF1 );
1030 if ( bRes == NULL )
1031 return NULL;
1032 }
1033 else if ( bF1 == b0 )
1034 {
1035 bRes = extraBddSpaceCanonVars( dd, bF0 );
1036 if ( bRes == NULL )
1037 return NULL;
1038 }
1039 else
1040 {
1041 bRes0 = extraBddSpaceCanonVars( dd, bF0 );
1042 if ( bRes0 == NULL )
1043 return NULL;
1044 cuddRef( bRes0 );
1045
1046 bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 );
1047 if ( bRes == NULL )
1048 {
1049 Cudd_RecursiveDeref( dd,bRes0 );
1050 return NULL;
1051 }
1052 cuddDeref( bRes0 );
1053 }
1054
1055 cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes );
1056 return bRes;
1057 }
1058 }
1059
1060 /**Function*************************************************************
1061
1062 Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().]
1063
1064 Description []
1065
1066 SideEffects []
1067
1068 SeeAlso []
1069
1070 ***********************************************************************/
extraBddSpaceEquationsPos(DdManager * dd,DdNode * bF)1071 DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF )
1072 {
1073 DdNode * zRes;
1074 statLine( dd );
1075
1076 if ( bF == b0 )
1077 return z1;
1078 if ( bF == b1 )
1079 return z0;
1080
1081 if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF)) )
1082 return zRes;
1083 else
1084 {
1085 DdNode * bFR, * bF0, * bF1;
1086 DdNode * zPos0, * zPos1, * zNeg1;
1087 DdNode * zRes, * zRes0, * zRes1;
1088
1089 bFR = Cudd_Regular(bF);
1090 if ( bFR != bF ) // bF is complemented
1091 {
1092 bF0 = Cudd_Not( cuddE(bFR) );
1093 bF1 = Cudd_Not( cuddT(bFR) );
1094 }
1095 else
1096 {
1097 bF0 = cuddE(bFR);
1098 bF1 = cuddT(bFR);
1099 }
1100
1101 if ( bF0 == b0 )
1102 {
1103 zRes1 = extraBddSpaceEquationsPos( dd, bF1 );
1104 if ( zRes1 == NULL )
1105 return NULL;
1106 cuddRef( zRes1 );
1107
1108 // add the current element to the set
1109 zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 );
1110 if ( zRes == NULL )
1111 {
1112 Cudd_RecursiveDerefZdd(dd, zRes1);
1113 return NULL;
1114 }
1115 cuddDeref( zRes1 );
1116 }
1117 else if ( bF1 == b0 )
1118 {
1119 zRes = extraBddSpaceEquationsPos( dd, bF0 );
1120 if ( zRes == NULL )
1121 return NULL;
1122 }
1123 else
1124 {
1125 zPos0 = extraBddSpaceEquationsPos( dd, bF0 );
1126 if ( zPos0 == NULL )
1127 return NULL;
1128 cuddRef( zPos0 );
1129
1130 zPos1 = extraBddSpaceEquationsPos( dd, bF1 );
1131 if ( zPos1 == NULL )
1132 {
1133 Cudd_RecursiveDerefZdd(dd, zPos0);
1134 return NULL;
1135 }
1136 cuddRef( zPos1 );
1137
1138 zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 );
1139 if ( zNeg1 == NULL )
1140 {
1141 Cudd_RecursiveDerefZdd(dd, zPos0);
1142 Cudd_RecursiveDerefZdd(dd, zPos1);
1143 return NULL;
1144 }
1145 cuddRef( zNeg1 );
1146
1147
1148 zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
1149 if ( zRes0 == NULL )
1150 {
1151 Cudd_RecursiveDerefZdd(dd, zNeg1);
1152 Cudd_RecursiveDerefZdd(dd, zPos0);
1153 Cudd_RecursiveDerefZdd(dd, zPos1);
1154 return NULL;
1155 }
1156 cuddRef( zRes0 );
1157
1158 zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
1159 if ( zRes1 == NULL )
1160 {
1161 Cudd_RecursiveDerefZdd(dd, zRes0);
1162 Cudd_RecursiveDerefZdd(dd, zNeg1);
1163 Cudd_RecursiveDerefZdd(dd, zPos0);
1164 Cudd_RecursiveDerefZdd(dd, zPos1);
1165 return NULL;
1166 }
1167 cuddRef( zRes1 );
1168 Cudd_RecursiveDerefZdd(dd, zNeg1);
1169 Cudd_RecursiveDerefZdd(dd, zPos0);
1170 Cudd_RecursiveDerefZdd(dd, zPos1);
1171 // only zRes0 and zRes1 are refed at this point
1172
1173 zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
1174 if ( zRes == NULL )
1175 {
1176 Cudd_RecursiveDerefZdd(dd, zRes0);
1177 Cudd_RecursiveDerefZdd(dd, zRes1);
1178 return NULL;
1179 }
1180 cuddDeref( zRes0 );
1181 cuddDeref( zRes1 );
1182 }
1183
1184 cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes );
1185 return zRes;
1186 }
1187 }
1188
1189
1190 /**Function*************************************************************
1191
1192 Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().]
1193
1194 Description []
1195
1196 SideEffects []
1197
1198 SeeAlso []
1199
1200 ***********************************************************************/
extraBddSpaceEquationsNeg(DdManager * dd,DdNode * bF)1201 DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF )
1202 {
1203 DdNode * zRes;
1204 statLine( dd );
1205
1206 if ( bF == b0 )
1207 return z1;
1208 if ( bF == b1 )
1209 return z0;
1210
1211 if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF)) )
1212 return zRes;
1213 else
1214 {
1215 DdNode * bFR, * bF0, * bF1;
1216 DdNode * zPos0, * zPos1, * zNeg1;
1217 DdNode * zRes, * zRes0, * zRes1;
1218
1219 bFR = Cudd_Regular(bF);
1220 if ( bFR != bF ) // bF is complemented
1221 {
1222 bF0 = Cudd_Not( cuddE(bFR) );
1223 bF1 = Cudd_Not( cuddT(bFR) );
1224 }
1225 else
1226 {
1227 bF0 = cuddE(bFR);
1228 bF1 = cuddT(bFR);
1229 }
1230
1231 if ( bF0 == b0 )
1232 {
1233 zRes = extraBddSpaceEquationsNeg( dd, bF1 );
1234 if ( zRes == NULL )
1235 return NULL;
1236 }
1237 else if ( bF1 == b0 )
1238 {
1239 zRes0 = extraBddSpaceEquationsNeg( dd, bF0 );
1240 if ( zRes0 == NULL )
1241 return NULL;
1242 cuddRef( zRes0 );
1243
1244 // add the current element to the set
1245 zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 );
1246 if ( zRes == NULL )
1247 {
1248 Cudd_RecursiveDerefZdd(dd, zRes0);
1249 return NULL;
1250 }
1251 cuddDeref( zRes0 );
1252 }
1253 else
1254 {
1255 zPos0 = extraBddSpaceEquationsNeg( dd, bF0 );
1256 if ( zPos0 == NULL )
1257 return NULL;
1258 cuddRef( zPos0 );
1259
1260 zPos1 = extraBddSpaceEquationsNeg( dd, bF1 );
1261 if ( zPos1 == NULL )
1262 {
1263 Cudd_RecursiveDerefZdd(dd, zPos0);
1264 return NULL;
1265 }
1266 cuddRef( zPos1 );
1267
1268 zNeg1 = extraBddSpaceEquationsPos( dd, bF1 );
1269 if ( zNeg1 == NULL )
1270 {
1271 Cudd_RecursiveDerefZdd(dd, zPos0);
1272 Cudd_RecursiveDerefZdd(dd, zPos1);
1273 return NULL;
1274 }
1275 cuddRef( zNeg1 );
1276
1277
1278 zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
1279 if ( zRes0 == NULL )
1280 {
1281 Cudd_RecursiveDerefZdd(dd, zNeg1);
1282 Cudd_RecursiveDerefZdd(dd, zPos0);
1283 Cudd_RecursiveDerefZdd(dd, zPos1);
1284 return NULL;
1285 }
1286 cuddRef( zRes0 );
1287
1288 zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
1289 if ( zRes1 == NULL )
1290 {
1291 Cudd_RecursiveDerefZdd(dd, zRes0);
1292 Cudd_RecursiveDerefZdd(dd, zNeg1);
1293 Cudd_RecursiveDerefZdd(dd, zPos0);
1294 Cudd_RecursiveDerefZdd(dd, zPos1);
1295 return NULL;
1296 }
1297 cuddRef( zRes1 );
1298 Cudd_RecursiveDerefZdd(dd, zNeg1);
1299 Cudd_RecursiveDerefZdd(dd, zPos0);
1300 Cudd_RecursiveDerefZdd(dd, zPos1);
1301 // only zRes0 and zRes1 are refed at this point
1302
1303 zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
1304 if ( zRes == NULL )
1305 {
1306 Cudd_RecursiveDerefZdd(dd, zRes0);
1307 Cudd_RecursiveDerefZdd(dd, zRes1);
1308 return NULL;
1309 }
1310 cuddDeref( zRes0 );
1311 cuddDeref( zRes1 );
1312 }
1313
1314 cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes );
1315 return zRes;
1316 }
1317 }
1318
1319
1320
1321
1322 /**Function*************************************************************
1323
1324 Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
1325
1326 Description []
1327
1328 SideEffects []
1329
1330 SeeAlso []
1331
1332 ***********************************************************************/
extraBddSpaceFromMatrixPos(DdManager * dd,DdNode * zA)1333 DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
1334 {
1335 DdNode * bRes;
1336 statLine( dd );
1337
1338 if ( zA == z0 )
1339 return b1;
1340 if ( zA == z1 )
1341 return b1;
1342
1343 if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA)) )
1344 return bRes;
1345 else
1346 {
1347 DdNode * bP0, * bP1;
1348 DdNode * bN0, * bN1;
1349 DdNode * bRes0, * bRes1;
1350
1351 bP0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
1352 if ( bP0 == NULL )
1353 return NULL;
1354 cuddRef( bP0 );
1355
1356 bP1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
1357 if ( bP1 == NULL )
1358 {
1359 Cudd_RecursiveDeref( dd, bP0 );
1360 return NULL;
1361 }
1362 cuddRef( bP1 );
1363
1364 bRes0 = cuddBddAndRecur( dd, bP0, bP1 );
1365 if ( bRes0 == NULL )
1366 {
1367 Cudd_RecursiveDeref( dd, bP0 );
1368 Cudd_RecursiveDeref( dd, bP1 );
1369 return NULL;
1370 }
1371 cuddRef( bRes0 );
1372 Cudd_RecursiveDeref( dd, bP0 );
1373 Cudd_RecursiveDeref( dd, bP1 );
1374
1375
1376 bN0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
1377 if ( bN0 == NULL )
1378 {
1379 Cudd_RecursiveDeref( dd, bRes0 );
1380 return NULL;
1381 }
1382 cuddRef( bN0 );
1383
1384 bN1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
1385 if ( bN1 == NULL )
1386 {
1387 Cudd_RecursiveDeref( dd, bRes0 );
1388 Cudd_RecursiveDeref( dd, bN0 );
1389 return NULL;
1390 }
1391 cuddRef( bN1 );
1392
1393 bRes1 = cuddBddAndRecur( dd, bN0, bN1 );
1394 if ( bRes1 == NULL )
1395 {
1396 Cudd_RecursiveDeref( dd, bRes0 );
1397 Cudd_RecursiveDeref( dd, bN0 );
1398 Cudd_RecursiveDeref( dd, bN1 );
1399 return NULL;
1400 }
1401 cuddRef( bRes1 );
1402 Cudd_RecursiveDeref( dd, bN0 );
1403 Cudd_RecursiveDeref( dd, bN1 );
1404
1405
1406 // consider the case when Res0 and Res1 are the same node
1407 if ( bRes0 == bRes1 )
1408 bRes = bRes1;
1409 // consider the case when Res1 is complemented
1410 else if ( Cudd_IsComplement(bRes1) )
1411 {
1412 bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
1413 if ( bRes == NULL )
1414 {
1415 Cudd_RecursiveDeref(dd,bRes0);
1416 Cudd_RecursiveDeref(dd,bRes1);
1417 return NULL;
1418 }
1419 bRes = Cudd_Not(bRes);
1420 }
1421 else
1422 {
1423 bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
1424 if ( bRes == NULL )
1425 {
1426 Cudd_RecursiveDeref(dd,bRes0);
1427 Cudd_RecursiveDeref(dd,bRes1);
1428 return NULL;
1429 }
1430 }
1431 cuddDeref( bRes0 );
1432 cuddDeref( bRes1 );
1433
1434 cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes );
1435 return bRes;
1436 }
1437 }
1438
1439
1440 /**Function*************************************************************
1441
1442 Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
1443
1444 Description []
1445
1446 SideEffects []
1447
1448 SeeAlso []
1449
1450 ***********************************************************************/
extraBddSpaceFromMatrixNeg(DdManager * dd,DdNode * zA)1451 DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
1452 {
1453 DdNode * bRes;
1454 statLine( dd );
1455
1456 if ( zA == z0 )
1457 return b1;
1458 if ( zA == z1 )
1459 return b0;
1460
1461 if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA)) )
1462 return bRes;
1463 else
1464 {
1465 DdNode * bP0, * bP1;
1466 DdNode * bN0, * bN1;
1467 DdNode * bRes0, * bRes1;
1468
1469 bP0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
1470 if ( bP0 == NULL )
1471 return NULL;
1472 cuddRef( bP0 );
1473
1474 bP1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
1475 if ( bP1 == NULL )
1476 {
1477 Cudd_RecursiveDeref( dd, bP0 );
1478 return NULL;
1479 }
1480 cuddRef( bP1 );
1481
1482 bRes0 = cuddBddAndRecur( dd, bP0, bP1 );
1483 if ( bRes0 == NULL )
1484 {
1485 Cudd_RecursiveDeref( dd, bP0 );
1486 Cudd_RecursiveDeref( dd, bP1 );
1487 return NULL;
1488 }
1489 cuddRef( bRes0 );
1490 Cudd_RecursiveDeref( dd, bP0 );
1491 Cudd_RecursiveDeref( dd, bP1 );
1492
1493
1494 bN0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
1495 if ( bN0 == NULL )
1496 {
1497 Cudd_RecursiveDeref( dd, bRes0 );
1498 return NULL;
1499 }
1500 cuddRef( bN0 );
1501
1502 bN1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
1503 if ( bN1 == NULL )
1504 {
1505 Cudd_RecursiveDeref( dd, bRes0 );
1506 Cudd_RecursiveDeref( dd, bN0 );
1507 return NULL;
1508 }
1509 cuddRef( bN1 );
1510
1511 bRes1 = cuddBddAndRecur( dd, bN0, bN1 );
1512 if ( bRes1 == NULL )
1513 {
1514 Cudd_RecursiveDeref( dd, bRes0 );
1515 Cudd_RecursiveDeref( dd, bN0 );
1516 Cudd_RecursiveDeref( dd, bN1 );
1517 return NULL;
1518 }
1519 cuddRef( bRes1 );
1520 Cudd_RecursiveDeref( dd, bN0 );
1521 Cudd_RecursiveDeref( dd, bN1 );
1522
1523
1524 // consider the case when Res0 and Res1 are the same node
1525 if ( bRes0 == bRes1 )
1526 bRes = bRes1;
1527 // consider the case when Res1 is complemented
1528 else if ( Cudd_IsComplement(bRes1) )
1529 {
1530 bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
1531 if ( bRes == NULL )
1532 {
1533 Cudd_RecursiveDeref(dd,bRes0);
1534 Cudd_RecursiveDeref(dd,bRes1);
1535 return NULL;
1536 }
1537 bRes = Cudd_Not(bRes);
1538 }
1539 else
1540 {
1541 bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
1542 if ( bRes == NULL )
1543 {
1544 Cudd_RecursiveDeref(dd,bRes0);
1545 Cudd_RecursiveDeref(dd,bRes1);
1546 return NULL;
1547 }
1548 }
1549 cuddDeref( bRes0 );
1550 cuddDeref( bRes1 );
1551
1552 cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes );
1553 return bRes;
1554 }
1555 }
1556
1557
1558 /*---------------------------------------------------------------------------*/
1559 /* Definition of static functions */
1560 /*---------------------------------------------------------------------------*/
1561
1562 ABC_NAMESPACE_IMPL_END
1563
1564