abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraBddUnate.c File Reference
#include "extraBdd.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Extra_UnateInfo_t
Extra_UnateComputeFast (DdManager *dd, DdNode *bFunc)
 
DdNodeExtra_zddUnateInfoCompute (DdManager *dd, DdNode *bF, DdNode *bVars)
 
DdNodeExtra_zddGetSingletonsBoth (DdManager *dd, DdNode *bVars)
 
Extra_UnateInfo_tExtra_UnateInfoAllocate (int nVars)
 
void Extra_UnateInfoDissolve (Extra_UnateInfo_t *p)
 
void Extra_UnateInfoPrint (Extra_UnateInfo_t *p)
 
Extra_UnateInfo_tExtra_UnateInfoCreateFromZdd (DdManager *dd, DdNode *zPairs, DdNode *bSupp)
 
Extra_UnateInfo_tExtra_UnateComputeSlow (DdManager *dd, DdNode *bFunc)
 
int Extra_bddCheckUnateNaive (DdManager *dd, DdNode *bF, int iVar)
 
DdNodeextraZddUnateInfoCompute (DdManager *dd, DdNode *bFunc, DdNode *bVars)
 
DdNodeextraZddGetSingletonsBoth (DdManager *dd, DdNode *bVars)
 

Function Documentation

int Extra_bddCheckUnateNaive ( DdManager dd,
DdNode bF,
int  iVar 
)

Function********************************************************************

Synopsis [Checks if the two variables are symmetric.]

Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.]

SideEffects []

SeeAlso []

Definition at line 338 of file extraBddUnate.c.

342 {
343  DdNode * bCof0, * bCof1;
344  int Res;
345 
346  assert( iVar < dd->size );
347 
348  bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) ); Cudd_Ref( bCof0 );
349  bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) ); Cudd_Ref( bCof1 );
350 
351  if ( Cudd_bddLeq( dd, bCof0, bCof1 ) )
352  Res = 1;
353  else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) )
354  Res =-1;
355  else
356  Res = 0;
357 
358  Cudd_RecursiveDeref( dd, bCof0 );
359  Cudd_RecursiveDeref( dd, bCof1 );
360  return Res;
361 } /* end of Extra_bddCheckUnateNaive */
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
static int size
Definition: cuddSign.c:86
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
#define assert(ex)
Definition: util_old.h:213
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
ABC_NAMESPACE_IMPL_START Extra_UnateInfo_t* Extra_UnateComputeFast ( DdManager dd,
DdNode bFunc 
)

CFile****************************************************************

FileName [extraBddUnate.c]

PackageName [extra]

Synopsis [Efficient methods to compute the information about unate variables using an algorithm that is conceptually similar to the algorithm for two-variable symmetry computation presented in: A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. Transactions on CAD, Nov. 2003.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - September 1, 2003.]

Revision [

Id:
extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp

]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Computes the classical symmetry information for the function.]

Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.]

SideEffects [If the ZDD variables are not derived from BDD variables with multiplicity 2, this function may derive them in a wrong way.]

SeeAlso []

Definition at line 73 of file extraBddUnate.c.

76 {
77  DdNode * bSupp;
78  DdNode * zRes;
80 
81  bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp );
82  zRes = Extra_zddUnateInfoCompute( dd, bFunc, bSupp ); Cudd_Ref( zRes );
83 
84  p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp );
85 
86  Cudd_RecursiveDeref( dd, bSupp );
87  Cudd_RecursiveDerefZdd( dd, zRes );
88 
89  return p;
90 
91 } /* end of Extra_UnateInfoCompute */
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
static Llb_Mgr_t * p
Definition: llb3Image.c:950
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
DdNode * Extra_zddUnateInfoCompute(DdManager *dd, DdNode *bF, DdNode *bVars)
Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd(DdManager *dd, DdNode *zPairs, DdNode *bSupp)
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Extra_UnateInfo_t* Extra_UnateComputeSlow ( DdManager dd,
DdNode bFunc 
)

Function********************************************************************

Synopsis [Computes the classical unateness information for the function.]

Description [Uses the naive way of comparing cofactors.]

SideEffects []

SeeAlso []

Definition at line 293 of file extraBddUnate.c.

294 {
295  int nSuppSize;
296  DdNode * bSupp, * bTemp;
298  int i, Res;
299 
300  // compute the support
301  bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp );
302  nSuppSize = Extra_bddSuppSize( dd, bSupp );
303 //printf( "Support = %d. ", nSuppSize );
304 //Extra_bddPrint( dd, bSupp );
305 //printf( "%d ", nSuppSize );
306 
307  // allocate the storage for symmetry info
308  p = Extra_UnateInfoAllocate( nSuppSize );
309 
310  // assign the variables
311  p->nVarsMax = dd->size;
312  for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
313  {
314  Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index );
315  p->pVars[i].iVar = bTemp->index;
316  if ( Res == -1 )
317  p->pVars[i].Neg = 1;
318  else if ( Res == 1 )
319  p->pVars[i].Pos = 1;
320  p->nUnate += (Res != 0);
321  }
322  Cudd_RecursiveDeref( dd, bSupp );
323  return p;
324 
325 } /* end of Extra_UnateComputeSlow */
int Extra_bddSuppSize(DdManager *dd, DdNode *bSupp)
Definition: extraBddMisc.c:321
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
static Llb_Mgr_t * p
Definition: llb3Image.c:950
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
int size
Definition: cuddInt.h:361
#define b1
Definition: extraBdd.h:76
unsigned iVar
Definition: extraBdd.h:271
Extra_UnateInfo_t * Extra_UnateInfoAllocate(int nVars)
#define cuddT(node)
Definition: cuddInt.h:636
unsigned Neg
Definition: extraBdd.h:273
DdHalfWord index
Definition: cudd.h:279
Extra_UnateVar_t * pVars
Definition: extraBdd.h:281
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
int Extra_bddCheckUnateNaive(DdManager *dd, DdNode *bF, int iVar)
unsigned Pos
Definition: extraBdd.h:272
Extra_UnateInfo_t* Extra_UnateInfoAllocate ( int  nVars)

Function********************************************************************

Synopsis [Allocates unateness information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file extraBddUnate.c.

156 {
158  // allocate and clean the storage for unateness info
159  p = ABC_ALLOC( Extra_UnateInfo_t, 1 );
160  memset( p, 0, sizeof(Extra_UnateInfo_t) );
161  p->nVars = nVars;
162  p->pVars = ABC_ALLOC( Extra_UnateVar_t, nVars );
163  memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) );
164  return p;
165 } /* end of Extra_UnateInfoAllocate */
char * memset()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Extra_UnateVar_t * pVars
Definition: extraBdd.h:281
Extra_UnateInfo_t* Extra_UnateInfoCreateFromZdd ( DdManager dd,
DdNode zPairs,
DdNode bSupp 
)

Function********************************************************************

Synopsis [Creates the symmetry information structure from ZDD.]

Description [ZDD representation of symmetries is the set of cubes, each of which has two variables in the positive polarity. These variables correspond to the symmetric variable pair.]

SideEffects []

SeeAlso []

Definition at line 227 of file extraBddUnate.c.

228 {
230  DdNode * bTemp, * zSet, * zCube, * zTemp;
231  int * pMapVars2Nums;
232  int i, nSuppSize;
233 
234  nSuppSize = Extra_bddSuppSize( dd, bSupp );
235 
236  // allocate and clean the storage for symmetry info
237  p = Extra_UnateInfoAllocate( nSuppSize );
238 
239  // allocate the storage for the temporary map
240  pMapVars2Nums = ABC_ALLOC( int, dd->size );
241  memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
242 
243  // assign the variables
244  p->nVarsMax = dd->size;
245  for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
246  {
247  p->pVars[i].iVar = bTemp->index;
248  pMapVars2Nums[bTemp->index] = i;
249  }
250 
251  // write the symmetry info into the structure
252  zSet = zPairs; Cudd_Ref( zSet );
253 // Cudd_zddPrintCover( dd, zPairs ); printf( "\n" );
254  while ( zSet != z0 )
255  {
256  // get the next cube
257  zCube = Extra_zddSelectOneSubset( dd, zSet ); Cudd_Ref( zCube );
258 
259  // add this var to the data structure
260  assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 );
261  if ( zCube->index & 1 ) // neg
262  p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1;
263  else
264  p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1;
265  // count the unate vars
266  p->nUnate++;
267 
268  // update the cuver and deref the cube
269  zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube ); Cudd_Ref( zSet );
270  Cudd_RecursiveDerefZdd( dd, zTemp );
271  Cudd_RecursiveDerefZdd( dd, zCube );
272 
273  } // for each cube
274  Cudd_RecursiveDerefZdd( dd, zSet );
275  ABC_FREE( pMapVars2Nums );
276  return p;
277 
278 } /* end of Extra_UnateInfoCreateFromZdd */
char * memset()
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
int Extra_bddSuppSize(DdManager *dd, DdNode *bSupp)
Definition: extraBddMisc.c:321
Definition: cudd.h:278
#define z1
Definition: extraBdd.h:78
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int size
Definition: cuddInt.h:361
#define b1
Definition: extraBdd.h:76
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdNode * Cudd_zddDiff(DdManager *dd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:236
unsigned iVar
Definition: extraBdd.h:271
Extra_UnateInfo_t * Extra_UnateInfoAllocate(int nVars)
#define z0
Definition: extraBdd.h:77
DdNode * Extra_zddSelectOneSubset(DdManager *dd, DdNode *zS)
Definition: extraBddSymm.c:546
#define cuddT(node)
Definition: cuddInt.h:636
unsigned Neg
Definition: extraBdd.h:273
DdHalfWord index
Definition: cudd.h:279
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define cuddE(node)
Definition: cuddInt.h:652
Extra_UnateVar_t * pVars
Definition: extraBdd.h:281
#define assert(ex)
Definition: util_old.h:213
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
unsigned Pos
Definition: extraBdd.h:272
void Extra_UnateInfoDissolve ( Extra_UnateInfo_t p)

Function********************************************************************

Synopsis [Deallocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file extraBddUnate.c.

179 {
180  ABC_FREE( p->pVars );
181  ABC_FREE( p );
182 } /* end of Extra_UnateInfoDissolve */
#define ABC_FREE(obj)
Definition: abc_global.h:232
Extra_UnateVar_t * pVars
Definition: extraBdd.h:281
void Extra_UnateInfoPrint ( Extra_UnateInfo_t p)

Function********************************************************************

Synopsis [Allocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file extraBddUnate.c.

196 {
197  char * pBuffer;
198  int i;
199  pBuffer = ABC_ALLOC( char, p->nVarsMax+1 );
200  memset( pBuffer, ' ', p->nVarsMax );
201  pBuffer[p->nVarsMax] = 0;
202  for ( i = 0; i < p->nVars; i++ )
203  if ( p->pVars[i].Neg )
204  pBuffer[ p->pVars[i].iVar ] = 'n';
205  else if ( p->pVars[i].Pos )
206  pBuffer[ p->pVars[i].iVar ] = 'p';
207  else
208  pBuffer[ p->pVars[i].iVar ] = '.';
209  printf( "%s\n", pBuffer );
210  ABC_FREE( pBuffer );
211 } /* end of Extra_UnateInfoPrint */
char * memset()
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
unsigned iVar
Definition: extraBdd.h:271
unsigned Neg
Definition: extraBdd.h:273
#define ABC_FREE(obj)
Definition: abc_global.h:232
Extra_UnateVar_t * pVars
Definition: extraBdd.h:281
unsigned Pos
Definition: extraBdd.h:272
DdNode* Extra_zddGetSingletonsBoth ( DdManager dd,
DdNode bVars 
)

Function********************************************************************

Synopsis [Converts a set of variables into a set of singleton subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file extraBddUnate.c.

134 {
135  DdNode * res;
136  do {
137  dd->reordered = 0;
138  res = extraZddGetSingletonsBoth( dd, bVars );
139  } while (dd->reordered == 1);
140  return(res);
141 
142 } /* end of Extra_zddGetSingletonsBoth */
Definition: cudd.h:278
int reordered
Definition: cuddInt.h:409
DdNode * extraZddGetSingletonsBoth(DdManager *dd, DdNode *bVars)
DdNode* Extra_zddUnateInfoCompute ( DdManager dd,
DdNode bF,
DdNode bVars 
)

Function********************************************************************

Synopsis [Computes the classical symmetry information as a ZDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file extraBddUnate.c.

109 {
110  DdNode * res;
111  do {
112  dd->reordered = 0;
113  res = extraZddUnateInfoCompute( dd, bF, bVars );
114  } while (dd->reordered == 1);
115  return(res);
116 
117 } /* end of Extra_zddUnateInfoCompute */
Definition: cudd.h:278
DdNode * extraZddUnateInfoCompute(DdManager *dd, DdNode *bFunc, DdNode *bVars)
int reordered
Definition: cuddInt.h:409
DdNode* extraZddGetSingletonsBoth ( DdManager dd,
DdNode bVars 
)

Function********************************************************************

Synopsis [Performs a recursive step of Extra_zddGetSingletons.]

Description [Returns the set of ZDD singletons, containing those pos/neg polarity ZDD variables that correspond to the BDD variables in bVars.]

SideEffects []

SeeAlso []

Definition at line 570 of file extraBddUnate.c.

573 {
574  DdNode * zRes;
575 
576  if ( bVars == b1 )
577  return z1;
578 
579  if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars)) )
580  return zRes;
581  else
582  {
583  DdNode * zTemp, * zPlus;
584 
585  // solve subproblem
586  zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) );
587  if ( zRes == NULL )
588  return NULL;
589  cuddRef( zRes );
590 
591 
592  // create the negative singleton
593  zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 );
594  if ( zPlus == NULL )
595  {
596  Cudd_RecursiveDerefZdd( dd, zRes );
597  return NULL;
598  }
599  cuddRef( zPlus );
600 
601  // add these to the result
602  zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
603  if ( zRes == NULL )
604  {
605  Cudd_RecursiveDerefZdd( dd, zTemp );
606  Cudd_RecursiveDerefZdd( dd, zPlus );
607  return NULL;
608  }
609  cuddRef( zRes );
610  Cudd_RecursiveDerefZdd( dd, zTemp );
611  Cudd_RecursiveDerefZdd( dd, zPlus );
612 
613 
614  // create the positive singleton
615  zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
616  if ( zPlus == NULL )
617  {
618  Cudd_RecursiveDerefZdd( dd, zRes );
619  return NULL;
620  }
621  cuddRef( zPlus );
622 
623  // add these to the result
624  zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
625  if ( zRes == NULL )
626  {
627  Cudd_RecursiveDerefZdd( dd, zTemp );
628  Cudd_RecursiveDerefZdd( dd, zPlus );
629  return NULL;
630  }
631  cuddRef( zRes );
632  Cudd_RecursiveDerefZdd( dd, zTemp );
633  Cudd_RecursiveDerefZdd( dd, zPlus );
634 
635  cuddDeref( zRes );
636  cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes );
637  return zRes;
638  }
639 } /* end of extraZddGetSingletonsBoth */
#define cuddRef(n)
Definition: cuddInt.h:584
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
#define cuddDeref(n)
Definition: cuddInt.h:604
Definition: cudd.h:278
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Definition: cuddTable.c:1041
#define z1
Definition: extraBdd.h:78
#define b1
Definition: extraBdd.h:76
#define z0
Definition: extraBdd.h:77
#define cuddT(node)
Definition: cuddInt.h:636
DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:553
DdHalfWord index
Definition: cudd.h:279
DdNode * extraZddGetSingletonsBoth(DdManager *dd, DdNode *bVars)
DdNode * cuddCacheLookup1Zdd(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:664
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323
DdNode* extraZddUnateInfoCompute ( DdManager dd,
DdNode bFunc,
DdNode bVars 
)

Function********************************************************************

Synopsis [Performs a recursive step of Extra_UnateInfoCompute.]

Description [Returns the set of symmetric variable pairs represented as a set of two-literal ZDD cubes. Both variables always appear in the positive polarity in the cubes. This function works without building new BDD nodes. Some relatively small number of ZDD nodes may be built to ensure proper bookkeeping of the symmetry information.]

SideEffects []

SeeAlso []

Definition at line 385 of file extraBddUnate.c.

389 {
390  DdNode * zRes;
391  DdNode * bFR = Cudd_Regular(bFunc);
392 
393  if ( cuddIsConstant(bFR) )
394  {
395  if ( cuddIsConstant(bVars) )
396  return z0;
397  return extraZddGetSingletonsBoth( dd, bVars );
398  }
399  assert( bVars != b1 );
400 
401  if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars)) )
402  return zRes;
403  else
404  {
405  DdNode * zRes0, * zRes1;
406  DdNode * zTemp, * zPlus;
407  DdNode * bF0, * bF1;
408  DdNode * bVarsNew;
409  int nVarsExtra;
410  int LevelF;
411  int AddVar;
412 
413  // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
414  // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
415  // count how many extra vars are there in bVars
416  nVarsExtra = 0;
417  LevelF = dd->perm[bFR->index];
418  for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
419  nVarsExtra++;
420  // the indexes (level) of variables should be synchronized now
421  assert( bFR->index == bVarsNew->index );
422 
423  // cofactor the function
424  if ( bFR != bFunc ) // bFunc is complemented
425  {
426  bF0 = Cudd_Not( cuddE(bFR) );
427  bF1 = Cudd_Not( cuddT(bFR) );
428  }
429  else
430  {
431  bF0 = cuddE(bFR);
432  bF1 = cuddT(bFR);
433  }
434 
435  // solve subproblems
436  zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) );
437  if ( zRes0 == NULL )
438  return NULL;
439  cuddRef( zRes0 );
440 
441  // if there is no symmetries in the negative cofactor
442  // there is no need to test the positive cofactor
443  if ( zRes0 == z0 )
444  zRes = zRes0; // zRes takes reference
445  else
446  {
447  zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) );
448  if ( zRes1 == NULL )
449  {
450  Cudd_RecursiveDerefZdd( dd, zRes0 );
451  return NULL;
452  }
453  cuddRef( zRes1 );
454 
455  // only those variables are pair-wise symmetric
456  // that are pair-wise symmetric in both cofactors
457  // therefore, intersect the solutions
458  zRes = cuddZddIntersect( dd, zRes0, zRes1 );
459  if ( zRes == NULL )
460  {
461  Cudd_RecursiveDerefZdd( dd, zRes0 );
462  Cudd_RecursiveDerefZdd( dd, zRes1 );
463  return NULL;
464  }
465  cuddRef( zRes );
466  Cudd_RecursiveDerefZdd( dd, zRes0 );
467  Cudd_RecursiveDerefZdd( dd, zRes1 );
468  }
469 
470  // consider the current top-most variable
471  AddVar = -1;
472  if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos
473  AddVar = 0;
474  else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg
475  AddVar = 1;
476  if ( AddVar >= 0 )
477  {
478  // create the singleton
479  zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 );
480  if ( zPlus == NULL )
481  {
482  Cudd_RecursiveDerefZdd( dd, zRes );
483  return NULL;
484  }
485  cuddRef( zPlus );
486 
487  // add these to the result
488  zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
489  if ( zRes == NULL )
490  {
491  Cudd_RecursiveDerefZdd( dd, zTemp );
492  Cudd_RecursiveDerefZdd( dd, zPlus );
493  return NULL;
494  }
495  cuddRef( zRes );
496  Cudd_RecursiveDerefZdd( dd, zTemp );
497  Cudd_RecursiveDerefZdd( dd, zPlus );
498  }
499  // only zRes is referenced at this point
500 
501  // if we skipped some variables, these variables cannot be symmetric with
502  // any variables that are currently in the support of bF, but they can be
503  // symmetric with the variables that are in bVars but not in the support of bF
504  for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
505  {
506  // create the negative singleton
507  zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 );
508  if ( zPlus == NULL )
509  {
510  Cudd_RecursiveDerefZdd( dd, zRes );
511  return NULL;
512  }
513  cuddRef( zPlus );
514 
515  // add these to the result
516  zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
517  if ( zRes == NULL )
518  {
519  Cudd_RecursiveDerefZdd( dd, zTemp );
520  Cudd_RecursiveDerefZdd( dd, zPlus );
521  return NULL;
522  }
523  cuddRef( zRes );
524  Cudd_RecursiveDerefZdd( dd, zTemp );
525  Cudd_RecursiveDerefZdd( dd, zPlus );
526 
527 
528  // create the positive singleton
529  zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
530  if ( zPlus == NULL )
531  {
532  Cudd_RecursiveDerefZdd( dd, zRes );
533  return NULL;
534  }
535  cuddRef( zPlus );
536 
537  // add these to the result
538  zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
539  if ( zRes == NULL )
540  {
541  Cudd_RecursiveDerefZdd( dd, zTemp );
542  Cudd_RecursiveDerefZdd( dd, zPlus );
543  return NULL;
544  }
545  cuddRef( zRes );
546  Cudd_RecursiveDerefZdd( dd, zTemp );
547  Cudd_RecursiveDerefZdd( dd, zPlus );
548  }
549  cuddDeref( zRes );
550 
551  /* insert the result into cache */
552  cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes);
553  return zRes;
554  }
555 } /* end of extraZddUnateInfoCompute */
DdNode * cuddCacheLookup2Zdd(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:610
#define cuddRef(n)
Definition: cuddInt.h:584
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
#define cuddDeref(n)
Definition: cuddInt.h:604
Definition: cudd.h:278
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Definition: cuddTable.c:1041
#define z1
Definition: extraBdd.h:78
#define Cudd_Not(node)
Definition: cudd.h:367
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
#define b1
Definition: extraBdd.h:76
#define Cudd_Regular(node)
Definition: cudd.h:397
DdNode * extraZddUnateInfoCompute(DdManager *dd, DdNode *bFunc, DdNode *bVars)
#define z0
Definition: extraBdd.h:77
DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:642
#define cuddIsConstant(node)
Definition: cuddInt.h:620
#define cuddT(node)
Definition: cuddInt.h:636
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:553
DdHalfWord index
Definition: cudd.h:279
#define cuddE(node)
Definition: cuddInt.h:652
#define assert(ex)
Definition: util_old.h:213
DdNode * extraZddGetSingletonsBoth(DdManager *dd, DdNode *bVars)
int * perm
Definition: cuddInt.h:386