ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraBddAuto.c
Go to the documentation of this file.
1
18
19#include "extraBdd.h"
20
21ABC_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
46
47/*---------------------------------------------------------------------------*/
48/* Static function prototypes */
49/*---------------------------------------------------------------------------*/
50
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
153DdNode * 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
253DdNode * 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
274DdNode * 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
295DdNode * 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
316DdNode * 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
337DdNode * 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
361DdNode * 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
387DdNode * 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
409DdNode * 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
431DdNode * 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
452DdNode * 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
473int 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
497DdNode ** 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
562DdNode * 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
738DdNode * 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
869DdNode * 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
1000DdNode * 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
1071DdNode * 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
1201DdNode * 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
1333DdNode * 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
1451DdNode * 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
1562ABC_NAMESPACE_IMPL_END
1563
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
b0
#define b0
Definition bbrImage.c:96
b1
#define b1
Definition bbrImage.c:97
extraBddSpaceEquationsPos
DdNode * extraBddSpaceEquationsPos(DdManager *dd, DdNode *bF)
Definition extraBddAuto.c:1071
Extra_bddSpaceEquationsPos
DdNode * Extra_bddSpaceEquationsPos(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:387
Extra_bddSpaceFromFunction
DdNode * Extra_bddSpaceFromFunction(DdManager *dd, DdNode *bF, DdNode *bG)
Definition extraBddAuto.c:253
extraBddSpaceFromMatrixPos
DdNode * extraBddSpaceFromMatrixPos(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:1333
Extra_bddSpaceFromMatrixPos
DdNode * Extra_bddSpaceFromMatrixPos(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:431
extraBddSpaceFromFunctionNeg
DdNode * extraBddSpaceFromFunctionNeg(DdManager *dd, DdNode *bF)
Definition extraBddAuto.c:869
Extra_zddLitCountComb
int Extra_zddLitCountComb(DdManager *dd, DdNode *zComb)
Definition extraBddAuto.c:473
extraBddSpaceEquationsNeg
DdNode * extraBddSpaceEquationsNeg(DdManager *dd, DdNode *bF)
Definition extraBddAuto.c:1201
extraBddSpaceCanonVars
DdNode * extraBddSpaceCanonVars(DdManager *dd, DdNode *bF)
Definition extraBddAuto.c:1000
Extra_bddSpaceCanonVars
DdNode * Extra_bddSpaceCanonVars(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:316
Extra_bddSpaceFromFunctionNeg
DdNode * Extra_bddSpaceFromFunctionNeg(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:295
Extra_bddSpaceExorGates
DdNode ** Extra_bddSpaceExorGates(DdManager *dd, DdNode *bFuncRed, DdNode *zEquations)
Definition extraBddAuto.c:497
Extra_bddSpaceFromMatrixNeg
DdNode * Extra_bddSpaceFromMatrixNeg(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:452
extraBddSpaceFromMatrixNeg
DdNode * extraBddSpaceFromMatrixNeg(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:1451
Extra_bddSpaceFromFunctionPos
DdNode * Extra_bddSpaceFromFunctionPos(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:274
extraBddSpaceFromFunctionPos
DdNode * extraBddSpaceFromFunctionPos(DdManager *dd, DdNode *bF)
Definition extraBddAuto.c:738
Extra_bddSpaceEquations
DdNode * Extra_bddSpaceEquations(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:361
extraBddSpaceFromFunction
DdNode * extraBddSpaceFromFunction(DdManager *dd, DdNode *bF, DdNode *bG)
Definition extraBddAuto.c:562
Extra_bddSpaceFromFunctionFast
ABC_NAMESPACE_IMPL_START DdNode * Extra_bddSpaceFromFunctionFast(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:153
Extra_bddSpaceReduce
DdNode * Extra_bddSpaceReduce(DdManager *dd, DdNode *bFunc, DdNode *bCanonVars)
Definition extraBddAuto.c:337
Extra_bddSpaceEquationsNeg
DdNode * Extra_bddSpaceEquationsNeg(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:409
extraBddSpaceFromMatrixPos
DdNode * extraBddSpaceFromMatrixPos(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:1333
extraBddSpaceEquationsPos
DdNode * extraBddSpaceEquationsPos(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:1071
z0
#define z0
Definition extraBdd.h:77
extraBddSpaceCanonVars
DdNode * extraBddSpaceCanonVars(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:1000
Extra_bddSupportNegativeCube
DdNode * Extra_bddSupportNegativeCube(DdManager *dd, DdNode *f)
Definition extraBddMisc.c:764
extraBddSpaceFromMatrixNeg
DdNode * extraBddSpaceFromMatrixNeg(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:1451
z1
#define z1
Definition extraBdd.h:78
extraBddSpaceFromFunctionPos
DdNode * extraBddSpaceFromFunctionPos(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:738
extraBddSpaceFromFunction
DdNode * extraBddSpaceFromFunction(DdManager *dd, DdNode *bF, DdNode *bG)
Definition extraBddAuto.c:562
extraBddSpaceFromFunctionNeg
DdNode * extraBddSpaceFromFunctionNeg(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:869
extraBddSpaceEquationsNeg
DdNode * extraBddSpaceEquationsNeg(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:1201
Extra_zddSelectOneSubset
DdNode * Extra_zddSelectOneSubset(DdManager *dd, DdNode *zS)
Definition extraBddSymm.c:546
Extra_SupportArray
int * Extra_SupportArray(DdManager *dd, DdNode *F, int *support)
Definition extraBddMisc.c:537
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()