/**CFile***********************************************************************

  FileName    [restrHammingD.c]

  PackageName [restr]

  Synopsis [The function in this file implements the Hamming distance heuristic
  to restructure the STG.]

  Description [The function in this file implements the Hamming distance
  heuristic to restructure the STG. Please refer to "A symbolic algorithm for
  low power sequential synthesis," ISLPED 97, for more details.]

  SeeAlso     [restrFaninout.c restrCProj.c]

  Author      [Balakrishna Kumthekar <kumtheka@colorado.edu>]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include "restrInt.h"

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


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


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

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


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


/**AutomaticStart*************************************************************/

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

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

/**AutomaticEnd***************************************************************/


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

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

/**Function********************************************************************

  Synopsis [This procedure implements the Hamming distance heuristic to
  restructure the STG. Returns the BDD of the restructured STG.]

  Description [This procedure implements the Hamming distance heuristic to
  restructure the STG. A priority function based on hamming distance is used to
  select destination state. oldTR is a BDD representing the transition relation
  of an FSM. pTR is the augmented transition relation. Both pTR and oldTR are
  functions of xVars and yVars. vVars are auxillary variables used inside this
  procedure. The three sets of variables, xVars, yVars and vVars are of length
  nVars. nPi are the number of primary input variables in the FSM.

  This heuristic selects a destination state such that the number of bit
  changes per state transition is minimized.  In order to do that the following
  function is utilized.

  H(x,y,v) = 1 if HD(x,y) < HD(x,v)
           = 0 otherwise

  where HD(x,y) is the hamming distance between states encoded by x and
  y. However, H(x,y,v) is not a priority function. To break the tie, relative
  proximity function is used. H(x,y,v) and the relative proximity function are
  used to defined a composite priority functioin.

  Please refer to "A symbolic algorithm for low power sequential synthesis,"
  ISLPED 97, for more details.]

  SideEffects [None]

  SeeAlso [RestrMinimizeFsmByCProj RestrMinimizeFsmByFaninFanout
  bdd_priority_select]

******************************************************************************/
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                                            */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis [Returns a BDD F(x,y,z) such that F(x,y,z) equals 1 when HD(x,y) >
  HD(x,z), and 0 otherwise. Returns the BDD if successful else NULL.]

  Description [This function generates a BDD for the function HD(x,y) >
  HD(x,z). x,y, and z are N-bit numbers, x[0],x[1] ... x[N-1], y[0], y[1]
  ... y[N-1] and z[0], z[1] ... z[N-1]. Hamming distance is defined as the
  number of bits differing in a given pair of encodings (X,Y). The BDD is built
  bottom-up.]

  SideEffects [None]

  SeeAlso     [bdd_priority_select bdd_add_hamming]

******************************************************************************/
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;
}