abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraBddAuto.c
Go to the documentation of this file.
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ******************************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 
memset
char * memset()
extraBddSpaceFromFunctionPos
DdNode * extraBddSpaceFromFunctionPos(DdManager *dd, DdNode *bF)
Definition: extraBddAuto.c:738
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
Extra_bddSpaceEquationsNeg
DdNode * Extra_bddSpaceEquationsNeg(DdManager *dd, DdNode *bSpace)
Definition: extraBddAuto.c:409
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
cuddZddGetNode
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Definition: cuddTable.c:1041
z1
#define z1
Definition: extraBdd.h:78
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Extra_bddSupportNegativeCube
DdNode * Extra_bddSupportNegativeCube(DdManager *dd, DdNode *f)
Definition: extraBddMisc.c:764
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
extraBddSpaceCanonVars
DdNode * extraBddSpaceCanonVars(DdManager *dd, DdNode *bF)
Definition: extraBddAuto.c:1000
Extra_bddSpaceFromFunctionNeg
DdNode * Extra_bddSpaceFromFunctionNeg(DdManager *dd, DdNode *bFunc)
Definition: extraBddAuto.c:295
extraBddSpaceFromMatrixPos
DdNode * extraBddSpaceFromMatrixPos(DdManager *dd, DdNode *zA)
Definition: extraBddAuto.c:1333
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdManager::size
int size
Definition: cuddInt.h:361
b1
#define b1
Definition: extraBdd.h:76
Extra_bddSpaceFromMatrixNeg
DdNode * Extra_bddSpaceFromMatrixNeg(DdManager *dd, DdNode *zA)
Definition: extraBddAuto.c:452
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
Extra_bddSpaceFromFunctionFast
ABC_NAMESPACE_IMPL_START DdNode * Extra_bddSpaceFromFunctionFast(DdManager *dd, DdNode *bFunc)
Definition: extraBddAuto.c:153
extraBddSpaceFromFunction
DdNode * extraBddSpaceFromFunction(DdManager *dd, DdNode *bF, DdNode *bG)
Definition: extraBddAuto.c:562
extraBddSpaceFromMatrixNeg
DdNode * extraBddSpaceFromMatrixNeg(DdManager *dd, DdNode *zA)
Definition: extraBddAuto.c:1451
Extra_bddSpaceFromMatrixPos
DdNode * Extra_bddSpaceFromMatrixPos(DdManager *dd, DdNode *zA)
Definition: extraBddAuto.c:431
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Cudd_zddDiff
DdNode * Cudd_zddDiff(DdManager *dd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:236
Extra_bddSpaceReduce
DdNode * Extra_bddSpaceReduce(DdManager *dd, DdNode *bFunc, DdNode *bCanonVars)
Definition: extraBddAuto.c:337
extraBddSpaceFromFunctionNeg
DdNode * extraBddSpaceFromFunctionNeg(DdManager *dd, DdNode *bF)
Definition: extraBddAuto.c:869
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
Cudd_bddVectorCompose
DdNode * Cudd_bddVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:791
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
Cudd_zddUnion
DdNode * Cudd_zddUnion(DdManager *dd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:178
Extra_bddSpaceFromFunction
DdNode * Extra_bddSpaceFromFunction(DdManager *dd, DdNode *bF, DdNode *bG)
Definition: extraBddAuto.c:253
DdManager::reordered
int reordered
Definition: cuddInt.h:409
Extra_zddLitCountComb
int Extra_zddLitCountComb(DdManager *dd, DdNode *zComb)
Definition: extraBddAuto.c:473
z0
#define z0
Definition: extraBdd.h:77
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
Cudd_Cofactor
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:556
Cudd_bddPermute
DdNode * Cudd_bddPermute(DdManager *manager, DdNode *node, int *permut)
Definition: cuddCompose.c:332
cuddZddIntersect
DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:642
Extra_zddSelectOneSubset
DdNode * Extra_zddSelectOneSubset(DdManager *dd, DdNode *zS)
Definition: extraBddSymm.c:546
Extra_bddSpaceEquations
DdNode * Extra_bddSpaceEquations(DdManager *dd, DdNode *bSpace)
Definition: extraBddAuto.c:361
Extra_SupportArray
int * Extra_SupportArray(DdManager *dd, DdNode *F, int *support)
Definition: extraBddMisc.c:537
Extra_bddSpaceExorGates
DdNode ** Extra_bddSpaceExorGates(DdManager *dd, DdNode *bFuncRed, DdNode *zEquations)
Definition: extraBddAuto.c:497
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
ddMax
#define ddMax(x, y)
Definition: cuddInt.h:832
Cudd_bddXorExistAbstract
DdNode * Cudd_bddXorExistAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddBddAbs.c:169
Counter
static int Counter
Definition: extraBddMisc.c:1877
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
extraBddSpaceEquationsNeg
DdNode * extraBddSpaceEquationsNeg(DdManager *dd, DdNode *bF)
Definition: extraBddAuto.c:1201
extraBddSpaceEquationsPos
DdNode * extraBddSpaceEquationsPos(DdManager *dd, DdNode *bF)
Definition: extraBddAuto.c:1071
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Extra_bddSpaceFromFunctionPos
DdNode * Extra_bddSpaceFromFunctionPos(DdManager *dd, DdNode *bFunc)
Definition: extraBddAuto.c:274
b0
#define b0
Definition: extraBdd.h:75
DdManager::sizeZ
int sizeZ
Definition: cuddInt.h:362
DdNode::index
DdHalfWord index
Definition: cudd.h:279
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
Cudd_bddXor
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:476
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Extra_bddSpaceCanonVars
DdNode * Extra_bddSpaceCanonVars(DdManager *dd, DdNode *bSpace)
Definition: extraBddAuto.c:316
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Extra_bddSpaceEquationsPos
DdNode * Extra_bddSpaceEquationsPos(DdManager *dd, DdNode *bSpace)
Definition: extraBddAuto.c:387
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
DdManager::perm
int * perm
Definition: cuddInt.h:386
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
cuddCacheLookup1Zdd
DdNode * cuddCacheLookup1Zdd(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:664
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323