src/restr/restrHammingD.c

Go to the documentation of this file.

#include "restrInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static bdd_node * restrHxygthxz(bdd_manager *dd, int N, bdd_node **x, bdd_node **y, bdd_node **z);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

bdd_node *
RestrSelectLeastHammingDStates(
  bdd_manager   *dd,
  bdd_node      *oldTR,
  bdd_node      *pTR,
  bdd_node      **xVars,
  bdd_node      **yVars,
  bdd_node      **vVars,
  int             nVars,
  int             nPi)
{
  bdd_node *result;
  bdd_node *temp1,*Pi;
  double oldSize,newSize;
  int twice = 0;

  /* restrHxygthxz is a function that returns 1 if HD(x,y) > HD(x,z) */
  bdd_ref(Pi = restrHxygthxz(dd,nVars,xVars,yVars,vVars));
  result = bdd_priority_select(dd,pTR,xVars,yVars,vVars,
                               Pi,nVars,NULL);
  bdd_recursive_deref(dd,Pi);
  if(! result) {
    return NIL(bdd_node);
  }
  bdd_ref(result);

  oldSize = bdd_count_minterm(dd,oldTR,2*nVars+nPi);
  newSize = bdd_count_minterm(dd,result,2*nVars+nPi);

  /* As restrHxygthxz is not a priority function, result might still be
     non-deterministic. Hence use the tie breaker bdd_dxygtdxz to make the
     "result" deterministic */

  if(newSize > oldSize) {
    temp1 = bdd_priority_select(dd,result,xVars,yVars,vVars,
                                NIL(bdd_node),nVars,bdd_dxygtdxz);
    if(! temp1) {
      return NIL(bdd_node);
    } 
    bdd_ref(temp1);
    bdd_recursive_deref(dd,result);
    result = temp1;
    twice = 1;
  }
  if (twice) {
    newSize = bdd_count_minterm(dd,result,2*nVars+nPi);
    assert(oldSize == newSize);
  }

  if(result == oldTR) {
    fprintf(vis_stdout,"** restr info: HammingD heuristic produces no restructuring.\n");
  }

  return result;

#if 0
  /* Compute a priority function that looks like:
   * \Pi_H(x,y,z) = H(x,y,z) \vee (\neg H(x,z,y) \wedge \Pi_{RP}(x,y,z))
   *
   * where H(x,y,z) = 1 if HD(x,y) < HD(x,z) and 0 otherwise;
   * Here z variables are vVars.
   */

  /* Observe that below I am computing H(x,z,y) */
  bdd_ref(Hxyz = restrHxygthxz(dd,nVars,xVars,vVars,yVars));
  bdd_ref(Hxzy = bdd_bdd_swap_variables(dd,Hxyz,yVars,vVars,nVars));
  bdd_ref(piRP = bdd_dxygtdxz(dd,nVars,xVars,yVars,vVars));

  bdd_ref(Pi = bdd_bdd_ite(dd,Hxyz,bdd_not_bdd_node(Hxzy),piRP));
  bdd_recursive_deref(dd,Hxzy);
  bdd_recursive_deref(dd,piRP);
  bdd_recursive_deref(dd,Hxyz);

  /* Compute \Pi_H(x,z,y) and use priority select formulation */
  bdd_ref(temp = bdd_bdd_swap_variables(dd,Pi,yVars,vVars,nVars));
  bdd_recursive_deref(dd,Pi);
  Pi = temp;
  result = bdd_priority_select(dd,pTR,xVars,yVars,vVars,
                               Pi,nVars,NULL);
  if(! result) {
    return NIL(bdd_node);
  }
  bdd_ref(result);
#endif
}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

static bdd_node *
restrHxygthxz(
  bdd_manager *dd, 
  int N,         
  bdd_node **x,    
  bdd_node **y,    
  bdd_node **z)    
{
  bdd_node **dEqualToINodes, **tempDEqualToINodes;
  bdd_node *z1, *z2, *z3, *z4, *y1, *y2;
  bdd_node *one, *zero;
  bdd_node *temp;
  bdd_node *result;
  int i, j, m;
  int fromIndex, toIndex;

  dEqualToINodes = ALLOC(bdd_node *, 2*N+1);
  tempDEqualToINodes = ALLOC(bdd_node *, 2*N+1);

  one = bdd_read_one(dd);
  zero = bdd_not_bdd_node(one);

  for(i = 0; i <= N; i++) {
    dEqualToINodes[i] = zero;
    bdd_ref(dEqualToINodes[i]);
    tempDEqualToINodes[i] = zero;
    bdd_ref(tempDEqualToINodes[i]);
  }
  for(i = N+1; i < 2*N+1; i++) {
    dEqualToINodes[i] = one;
    bdd_ref(dEqualToINodes[i]);
    tempDEqualToINodes[i] = one;
    bdd_ref(tempDEqualToINodes[i]);
  }

  /* Loop to build the rest of the BDD */
  for(i = N-1; i >= 0; i--) {
    fromIndex = N - restrMin(N-i-1,i);
    toIndex = restrMin(N-i,i) + N;

    for(j = fromIndex;j <= toIndex; j++) {
      z1 = bdd_bdd_ite(dd,z[i],tempDEqualToINodes[j],
                       tempDEqualToINodes[j-1]);
      if(! z1){
        goto endgame;
      }
      bdd_ref(z1);
 
      z2 = bdd_bdd_ite(dd,z[i],tempDEqualToINodes[j+1],
                       tempDEqualToINodes[j]);
      if(! z2){
        bdd_recursive_deref(dd,z1);
        goto endgame;
      }
      bdd_ref(z2);
 
      z3 = bdd_bdd_ite(dd,z[i],tempDEqualToINodes[j],
                       tempDEqualToINodes[j+1]);
      if(! z3){
        bdd_recursive_deref(dd,z1);
        bdd_recursive_deref(dd,z2);
        goto endgame;
      }
      bdd_ref(z3);
 
      z4 = bdd_bdd_ite(dd,z[i],tempDEqualToINodes[j-1],
                       tempDEqualToINodes[j]);
      if(! z4){
        bdd_recursive_deref(dd,z1);
        bdd_recursive_deref(dd,z2);
        bdd_recursive_deref(dd,z3);
        goto endgame;
      }
      bdd_ref(z4);
 
      y1 = bdd_bdd_ite(dd,y[i],z1,z2);
      if(! y1){
        bdd_recursive_deref(dd,z1);
        bdd_recursive_deref(dd,z2);
        bdd_recursive_deref(dd,z3);
        bdd_recursive_deref(dd,z4);
        goto endgame;
      }
      bdd_ref(y1);
 
      y2 = bdd_bdd_ite(dd,y[i],z3,z4);
      if(! y2){
        bdd_recursive_deref(dd,z1);
        bdd_recursive_deref(dd,z2);
        bdd_recursive_deref(dd,z3);
        bdd_recursive_deref(dd,z4);
        bdd_recursive_deref(dd,y1);
        goto endgame;
      }
      bdd_ref(y2);
 
      bdd_recursive_deref(dd,z1);
      bdd_recursive_deref(dd,z2);
      bdd_recursive_deref(dd,z3);
      bdd_recursive_deref(dd,z4);
 
      temp = bdd_bdd_ite(dd,x[i],y1,y2);
      if(! temp){
        bdd_recursive_deref(dd,y1);
        bdd_recursive_deref(dd,y2);
        goto endgame;
      }
      bdd_ref(temp);
      dEqualToINodes[j] = temp;
      bdd_recursive_deref(dd,y1);
      bdd_recursive_deref(dd,y2);
    }

    for(j = 0; j < 2*N+1; j++) {
      if(tempDEqualToINodes[j]) {
        bdd_recursive_deref(dd,tempDEqualToINodes[j]);
      }
      tempDEqualToINodes[j] = dEqualToINodes[j]; 
      if(tempDEqualToINodes[j]) {
        bdd_ref(tempDEqualToINodes[j]);
      }
      if(dEqualToINodes[j] &&
         j >= fromIndex && j <= toIndex) {
        bdd_recursive_deref(dd,dEqualToINodes[j]);
        /* To be safe */
        dEqualToINodes[j] = NIL(bdd_node);
      }
    }
  }
  /* Clean up */
  for(j = 0; j < N; j++) {
    if(tempDEqualToINodes[j]) {
      bdd_recursive_deref(dd,tempDEqualToINodes[j]);
    }
  }
  for(j = N+1; j < 2*N+1; j++) {
    if(tempDEqualToINodes[j]) {
      bdd_recursive_deref(dd,tempDEqualToINodes[j]);
    }
  }

  result = tempDEqualToINodes[N];
  bdd_deref(result);

  FREE(dEqualToINodes);
  FREE(tempDEqualToINodes);

  return result;

endgame:
  for(m = 0; m < 2*N+1; m++) {
    if(tempDEqualToINodes[m]) {
      bdd_recursive_deref(dd,tempDEqualToINodes[m]);
    }
  }
  for(m = fromIndex; m < j; m++) {
    bdd_recursive_deref(dd,dEqualToINodes[m]);
  }
  FREE(dEqualToINodes);
  FREE(tempDEqualToINodes);

  return NULL;
}