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

  FileName    [restrFaninout.c]

  PackageName [restr]

  Synopsis [Routines in this file implement the Fanin and Fanin-Fanout oriented
  restructuring heuristics.]

  Description [Routines in the file implement the Fanin oriented and
  Fanin-Fanout oriented restructuring heuristics.

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

  SeeAlso     [restrHammingD.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                                                */
/*---------------------------------------------------------------------------*/


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


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

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

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

  Synopsis [This routine implements the Fanin oriented and Fanin-Fanout
  oriented restructuring heuristics. Returns the BDD of the restructured STG.]

  Description [This routine implements the Fanin oriented and Fanin-Fanout
  oriented restructuring heuristics. Returns the BDD of the restructured STG.

  <tt>equivRel</tt> is the state equivalence relation of the
  fsm. <tt>oldTR</tt> if the state transition relation.  <tt>addPTR</tt> is the
  0-1 ADD of the augmented transition relation. <tt>possessedProbMatrix</tt> is
  the weighted graph representing the augmented transition relation. The edge
  weights are the prob. of transition of that edge. <tt>stateProbs</tt> is an
  ADD representing the steady state probabilities of the fsm. <tt>piVars</tt>
  are the BDD variables for primary inputs. <tt>heuristic</tt> takes on two
  values: RestrFanin_c and RestrFaninFanout_c.

  Please refer to "A Symbolic Algorithm for Low-Power Sequential
  Synthesis", ISLPED 97 for more details.]

  SideEffects [<tt>addPtr</tt> and <tt>possessedProbMatrix</tt> are
  dereferenced in this routine. <tt>outBdds</tt> and <tt>newInit</tt> are
  changed to reflect the restructured STG.]

  SeeAlso     [RestrMinimizeFsmByCProj RestrSelectLeastHammingDStates]
******************************************************************************/
bdd_node *
RestrMinimizeFsmByFaninFanout(
  bdd_manager *ddManager,
  bdd_node *equivRel,
  bdd_node *oldTR,
  bdd_node **addPTR,
  bdd_node **possessedProbMatrix,
  bdd_node *initBdd,
  bdd_node *reachable,
  bdd_node *stateProbs,
  bdd_node **piVars,
  bdd_node **xVars,
  bdd_node **yVars,
  bdd_node **uVars,
  bdd_node **vVars,
  int nVars,
  int nPi,
  RestructureHeuristic heuristic,
  array_t **outBdds,
  bdd_node **newInit)
{
  bdd_node *temp1, *temp2, *temp3;
  bdd_node *xCube, *yCube;
  bdd_node *Rxy,*Rxv;
  bdd_node *RxvgtRxy, *RxveqRxy; /* These are BDDs */
  bdd_node **xAddVars,**yAddVars,**vAddVars;
  bdd_node *priority, *result, *matrix;
  bdd_node *newEquivRel;
  bdd_node *oneInitState;
  bdd_node *hammingWeight;
  bdd_node *lhs, *rhs;
  bdd_node *bddCProj;
  bdd_node *bddCProjvy, *addCProjvy;
  bdd_node *newCProjvy, *newCProjux;
  bdd_node *zeroProbs, *zeroProbFactor;
  bdd_node *weight;

  array_t *newOutBdds;
  int i, index;

  /* Collect the ADD variables for futre use */
  xAddVars = ALLOC(bdd_node *,nVars);
  yAddVars = ALLOC(bdd_node *,nVars);
  vAddVars = ALLOC(bdd_node *,nVars);

  for(i = 0; i < nVars; i++) {
    index = bdd_node_read_index(yVars[i]);
    bdd_ref(yAddVars[i] = bdd_add_ith_var(ddManager,index));
    index = bdd_node_read_index(vVars[i]);
    bdd_ref(vAddVars[i] = bdd_add_ith_var(ddManager,index));
    index = bdd_node_read_index(xVars[i]);
    bdd_ref(xAddVars[i] = bdd_add_ith_var(ddManager,index));
  }

  /* Restrict the equivalence relation only to the reachable states */
  /* temp1 = R(v) */
  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,reachable,xVars,
					 vVars,nVars));
  /* temp2 = R(y) */
  bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,reachable,xVars,
					 yVars,nVars));
  /* temp3 = R(v) * R(y) */
  bdd_ref(temp3 = bdd_bdd_and(ddManager,temp1,temp2));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,temp2);
  /* newEquivRel(v,y) = E(v,y) * R(v) * R(y) */
  bdd_ref(newEquivRel = bdd_bdd_and(ddManager,equivRel,temp3));
  bdd_recursive_deref(ddManager,temp3);

  /* Select one state from the set of initial states */
  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
  bdd_ref(oneInitState);

  /* Initially an arbitrary choice of a 'nominal representative' for each
     equivalence class is made--using compatible projection--with the initial
     state as the reference vertex. bddCProj is as the name indicates, in terms
     of y and x. bddCProj refers to $\Psi(x,y)$ in the ISLPED 97 reference. */

  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,oneInitState,xVars,
					 vVars,nVars));
  bdd_recursive_deref(ddManager,oneInitState);
  bdd_ref(bddCProjvy = bdd_bdd_cprojection(ddManager, newEquivRel, temp1));
  bdd_recursive_deref(ddManager,newEquivRel);
  bdd_recursive_deref(ddManager,temp1);
  bdd_ref(bddCProj = bdd_bdd_swap_variables(ddManager,bddCProjvy,vVars,
					    xVars,nVars));
  bdd_ref(addCProjvy = bdd_bdd_to_add(ddManager,bddCProjvy));
  bdd_recursive_deref(ddManager,bddCProjvy);

  /* Let's compute the weight matrix */
  /* hammingWeight equal (nVars - HD(x,y)) */
  bdd_ref(temp1 = bdd_add_const(ddManager,(double)nVars));
  bdd_ref(temp2 = bdd_add_hamming(ddManager,xVars,yVars,nVars));
  bdd_ref(hammingWeight = bdd_add_apply(ddManager,bdd_add_minus,
					temp1,temp2));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,temp2);

  /* temp1 = possessedProbMatrix * (nVars - HD(x,y)) */
  bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_times,hammingWeight,
				*possessedProbMatrix));
  bdd_recursive_deref(ddManager,*possessedProbMatrix);

  /* matrix = possessedProbMatrix * (nVars - HD(x,y)) * stateProbs */
  bdd_ref(matrix = bdd_add_apply(ddManager,bdd_add_times,temp1,
				 stateProbs));
  bdd_recursive_deref(ddManager,temp1);

  /* Compute the contribution of the edges that have a state with zero
   * probability as its source node. The contribution is measured in terms
   * of the hamming distance between the end points of the edge.
   * The total weight on any edge is the sum of "matrix" as computed
   * above and "zeroProbFactor" as computed below.
   */
  bdd_ref(temp1 = bdd_add_bdd_strict_threshold(ddManager,stateProbs,0.0));
  bdd_ref(temp2 = bdd_not_bdd_node(temp1));
  bdd_recursive_deref(ddManager,temp1);
  /* zeroProbs evaluates to 1 for those states which have zero steady state
   * probability. zeroProbs is a 0-1 ADD.
   */
  bdd_ref(zeroProbs = bdd_bdd_to_add(ddManager,temp2));
  bdd_recursive_deref(ddManager,temp2);

  /* temp1 = (1 - HD(x,y)/nVars) */
  bdd_ref(temp2 = bdd_add_const(ddManager,(double)nVars));
  bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_divide,hammingWeight,
				temp2));
  bdd_recursive_deref(ddManager,temp2);
  bdd_recursive_deref(ddManager,hammingWeight);

  /* temp2 = (1 - HD(x,y)/nVars) * zeroProbs(x) */
  bdd_ref(temp2 = bdd_add_apply(ddManager,bdd_add_times,temp1,zeroProbs));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,zeroProbs);

  /* zeroProbFactor = (1 - HD(x,y)/nVars) * zeroProbs(x) * addPTR */
  bdd_ref(zeroProbFactor = bdd_add_apply(ddManager,bdd_add_times,
					 *addPTR,temp2));
  bdd_recursive_deref(ddManager,*addPTR);
  bdd_recursive_deref(ddManager,temp2);

  /* Total edge weight = matrix + zeroProbFactor */
  bdd_ref(weight = bdd_add_apply(ddManager,bdd_add_plus,matrix,
				 zeroProbFactor));
  bdd_recursive_deref(ddManager,matrix);
  bdd_recursive_deref(ddManager,zeroProbFactor);
    
  /* lhs = Abs(x) (weight(x,y)*CProj(v,y)) */
  bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_times,weight,
				addCProjvy));
  bdd_ref(temp3 = bdd_add_compute_cube(ddManager,xAddVars,NIL(int),nVars));
  bdd_ref(lhs = bdd_add_exist_abstract(ddManager,temp1,temp3));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,temp3);

  /* Now lhs is a function of x and y */
  bdd_ref(temp1 = bdd_add_swap_variables(ddManager,lhs,vAddVars,xAddVars,
					 nVars));
  bdd_recursive_deref(ddManager,lhs);
  lhs = temp1;

  if (heuristic == RestrFaninFanout_c) {
    /* let's compute the rhs */
    bdd_ref(temp1 = bdd_add_swap_variables(ddManager,addCProjvy,yAddVars,
					   xAddVars, nVars));
    bdd_recursive_deref(ddManager,addCProjvy);
    bdd_ref(rhs = bdd_add_apply(ddManager,bdd_add_times,weight,temp1));
    bdd_recursive_deref(ddManager,temp1);
    bdd_recursive_deref(ddManager,weight);
    temp1 = rhs;
    bdd_ref(temp3 = bdd_add_compute_cube(ddManager,yAddVars,NIL(int),nVars));
    bdd_ref(rhs = bdd_add_exist_abstract(ddManager,temp1,temp3));
    bdd_recursive_deref(ddManager,temp1);
    bdd_recursive_deref(ddManager,temp3);

    /* rhs is now a function of x and y */
    bdd_ref(temp1 = bdd_add_swap_variables(ddManager,rhs,xAddVars,
					   yAddVars,nVars));
    bdd_recursive_deref(ddManager,rhs);
    bdd_ref(rhs = bdd_add_swap_variables(ddManager,temp1,vAddVars,
					 xAddVars,nVars));
    bdd_recursive_deref(ddManager,temp1);

    /* take the average of lhs and rhs */
    bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_plus,lhs,rhs));
    bdd_recursive_deref(ddManager,lhs);
    bdd_recursive_deref(ddManager,rhs);
    bdd_ref(temp2 = bdd_add_const(ddManager,(double)2.0));
    bdd_ref(Rxy = bdd_add_apply(ddManager,bdd_add_divide,temp1,temp2));
    bdd_recursive_deref(ddManager,temp1);
    bdd_recursive_deref(ddManager,temp2);  
  }
  else {
    bdd_recursive_deref(ddManager,weight);
    bdd_recursive_deref(ddManager,addCProjvy);
    Rxy = lhs;
  }

  /* Rxv = Rxy(x,v) */
  bdd_ref(Rxv = bdd_add_swap_variables(ddManager,Rxy,yAddVars,vAddVars,
				       nVars));
  /* RxvgtRxy(x,v,y) = Rxv(x,v) > Rxy(x,y) */
  bdd_ref(temp1 = bdd_add_apply(ddManager,RestrAddMaximum,Rxv,Rxy));
  bdd_ref(RxvgtRxy = bdd_add_bdd_threshold(ddManager,temp1,(double) 1.0));
  bdd_recursive_deref(ddManager,temp1);

  /* RxveqRxy(x,v,y) = Rxz(x,v) == Rxy(x,y) */
  bdd_ref(temp1 = bdd_add_apply(ddManager,RestrAddEqual,Rxv,Rxy));
  bdd_ref(RxveqRxy = bdd_add_bdd_threshold(ddManager,temp1,(double) 1.0));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,Rxv);
  bdd_recursive_deref(ddManager,Rxy);

  /* temp1 is the tie-break function. (RxveqRxy . temp1 = temp2)*/
  bdd_ref(temp1 = bdd_dxygtdxz(ddManager,nVars,xVars,yVars,vVars));
  bdd_ref(temp2 = bdd_bdd_and(ddManager,RxveqRxy,temp1));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,RxveqRxy);

  bdd_ref(priority = bdd_bdd_or(ddManager,temp2,RxvgtRxy));
  bdd_recursive_deref(ddManager,RxvgtRxy);
  bdd_recursive_deref(ddManager,temp2);

  /* temp1 represents the pair (oldrepresentative,newprepresentative) in terms
   of x and y respectively */
  bdd_ref(temp1 = bdd_priority_select(ddManager,bddCProj,xVars,
				      yVars,vVars,priority,nVars,NULL));
  bdd_recursive_deref(ddManager,priority);

  bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
  bdd_ref(yCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars));

  /* newCProjvy is in terms of v,y */
  /* v represents the new representative of equivalent states */

  bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,yVars,vVars,
					 nVars));
  bdd_recursive_deref(ddManager,temp1);
  bdd_ref(newCProjvy = bdd_bdd_and_abstract(ddManager,bddCProj,temp2,
					    xCube));
  bdd_recursive_deref(ddManager,bddCProj);
  bdd_recursive_deref(ddManager,temp2);

  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,newCProjvy,yVars,
					 xVars,nVars));
  bdd_ref(newCProjux = bdd_bdd_swap_variables(ddManager,temp1,vVars,
					      uVars,nVars));
  bdd_recursive_deref(ddManager,temp1);

  /* Change the output functions accordingly */
  newOutBdds = array_alloc(bdd_node *,0);
  arrayForEachItem(bdd_node *,*outBdds,i,temp3) {
    bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,temp3,newCProjux,
					 xCube));
    bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,
					   nVars));
    bdd_recursive_deref(ddManager,temp1);
    bdd_recursive_deref(ddManager,temp3);
    array_insert_last(bdd_node *,newOutBdds,temp2);
  }
  array_free(*outBdds);
  *outBdds = newOutBdds;

  /* Change the initBdd accordingly */
  bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,initBdd,newCProjux,xCube));
  bdd_ref(*newInit = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,
					    nVars));
  bdd_recursive_deref(ddManager,temp1);

  /* Compute the new transition relation w.r.t the new CProjection function.
   * result = newCProjux * oldTR(x,y) * newCProjvy 
   */
  bdd_ref(temp1 = bdd_bdd_and(ddManager,xCube,yCube));
  bdd_recursive_deref(ddManager,xCube);
  bdd_recursive_deref(ddManager,yCube);
  bdd_ref(temp2 = bdd_bdd_and(ddManager,newCProjux,oldTR));
  bdd_recursive_deref(ddManager,newCProjux);
  bdd_ref(temp3 = bdd_bdd_and(ddManager,temp2,newCProjvy));
  bdd_recursive_deref(ddManager,newCProjvy);
  bdd_recursive_deref(ddManager,temp2);
  bdd_ref(result = bdd_bdd_exist_abstract(ddManager,temp3,temp1));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,temp3);

  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,result,uVars,xVars,
					 nVars));
  bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,vVars,yVars,
					 nVars));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,result);
  result = temp2;

  /* Clean up */
  for(i = 0; i < nVars; i++) {
    bdd_recursive_deref(ddManager,yAddVars[i]);
    bdd_recursive_deref(ddManager,vAddVars[i]);
    bdd_recursive_deref(ddManager,xAddVars[i]);
  }
  FREE(yAddVars);
  FREE(vAddVars);
  FREE(xAddVars);
  
  /* Return the restructred STG */
  return result;
}


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