text: /**CFile****************************************************************
  
    FileName    [extraBddSymm.c]
  
    PackageName [extra]
  
    Synopsis    [Efficient methods to compute the information about
    symmetric variables using the algorithm presented in the paper:
    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: extraBddSymm.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  #include "extra.h"
  
  /*---------------------------------------------------------------------------*/
  /* Constant declarations                                                     */
  /*---------------------------------------------------------------------------*/
  
  /*---------------------------------------------------------------------------*/
  /* Stucture declarations                                                     */
  /*---------------------------------------------------------------------------*/
  
  /*---------------------------------------------------------------------------*/
  /* Type declarations                                                         */
  /*---------------------------------------------------------------------------*/
  
  /*---------------------------------------------------------------------------*/
  /* Variable declarations                                                     */
  /*---------------------------------------------------------------------------*/
  
  /*---------------------------------------------------------------------------*/
  /* Macro declarations                                                        */
  /*---------------------------------------------------------------------------*/
  
  #define DD_GET_SYMM_VARS_TAG          0x0a /* former DD_BDD_XOR_EXIST_ABSTRACT_TAG */
  
  /**AutomaticStart*************************************************************/
  
  /*---------------------------------------------------------------------------*/
  /* Static function prototypes                                                */
  /*---------------------------------------------------------------------------*/
  
  /**AutomaticEnd***************************************************************/
  
  /*---------------------------------------------------------------------------*/
  /* Definition of exported functions                                          */
  /*---------------------------------------------------------------------------*/
  
  /**Function********************************************************************
  
    Synopsis    [Computes the classical symmetry information for the function.]
  
    Description [Returns the symmetry information in the form of Extra_SymmInfo_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     []
  
  ******************************************************************************/
  Extra_SymmInfo_t * Extra_SymmPairsCompute( 
    DdManager * dd,   /* the manager */
    DdNode * bFunc)   /* the function whose symmetries are computed */
  {
      DdNode * bSupp;
      DdNode * zRes;
      Extra_SymmInfo_t * p;
  
      bSupp = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSupp );
      zRes  = Extra_zddSymmPairsCompute( dd, bFunc, bSupp );  Cudd_Ref( zRes );
  
      p = Extra_SymmPairsCreateFromZdd( dd, zRes, bSupp );
  
      Cudd_RecursiveDeref( dd, bSupp );
      Cudd_RecursiveDerefZdd( dd, zRes );
  
      return p;
  
  } /* end of Extra_SymmPairsCompute */
  
  
  /**Function********************************************************************
  
    Synopsis    [Computes the classical symmetry information as a ZDD.]
  
    Description []
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * Extra_zddSymmPairsCompute( 
    DdManager * dd,   /* the DD manager */
    DdNode * bF,
    DdNode * bVars) 
  {
      DdNode * res;
      do {
          dd->reordered = 0;
          res = extraZddSymmPairsCompute( dd, bF, bVars );
      } while (dd->reordered == 1);
      return(res);
  
  } /* end of Extra_zddSymmPairsCompute */
  
  /**Function********************************************************************
  
    Synopsis    [Returns a singleton-set ZDD containing all variables that are symmetric with the given one.]
  
    Description []
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * Extra_zddGetSymmetricVars( 
    DdManager * dd,    /* the DD manager */
    DdNode * bF,       /* the first function  - originally, the positive cofactor */
    DdNode * bG,       /* the second fucntion - originally, the negative cofactor */
    DdNode * bVars)    /* the set of variables, on which F and G depend */
  {
      DdNode * res;
      do {
          dd->reordered = 0;
          res = extraZddGetSymmetricVars( dd, bF, bG, bVars );
      } while (dd->reordered == 1);
      return(res);
  
  } /* end of Extra_zddGetSymmetricVars */
  
  
  /**Function********************************************************************
  
    Synopsis    [Converts a set of variables into a set of singleton subsets.]
  
    Description []
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * Extra_zddGetSingletons( 
    DdManager * dd,    /* the DD manager */
    DdNode * bVars)    /* the set of variables */
  {
      DdNode * res;
      do {
          dd->reordered = 0;
          res = extraZddGetSingletons( dd, bVars );
      } while (dd->reordered == 1);
      return(res);
  
  } /* end of Extra_zddGetSingletons */
  
  /**Function********************************************************************
  
    Synopsis    [Filters the set of variables using the support of the function.]
  
    Description []
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * Extra_bddReduceVarSet( 
    DdManager * dd,    /* the DD manager */
    DdNode * bVars,    /* the set of variables to be reduced */
    DdNode * bF)       /* the function whose support is used for reduction */
  {
      DdNode * res;
      do {
          dd->reordered = 0;
          res = extraBddReduceVarSet( dd, bVars, bF );
      } while (dd->reordered == 1);
      return(res);
  
  } /* end of Extra_bddReduceVarSet */
  
  
  /**Function********************************************************************
  
    Synopsis    [Allocates symmetry information structure.]
  
    Description []
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
  {
      int i;
      Extra_SymmInfo_t * p;
  
      // allocate and clean the storage for symmetry info
      p = ALLOC( Extra_SymmInfo_t, 1 );
      memset( p, 0, sizeof(Extra_SymmInfo_t) );
      p->nVars     = nVars;
      p->pVars     = ALLOC( int, nVars );  
      p->pSymms    = ALLOC( char *, nVars );  
      p->pSymms[0] = ALLOC( char  , nVars * nVars );
      memset( p->pSymms[0], 0, nVars * nVars * sizeof(char) );
  
      for ( i = 1; i < nVars; i++ )
          p->pSymms[i] = p->pSymms[i-1] + nVars;
  
      return p;
  } /* end of Extra_SymmPairsAllocate */
  
  /**Function********************************************************************
  
    Synopsis    [Deallocates symmetry information structure.]
  
    Description []
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  void Extra_SymmPairsDissolve( Extra_SymmInfo_t * p )
  {
      free( p->pVars );
      free( p->pSymms[0] );
      free( p->pSymms    );
      free( p );
  } /* end of Extra_SymmPairsDissolve */
  
  /**Function********************************************************************
  
    Synopsis    [Allocates symmetry information structure.]
  
    Description []
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  void Extra_SymmPairsPrint( Extra_SymmInfo_t * p )
  {
      int i, k;
      printf( "\n" );
      for ( i = 0; i < p->nVars; i++ )
      {
          for ( k = 0; k <= i; k++ )
              printf( " " );
          for ( k = i+1; k < p->nVars; k++ )
              if ( p->pSymms[i][k] )
                  printf( "1" );
              else
                  printf( "." );
          printf( "\n" );
      }
  } /* end of Extra_SymmPairsPrint */
  
  
  /**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     []
  
  ******************************************************************************/
  Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp )
  {
      int i;
      int nSuppSize;
      Extra_SymmInfo_t * p;
      int * pMapVars2Nums;
      DdNode * bTemp;
      DdNode * zSet, * zCube, * zTemp;
      int iVar1, iVar2;
  
      nSuppSize = Extra_bddSuppSize( dd, bSupp );
  
      // allocate and clean the storage for symmetry info
      p = Extra_SymmPairsAllocate( nSuppSize );
  
      // allocate the storage for the temporary map
      pMapVars2Nums = ALLOC( int, dd->size );
      memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
  
      // assign the variables
      p->nVarsMax = dd->size;
  //  p->nNodes   = Cudd_DagSize( zPairs );
      p->nNodes   = 0;
      for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
      {
          p->pVars[i] = bTemp->index;
          pMapVars2Nums[bTemp->index] = i;
      }
  
      // write the symmetry info into the structure
      zSet = zPairs;   Cudd_Ref( zSet );
      while ( zSet != z0 )
      {
          // get the next cube
          zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );
  
          // add these two variables to the data structure
          assert( cuddT( cuddT(zCube) ) == z1 );
          iVar1 = zCube->index/2;
          iVar2 = cuddT(zCube)->index/2;
          if ( pMapVars2Nums[iVar1] < pMapVars2Nums[iVar2] )
              p->pSymms[ pMapVars2Nums[iVar1] ][ pMapVars2Nums[iVar2] ] = 1;
          else
              p->pSymms[ pMapVars2Nums[iVar2] ][ pMapVars2Nums[iVar1] ] = 1;
          // count the symmetric pairs
          p->nSymms ++;
  
          // update the cuver and deref the cube
          zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );
          Cudd_RecursiveDerefZdd( dd, zTemp );
          Cudd_RecursiveDerefZdd( dd, zCube );
  
      } // for each cube 
      Cudd_RecursiveDerefZdd( dd, zSet );
  
      FREE( pMapVars2Nums );
      return p;
  
  } /* end of Extra_SymmPairsCreateFromZdd */
  
  
  /**Function********************************************************************
  
    Synopsis    [Checks the possibility of two variables being symmetric.]
  
    Description [Returns 0 if vars are not symmetric. Return 1 if vars can be symmetric.]
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  int Extra_bddCheckVarsSymmetric( 
    DdManager * dd,   /* the DD manager */
    DdNode * bF,
    int iVar1,
    int iVar2) 
  {
      DdNode * bVars;
      int Res;
  
  //  return 1;
  
      assert( iVar1 != iVar2 );
      assert( iVar1 < dd->size );
      assert( iVar2 < dd->size );
  
      bVars = Cudd_bddAnd( dd, dd->vars[iVar1], dd->vars[iVar2] );   Cudd_Ref( bVars );
  
      Res = (int)( extraBddCheckVarsSymmetric( dd, bF, bVars ) == b1 );
  
      Cudd_RecursiveDeref( dd, bVars );
  
      return Res;
  } /* end of Extra_bddCheckVarsSymmetric */
  
  
  /**Function********************************************************************
  
    Synopsis    [Computes the classical symmetry information for the function.]
  
    Description [Uses the naive way of comparing cofactors.]
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc )
  {
      DdNode * bSupp, * bTemp;
      int nSuppSize;
      Extra_SymmInfo_t * p;
      int i, k;
  
      // compute the support
      bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
      nSuppSize = Extra_bddSuppSize( dd, bSupp );
  //printf( "Support = %d. ", nSuppSize );
  //Extra_bddPrint( dd, bSupp );
  //printf( "%d ", nSuppSize );
  
      // allocate the storage for symmetry info
      p = Extra_SymmPairsAllocate( nSuppSize );
  
      // assign the variables
      p->nVarsMax = dd->size;
      for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
          p->pVars[i] = bTemp->index;
  
      // go through the candidate pairs and check using Idea1
      for ( i = 0; i < nSuppSize; i++ )
      for ( k = i+1; k < nSuppSize; k++ )
      {
          p->pSymms[k][i] = p->pSymms[i][k] = Extra_bddCheckVarsSymmetricNaive( dd, bFunc, p->pVars[i], p->pVars[k] );
          if ( p->pSymms[i][k] )
               p->nSymms++;
      }
  
      Cudd_RecursiveDeref( dd, bSupp );
      return p;
  
  } /* end of Extra_SymmPairsComputeNaive */
  
  /**Function********************************************************************
  
    Synopsis    [Checks if the two variables are symmetric.]
  
    Description [Returns 0 if vars are not symmetric. Return 1 if vars are symmetric.]
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  int Extra_bddCheckVarsSymmetricNaive( 
    DdManager * dd,   /* the DD manager */
    DdNode * bF,
    int iVar1,
    int iVar2) 
  {
      DdNode * bCube1, * bCube2;
      DdNode * bCof01, * bCof10;
      int Res;
  
      assert( iVar1 != iVar2 );
      assert( iVar1 < dd->size );
      assert( iVar2 < dd->size );
  
      bCube1 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar1] ), dd->vars[iVar2] );   Cudd_Ref( bCube1 );
      bCube2 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar2] ), dd->vars[iVar1] );   Cudd_Ref( bCube2 );
  
      bCof01 = Cudd_Cofactor( dd, bF, bCube1 );  Cudd_Ref( bCof01 );
      bCof10 = Cudd_Cofactor( dd, bF, bCube2 );  Cudd_Ref( bCof10 );
  
      Res = (int)( bCof10 == bCof01 );
  
      Cudd_RecursiveDeref( dd, bCof01 );
      Cudd_RecursiveDeref( dd, bCof10 );
      Cudd_RecursiveDeref( dd, bCube1 );
      Cudd_RecursiveDeref( dd, bCube2 );
  
      return Res;
  } /* end of Extra_bddCheckVarsSymmetricNaive */
  
  
  /**Function********************************************************************
  
    Synopsis    [Builds ZDD representing the set of fixed-size variable tuples.]
  
    Description [Creates ZDD of all combinations of variables in Support that
    is represented by a BDD.]
  
    SideEffects [New ZDD variables are created if indices of the variables
                 present in the combination are larger than the currently
                 allocated number of ZDD variables.]
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode* Extra_zddTuplesFromBdd( 
    DdManager * dd,   /* the DD manager */
    int K,            /* the number of variables in tuples */
    DdNode * bVarsN)   /* the set of all variables represented as a BDD */
  {
      DdNode  *zRes;
      int     autoDynZ;
  
      autoDynZ = dd->autoDynZ;
      dd->autoDynZ = 0;
  
      do {
          /* transform the numeric arguments (K) into a DdNode* argument;
           * this allows us to use the standard internal CUDD cache */
          DdNode *bVarSet = bVarsN, *bVarsK = bVarsN;
          int     nVars = 0, i;
  
          /* determine the number of variables in VarSet */
          while ( bVarSet != b1 )
          {
              nVars++;
              /* make sure that the VarSet is a cube */
              if ( cuddE( bVarSet ) != b0 )
                  return NULL;
              bVarSet = cuddT( bVarSet );
          }
          /* make sure that the number of variables in VarSet is less or equal 
             that the number of variables that should be present in the tuples
          */
          if ( K > nVars )
              return NULL;
  
          /* the second argument in the recursive call stannds for <n>;
          /* reate the first argument, which stands for <k> 
           * as when we are talking about the tuple of <k> out of <n> */
          for ( i = 0; i < nVars-K; i++ )
              bVarsK = cuddT( bVarsK );
  
          dd->reordered = 0;
          zRes = extraZddTuplesFromBdd(dd, bVarsK, bVarsN );
  
      } while (dd->reordered == 1);
      dd->autoDynZ = autoDynZ;
      return zRes;
  
  } /* end of Extra_zddTuplesFromBdd */
  
  /**Function********************************************************************
  
    Synopsis    [Selects one subset from the set of subsets represented by a ZDD.]
  
    Description []
  
    SideEffects [None]
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode* Extra_zddSelectOneSubset( 
    DdManager * dd,   /* the DD manager */
    DdNode * zS)      /* the ZDD */
  {
      DdNode  *res;
      do {
          dd->reordered = 0;
          res = extraZddSelectOneSubset(dd, zS);
      } while (dd->reordered == 1);
      return(res);
  
  } /* end of Extra_zddSelectOneSubset */
  
  
  /*---------------------------------------------------------------------------*/
  /* Definition of internal functions                                          */
  /*---------------------------------------------------------------------------*/
  
  /**Function********************************************************************
  
    Synopsis    [Performs a recursive step of Extra_SymmPairsCompute.]
  
    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     []
  
  ******************************************************************************/
  DdNode * 
  extraZddSymmPairsCompute( 
    DdManager * dd,   /* the manager */
    DdNode * bFunc,   /* the function whose symmetries are computed */
    DdNode * bVars )  /* the set of variables on which this function depends */
  {
      DdNode * zRes;
      DdNode * bFR = Cudd_Regular(bFunc); 
  
      if ( cuddIsConstant(bFR) )
      {
          int nVars, i;
  
          // determine how many vars are in the bVars
          nVars = Extra_bddSuppSize( dd, bVars );
          if ( nVars < 2 )
              return z0;
          else
          {
              DdNode * bVarsK;
  
              // create the BDD bVarsK corresponding to K = 2;
              bVarsK = bVars;
              for ( i = 0; i < nVars-2; i++ )
                  bVarsK = cuddT( bVarsK );
              return extraZddTuplesFromBdd( dd, bVarsK, bVars );
          }
      }
      assert( bVars != b1 );
  
      if ( zRes = cuddCacheLookup2Zdd(dd, extraZddSymmPairsCompute, bFunc, bVars) )
          return zRes;
      else
      {
          DdNode * zRes0, * zRes1;
          DdNode * zTemp, * zPlus, * zSymmVars;             
          DdNode * bF0, * bF1;             
          DdNode * bVarsNew;
          int nVarsExtra;
          int LevelF;
  
          // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
          // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
          // count how many extra vars are there in bVars
          nVarsExtra = 0;
          LevelF = dd->perm[bFR->index];
          for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
              nVarsExtra++; 
          // the indexes (level) of variables should be synchronized now
          assert( bFR->index == bVarsNew->index );
  
          // cofactor the function
          if ( bFR != bFunc ) // bFunc is complemented 
          {
              bF0 = Cudd_Not( cuddE(bFR) );
              bF1 = Cudd_Not( cuddT(bFR) );
          }
          else
          {
              bF0 = cuddE(bFR);
              bF1 = cuddT(bFR);
          }
  
          // solve subproblems
          zRes0 = extraZddSymmPairsCompute( dd, bF0, cuddT(bVarsNew) );
          if ( zRes0 == NULL )
              return NULL;
          cuddRef( zRes0 );
  
          // if there is no symmetries in the negative cofactor
          // there is no need to test the positive cofactor
          if ( zRes0 == z0 )
              zRes = zRes0;  // zRes takes reference
          else
          {
              zRes1 = extraZddSymmPairsCompute( dd, bF1, cuddT(bVarsNew) );
              if ( zRes1 == NULL )
              {
                  Cudd_RecursiveDerefZdd( dd, zRes0 );
                  return NULL;
              }
              cuddRef( zRes1 );
  
              // only those variables are pair-wise symmetric 
              // that are pair-wise symmetric in both cofactors
              // therefore, intersect the solutions
              zRes = cuddZddIntersect( dd, zRes0, zRes1 );
              if ( zRes == NULL )
              {
                  Cudd_RecursiveDerefZdd( dd, zRes0 );
                  Cudd_RecursiveDerefZdd( dd, zRes1 );
                  return NULL;
              }
              cuddRef( zRes );
              Cudd_RecursiveDerefZdd( dd, zRes0 );
              Cudd_RecursiveDerefZdd( dd, zRes1 );
          }
  
          // consider the current top-most variable and find all the vars
          // that are pairwise symmetric with it
          // these variables are returned as a set of ZDD singletons
          zSymmVars = extraZddGetSymmetricVars( dd, bF1, bF0, cuddT(bVarsNew) );
          if ( zSymmVars == NULL )
          {
              Cudd_RecursiveDerefZdd( dd, zRes );
              return NULL;
          }
          cuddRef( zSymmVars );
  
          // attach the topmost variable to the set, to get the variable pairs
          // use the positive polarity ZDD variable for the purpose
  
          // there is no need to do so, if zSymmVars is empty
          if ( zSymmVars == z0 )
              Cudd_RecursiveDerefZdd( dd, zSymmVars );
          else
          {
              zPlus = cuddZddGetNode( dd, 2*bFR->index, zSymmVars, z0 );
              if ( zPlus == NULL ) 
              {
                  Cudd_RecursiveDerefZdd( dd, zRes );
                  Cudd_RecursiveDerefZdd( dd, zSymmVars );
                  return NULL;
              }
              cuddRef( zPlus );
              cuddDeref( zSymmVars );
  
              // add these variable pairs to the result
              zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
              if ( zRes == NULL )
              {
                  Cudd_RecursiveDerefZdd( dd, zTemp );
                  Cudd_RecursiveDerefZdd( dd, zPlus );
                  return NULL;
              }
              cuddRef( zRes );
              Cudd_RecursiveDerefZdd( dd, zTemp );
              Cudd_RecursiveDerefZdd( dd, zPlus );
          }
  
          // only zRes is referenced at this point
  
          // if we skipped some variables, these variables cannot be symmetric with
          // any variables that are currently in the support of bF, but they can be 
          // symmetric with the variables that are in bVars but not in the support of bF
          if ( nVarsExtra )
          {
              // it is possible to improve this step:
              // (1) there is no need to enter here, if nVarsExtra < 2
  
              // create the set of topmost nVarsExtra in bVars
              DdNode * bVarsExtra;
              int nVars;
  
              // remove from bVars all the variable that are in the support of bFunc
              bVarsExtra = extraBddReduceVarSet( dd, bVars, bFunc );  
              if ( bVarsExtra == NULL )
              {
                  Cudd_RecursiveDerefZdd( dd, zRes );
                  return NULL;
              }
              cuddRef( bVarsExtra );
  
              // determine how many vars are in the bVarsExtra
              nVars = Extra_bddSuppSize( dd, bVarsExtra );
              if ( nVars < 2 )
              {
                  Cudd_RecursiveDeref( dd, bVarsExtra );
              }
              else
              {
                  int i;
                  DdNode * bVarsK;
  
                  // create the BDD bVarsK corresponding to K = 2;
                  bVarsK = bVarsExtra;
                  for ( i = 0; i < nVars-2; i++ )
                      bVarsK = cuddT( bVarsK );
  
                  // create the 2 variable tuples
                  zPlus = extraZddTuplesFromBdd( dd, bVarsK, bVarsExtra );
                  if ( zPlus == NULL )
                  {
                      Cudd_RecursiveDeref( dd, bVarsExtra );
                      Cudd_RecursiveDerefZdd( dd, zRes );
                      return NULL;
                  }
                  cuddRef( zPlus );
                  Cudd_RecursiveDeref( dd, bVarsExtra );
  
                  // add these to the result
                  zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
                  if ( zRes == NULL )
                  {
                      Cudd_RecursiveDerefZdd( dd, zTemp );
                      Cudd_RecursiveDerefZdd( dd, zPlus );
                      return NULL;
                  }
                  cuddRef( zRes );
                  Cudd_RecursiveDerefZdd( dd, zTemp );
                  Cudd_RecursiveDerefZdd( dd, zPlus );
              }
          }
          cuddDeref( zRes );
  
  
          /* insert the result into cache */
          cuddCacheInsert2(dd, extraZddSymmPairsCompute, bFunc, bVars, zRes);
          return zRes;
      }
  } /* end of extraZddSymmPairsCompute */
  
  /**Function********************************************************************
  
    Synopsis    [Performs a recursive step of Extra_zddGetSymmetricVars.]
  
    Description [Returns the set of ZDD singletons, containing those positive
    ZDD variables that correspond to BDD variables x, for which it is true 
    that bF(x=0) == bG(x=1).]
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * extraZddGetSymmetricVars( 
    DdManager * dd,    /* the DD manager */
    DdNode * bF,       /* the first function  - originally, the positive cofactor */
    DdNode * bG,       /* the second function - originally, the negative cofactor */
    DdNode * bVars)    /* the set of variables, on which F and G depend */
  {
      DdNode * zRes;
      DdNode * bFR = Cudd_Regular(bF); 
      DdNode * bGR = Cudd_Regular(bG); 
  
      if ( cuddIsConstant(bFR) && cuddIsConstant(bGR) )
      {
          if ( bF == bG )
              return extraZddGetSingletons( dd, bVars );
          else 
              return z0;
      }
      assert( bVars != b1 );
  
      if ( zRes = cuddCacheLookupZdd(dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars) )
          return zRes;
      else
      {
          DdNode * zRes0, * zRes1;             
          DdNode * zPlus, * zTemp;
          DdNode * bF0, * bF1;             
          DdNode * bG0, * bG1;             
          DdNode * bVarsNew;
      
          int LevelF = cuddI(dd,bFR->index);
          int LevelG = cuddI(dd,bGR->index);
          int LevelFG;
  
          if ( LevelF < LevelG )
              LevelFG = LevelF;
          else
              LevelFG = LevelG;
  
          // at least one of the arguments is not a constant
          assert( LevelFG < dd->size );
  
          // every variable in bF and bG should be also in bVars, therefore LevelFG cannot be above LevelV
          // if LevelFG is below LevelV, scroll through the vars in bVars to the same level as LevelFG
          for ( bVarsNew = bVars; LevelFG > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) );
          assert( LevelFG == dd->perm[bVarsNew->index] );
  
          // cofactor the functions
          if ( LevelF == LevelFG )
          {
              if ( bFR != bF ) // bF is complemented 
              {
                  bF0 = Cudd_Not( cuddE(bFR) );
                  bF1 = Cudd_Not( cuddT(bFR) );
              }
              else
              {
                  bF0 = cuddE(bFR);
                  bF1 = cuddT(bFR);
              }
          }
          else 
              bF0 = bF1 = bF;
  
          if ( LevelG == LevelFG )
          {
              if ( bGR != bG ) // bG is complemented 
              {
                  bG0 = Cudd_Not( cuddE(bGR) );
                  bG1 = Cudd_Not( cuddT(bGR) );
              }
              else
              {
                  bG0 = cuddE(bGR);
                  bG1 = cuddT(bGR);
              }
          }
          else 
              bG0 = bG1 = bG;
  
          // solve subproblems
          zRes0 = extraZddGetSymmetricVars( dd, bF0, bG0, cuddT(bVarsNew) );
          if ( zRes0 == NULL ) 
              return NULL;
          cuddRef( zRes0 );
  
          // if there is not symmetries in the negative cofactor
          // there is no need to test the positive cofactor
          if ( zRes0 == z0 )
              zRes = zRes0;  // zRes takes reference
          else
          {
              zRes1 = extraZddGetSymmetricVars( dd, bF1, bG1, cuddT(bVarsNew) );
              if ( zRes1 == NULL ) 
              {
                  Cudd_RecursiveDerefZdd( dd, zRes0 );
                  return NULL;
              }
              cuddRef( zRes1 );
  
              // only those variables should belong to the resulting set 
              // for which the property is true for both cofactors
              zRes = cuddZddIntersect( dd, zRes0, zRes1 );
              if ( zRes == NULL )
              {
                  Cudd_RecursiveDerefZdd( dd, zRes0 );
                  Cudd_RecursiveDerefZdd( dd, zRes1 );
                  return NULL;
              }
              cuddRef( zRes );
              Cudd_RecursiveDerefZdd( dd, zRes0 );
              Cudd_RecursiveDerefZdd( dd, zRes1 );
          }
  
          // add one more singleton if the property is true for this variable
          if ( bF0 == bG1 )
          {
              zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
              if ( zPlus == NULL ) 
              {
                  Cudd_RecursiveDerefZdd( dd, zRes );
                  return NULL;
              }
              cuddRef( zPlus );
  
              // add these variable pairs to the result
              zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
              if ( zRes == NULL )
              {
                  Cudd_RecursiveDerefZdd( dd, zTemp );
                  Cudd_RecursiveDerefZdd( dd, zPlus );
                  return NULL;
              }
              cuddRef( zRes );
              Cudd_RecursiveDerefZdd( dd, zTemp );
              Cudd_RecursiveDerefZdd( dd, zPlus );
          }
  
          if ( bF == bG && bVars != bVarsNew )
          { 
              // if the functions are equal, so are their cofactors
              // add those variables from V that are above F and G 
  
              DdNode * bVarsExtra;
  
              assert( LevelFG > dd->perm[bVars->index] );
  
              // create the BDD of the extra variables
              bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsNew );
              if ( bVarsExtra == NULL )
              {
                  Cudd_RecursiveDerefZdd( dd, zRes );
                  return NULL;
              }
              cuddRef( bVarsExtra );
  
              zPlus = extraZddGetSingletons( dd, bVarsExtra );
              if ( zPlus == NULL )
              {
                  Cudd_RecursiveDeref( dd, bVarsExtra );
                  Cudd_RecursiveDerefZdd( dd, zRes );
                  return NULL;
              }
              cuddRef( zPlus );
              Cudd_RecursiveDeref( dd, bVarsExtra );
  
              // add these to the result
              zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
              if ( zRes == NULL )
              {
                  Cudd_RecursiveDerefZdd( dd, zTemp );
                  Cudd_RecursiveDerefZdd( dd, zPlus );
                  return NULL;
              }
              cuddRef( zRes );
              Cudd_RecursiveDerefZdd( dd, zTemp );
              Cudd_RecursiveDerefZdd( dd, zPlus );
          }
          cuddDeref( zRes );
  
          cuddCacheInsert( dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars, zRes );
          return zRes;
      }
  }   /* end of extraZddGetSymmetricVars */
  
  
  /**Function********************************************************************
  
    Synopsis    [Performs a recursive step of Extra_zddGetSingletons.]
  
    Description [Returns the set of ZDD singletons, containing those positive 
    polarity ZDD variables that correspond to the BDD variables in bVars.]
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * extraZddGetSingletons( 
    DdManager * dd,    /* the DD manager */
    DdNode * bVars)    /* the set of variables */
  {
      DdNode * zRes;
  
      if ( bVars == b1 )
  //    if ( bVars == b0 )  // bug fixed by Jin Zhang, Jan 23, 2004
          return z1;
  
      if ( zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars) )
          return zRes;
      else
      {
          DdNode * zTemp, * zPlus;          
  
          // solve subproblem
          zRes = extraZddGetSingletons( dd, cuddT(bVars) );
          if ( zRes == NULL ) 
              return NULL;
          cuddRef( zRes );
          
          zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
          if ( zPlus == NULL ) 
          {
              Cudd_RecursiveDerefZdd( dd, zRes );
              return NULL;
          }
          cuddRef( zPlus );
  
          // add these to the result
          zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
          if ( zRes == NULL )
          {
              Cudd_RecursiveDerefZdd( dd, zTemp );
              Cudd_RecursiveDerefZdd( dd, zPlus );
              return NULL;
          }
          cuddRef( zRes );
          Cudd_RecursiveDerefZdd( dd, zTemp );
          Cudd_RecursiveDerefZdd( dd, zPlus );
          cuddDeref( zRes );
  
          cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes );
          return zRes;
      }
  }   /* end of extraZddGetSingletons */
  
  
  /**Function********************************************************************
  
    Synopsis    [Performs a recursive step of Extra_bddReduceVarSet.]
  
    Description [Returns the set of all variables in the given set that are not in the 
    support of the given function.]
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * extraBddReduceVarSet( 
    DdManager * dd,    /* the DD manager */
    DdNode * bVars,    /* the set of variables to be reduced */
    DdNode * bF)       /* the function whose support is used for reduction */
  {
      DdNode * bRes;
      DdNode * bFR = Cudd_Regular(bF);
  
      if ( cuddIsConstant(bFR) || bVars == b1 )
          return bVars;
  
      if ( bRes = cuddCacheLookup2(dd, extraBddReduceVarSet, bVars, bF) )
          return bRes;
      else
      {
          DdNode * bF0, * bF1;             
          DdNode * bVarsThis, * bVarsLower, * bTemp;
          int LevelF;
  
          // if LevelF is below LevelV, scroll through the vars in bVars 
          LevelF = dd->perm[bFR->index];
          for ( bVarsThis = bVars; LevelF > cuddI(dd,bVarsThis->index); bVarsThis = cuddT(bVarsThis) );
          // scroll also through the current var, because it should be not be added
          if ( LevelF == cuddI(dd,bVarsThis->index) )
              bVarsLower = cuddT(bVarsThis);
          else
              bVarsLower = bVarsThis;
  
          // cofactor the function
          if ( bFR != bF ) // bFunc is complemented 
          {
              bF0 = Cudd_Not( cuddE(bFR) );
              bF1 = Cudd_Not( cuddT(bFR) );
          }
          else
          {
              bF0 = cuddE(bFR);
              bF1 = cuddT(bFR);
          }
  
          // solve subproblems
          bRes = extraBddReduceVarSet( dd, bVarsLower, bF0 );
          if ( bRes == NULL ) 
              return NULL;
          cuddRef( bRes );
  
          bRes = extraBddReduceVarSet( dd, bTemp = bRes, bF1 );
          if ( bRes == NULL ) 
          {
              Cudd_RecursiveDeref( dd, bTemp );
              return NULL;
          }
          cuddRef( bRes );
          Cudd_RecursiveDeref( dd, bTemp );
  
          // the current var should not be added
          // add the skipped vars
          if ( bVarsThis != bVars )
          {
              DdNode * bVarsExtra;
  
              // extract the skipped variables
              bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsThis );
              if ( bVarsExtra == NULL )
              {
                  Cudd_RecursiveDeref( dd, bRes );
                  return NULL;
              }
              cuddRef( bVarsExtra );
  
              // add these variables
              bRes = cuddBddAndRecur( dd, bTemp = bRes, bVarsExtra );
              if ( bRes == NULL ) 
              {
                  Cudd_RecursiveDeref( dd, bTemp );
                  Cudd_RecursiveDeref( dd, bVarsExtra );
                  return NULL;
              }
              cuddRef( bRes );
              Cudd_RecursiveDeref( dd, bTemp );
              Cudd_RecursiveDeref( dd, bVarsExtra );
          }
          cuddDeref( bRes );
  
          cuddCacheInsert2( dd, extraBddReduceVarSet, bVars, bF, bRes );
          return bRes;
      }
  }   /* end of extraBddReduceVarSet */
  
  
  /**Function********************************************************************
  
    Synopsis    [Performs the recursive step of Extra_bddCheckVarsSymmetric().]
  
    Description [Returns b0 if the variables are not symmetric. Returns b1 if the
    variables can be symmetric. The variables are represented in the form of a 
    two-variable cube. In case the cube contains one variable (below Var1 level),
    the cube's pointer is complemented if the variable Var1 occurred on the 
    current path; otherwise, the cube's pointer is regular. Uses additional 
    complemented bit (Hash_Not) to mark the result if in the BDD rooted that this
    node there is a branch passing though the node labeled with Var2.]
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * extraBddCheckVarsSymmetric( 
    DdManager * dd,    /* the DD manager */
    DdNode * bF,
    DdNode * bVars) 
  {
      DdNode * bRes;
  
      if ( bF == b0 )
          return b1;
  
      assert( bVars != b1 );
      
      if ( bRes = cuddCacheLookup2(dd, extraBddCheckVarsSymmetric, bF, bVars) )
          return bRes;
      else
      {
          DdNode * bRes0, * bRes1;
          DdNode * bF0, * bF1;             
          DdNode * bFR = Cudd_Regular(bF);
          int LevelF = cuddI(dd,bFR->index);
  
          DdNode * bVarsR = Cudd_Regular(bVars);
          int fVar1Pres;
          int iLev1;
          int iLev2;
  
          if ( bVarsR != bVars ) // cube's pointer is complemented
          {
              assert( cuddT(bVarsR) == b1 );
              fVar1Pres = 1;                    // the first var is present on the path
              iLev1 = -1;                       // we are already below the first var level
              iLev2 = dd->perm[bVarsR->index];  // the level of the second var
          }
          else  // cube's pointer is NOT complemented
          {
              fVar1Pres = 0;                    // the first var is absent on the path
              if ( cuddT(bVars) == b1 )
              {
                  iLev1 = -1;                             // we are already below the first var level 
                  iLev2 = dd->perm[bVars->index];         // the level of the second var
              }
              else
              {
                  assert( cuddT(cuddT(bVars)) == b1 );
                  iLev1 = dd->perm[bVars->index];         // the level of the first var 
                  iLev2 = dd->perm[cuddT(bVars)->index];  // the level of the second var
              }
          }
  
          // cofactor the function
          // the cofactors are needed only if we are above the second level
          if ( LevelF < iLev2 )
          {
              if ( bFR != bF ) // bFunc is complemented 
              {
                  bF0 = Cudd_Not( cuddE(bFR) );
                  bF1 = Cudd_Not( cuddT(bFR) );
              }
              else
              {
                  bF0 = cuddE(bFR);
                  bF1 = cuddT(bFR);
              }
          }
          else
              bF0 = bF1 = NULL;
  
          // consider five cases:
          // (1) F is above iLev1
          // (2) F is on the level iLev1
          // (3) F is between iLev1 and iLev2
          // (4) F is on the level iLev2
          // (5) F is below iLev2
  
          // (1) F is above iLev1
          if ( LevelF < iLev1 )
          {
              // the returned result cannot have the hash attribute
              // because we still did not reach the level of Var1;
              // the attribute never travels above the level of Var1
              bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
  //          assert( !Hash_IsComplement( bRes0 ) );
              assert( bRes0 != z0 );
              if ( bRes0 == b0 )
                  bRes = b0;
              else
                  bRes = extraBddCheckVarsSymmetric( dd, bF1, bVars );
  //          assert( !Hash_IsComplement( bRes ) );
              assert( bRes != z0 );
          }
          // (2) F is on the level iLev1
          else if ( LevelF == iLev1 )
          {
              bRes0 = extraBddCheckVarsSymmetric( dd, bF0, Cudd_Not( cuddT(bVars) ) );
              if ( bRes0 == b0 )
                  bRes = b0;
              else
              {
                  bRes1 = extraBddCheckVarsSymmetric( dd, bF1, Cudd_Not( cuddT(bVars) ) );
                  if ( bRes1 == b0 )
                      bRes = b0;
                  else
                  {
  //                  if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) )
                      if ( bRes0 == z0 || bRes1 == z0 )
                          bRes = b1;
                      else
                          bRes = b0;
                  }
              }
          }
          // (3) F is between iLev1 and iLev2
          else if ( LevelF < iLev2 )
          {
              bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
              if ( bRes0 == b0 )
                  bRes = b0;
              else
              {
                  bRes1 = extraBddCheckVarsSymmetric( dd, bF1, bVars );
                  if ( bRes1 == b0 )
                      bRes = b0;
                  else
                  {
  //                  if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) )
  //                      bRes = Hash_Not( b1 );
                      if ( bRes0 == z0 || bRes1 == z0 )
                          bRes = z0;
                      else
                          bRes = b1;
                  }
              }
          }
          // (4) F is on the level iLev2
          else if ( LevelF == iLev2 )
          {
              // this is the only place where the hash attribute (Hash_Not) can be added 
              // to the result; it can be added only if the path came through the node
              // lebeled with Var1; therefore, the hash attribute cannot be returned
              // to the caller function
              if ( fVar1Pres )
  //              bRes = Hash_Not( b1 );
                  bRes = z0;
              else 
                  bRes = b0;
          }
          // (5) F is below iLev2
          else // if ( LevelF > iLev2 )
          {
              // it is possible that the path goes through the node labeled by Var1
              // and still everything is okay; we do not label with Hash_Not here
              // because the path does not go through node labeled by Var2
              bRes = b1;
          }
  
          cuddCacheInsert2(dd, extraBddCheckVarsSymmetric, bF, bVars, bRes);
          return bRes;
      }
  } /* end of extraBddCheckVarsSymmetric */
  
  /**Function********************************************************************
  
    Synopsis    [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]
  
    Description [Generates in a bottom-up fashion ZDD for all combinations
                 composed of k variables out of variables belonging to Support.]
  
    SideEffects []
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode* extraZddTuplesFromBdd( 
    DdManager * dd,   /* the DD manager */
    DdNode * bVarsK,   /* the number of variables in tuples */
    DdNode * bVarsN)   /* the set of all variables */
  {
      DdNode *zRes, *zRes0, *zRes1;
      statLine(dd); 
  
      /* terminal cases */
  /*  if ( k < 0 || k > n )
   *      return dd->zero;
   *  if ( n == 0 )
   *      return dd->one; 
   */
      if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
          return z0;
      if ( bVarsN == b1 )
          return z1;
  
      /* check cache */
      zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN);
      if (zRes)
          return(zRes);
  
      /* ZDD in which this variable is 0 */
  /*  zRes0 = extraZddTuplesFromBdd( dd, k,     n-1 ); */
      zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) );
      if ( zRes0 == NULL ) 
          return NULL;
      cuddRef( zRes0 );
  
      /* ZDD in which this variable is 1 */
  /*  zRes1 = extraZddTuplesFromBdd( dd, k-1,          n-1 ); */
      if ( bVarsK == b1 )
      {
          zRes1 = z0;
          cuddRef( zRes1 );
      }
      else
      {
          zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) );
          if ( zRes1 == NULL ) 
          {
              Cudd_RecursiveDerefZdd( dd, zRes0 );
              return NULL;
          }
          cuddRef( zRes1 );
      }
  
      /* compose Res0 and Res1 with the given ZDD variable */
      zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 );
      if ( zRes == NULL ) 
      {
          Cudd_RecursiveDerefZdd( dd, zRes0 );
          Cudd_RecursiveDerefZdd( dd, zRes1 );
          return NULL;
      }
      cuddDeref( zRes0 );
      cuddDeref( zRes1 );
  
      /* insert the result into cache */
      cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes);
      return zRes;
  
  } /* end of extraZddTuplesFromBdd */
  
  
  /**Function********************************************************************
  
    Synopsis    [Performs the recursive step of Extra_zddSelectOneSubset.]
  
    Description []
  
    SideEffects [None]
  
    SeeAlso     []
  
  ******************************************************************************/
  DdNode * extraZddSelectOneSubset( 
    DdManager * dd, 
    DdNode * zS )
  // selects one subset from the ZDD zS
  // returns z0 if and only if zS is an empty set of cubes
  {
      DdNode * zRes;
  
      if ( zS == z0 )    return z0;
      if ( zS == z1 )    return z1;
      
      // check cache
      if ( zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS ) )
          return zRes;
      else
      {
          DdNode * zS0, * zS1, * zTemp; 
  
          zS0 = cuddE(zS);
          zS1 = cuddT(zS);
  
          if ( zS0 != z0 )
          {
              zRes = extraZddSelectOneSubset( dd, zS0 );
              if ( zRes == NULL )
                  return NULL;
          }
          else // if ( zS0 == z0 )
          {
              assert( zS1 != z0 );
              zRes = extraZddSelectOneSubset( dd, zS1 );
              if ( zRes == NULL )
                  return NULL;
              cuddRef( zRes );
  
              zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 );
              if ( zRes == NULL ) 
              {
                  Cudd_RecursiveDerefZdd( dd, zTemp );
                  return NULL;
              }
              cuddDeref( zTemp );
          }
  
          // insert the result into cache
          cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes );
          return zRes;
      }       
  } /* end of extraZddSelectOneSubset */
  
  
  /*---------------------------------------------------------------------------*/
  /* Definition of static Functions                                            */
  /*---------------------------------------------------------------------------*/
  