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

  FileName    [restrCProj.c]

  PackageName [restr]

  Synopsis [This file contains functions that implement the STG restructuring
  based on compatible projection.]

  Description [This file contains functions that implement the STG
  restructuring based on compatible projection.  Please refer to "A symbolic
  algorithm for low power sequential synthesis," ISLPED 97, for more details.]

  SeeAlso     [restrHammingD.c restrFaninout.c]

  Author      [Balakrishna Kumthekar]

  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 STG restructuring based on compatible
  projection.]

  Description [This routine implements the STG restructuring based on
  compatible projection. The BDD for the monolithic transition relation of the
  restructured STG is returned.

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

  <tt>equivRel</tt> is the BDD of the equivalnece relation of the FSM,
  <tt>originalTR</tt> is the monolithic transition relation, <tt>initBdd</tt>
  is the BDD for the initial state, <tt>piVars</tt> are the BDD variables for
  primary inputs, <tt>nVars are the numbers of state variables and <tt>nPi</tt>
  are the number of primary inputs. <tt>outBdd</tt> is an array of BDDs for the
  primary outputs of the sequential circuit.]

  SideEffects [<tt>outBdds</tt> and <tt>newInit</tt> are changed to reflect the
  restructured STG.]

  SeeAlso     [RestrSelectLeastHammingDStates RestrMinimizeFsmByFaninFanout]

******************************************************************************/
bdd_node *
RestrMinimizeFsmByCProj(
  bdd_manager 	*ddManager,
  bdd_node 	*equivRel,
  bdd_node 	*originalTR,
  bdd_node 	*initBdd,
  bdd_node	**xVars,
  bdd_node	**yVars,
  bdd_node	**uVars,
  bdd_node	**vVars,
  bdd_node      **piVars,
  int		nVars,
  int           nPi,
  array_t       **outBdds,
  bdd_node      **newInit)

{
  bdd_node *resultYV, *temp, *temp1, *temp2;
  bdd_node *result, *resultXU;
  bdd_node *xCube, *yCube;
  bdd_node *oneInitState;
  array_t *newOutBdds;
  int i;

  /* Select one state from the set of initial states. This is redundant in case
     of circuits described in blif format.*/
  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
  bdd_ref(oneInitState);

  temp = bdd_bdd_swap_variables(ddManager,oneInitState,xVars,vVars,nVars);
  bdd_ref(temp);
  bdd_recursive_deref(ddManager,oneInitState);

  /* Select a representative for each equivalence class. The vVars encode the
   * representative for each class. resultYV has yVars and vVars in its
   * support. equivRel is a function of yVars and vVars.
   */
  resultYV = bdd_bdd_cprojection(ddManager, equivRel, temp);
  bdd_ref(resultYV);
  bdd_recursive_deref(ddManager,temp);

  temp = bdd_bdd_swap_variables(ddManager,resultYV,yVars,xVars,nVars);
  bdd_ref(temp);
  resultXU = bdd_bdd_swap_variables(ddManager,temp,vVars,uVars,nVars);
  bdd_ref(resultXU);
  bdd_recursive_deref(ddManager, temp);

  /* Change the initBdd accordingly
   * initBdd^{new} = [\exists_x (initBdd(x) * result(x,u))]_{u=x}
   */
  xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars);
  bdd_ref(xCube);
  bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,initBdd,resultXU,
				       xCube));
  bdd_ref(*newInit = bdd_bdd_swap_variables(ddManager,temp1,uVars,
					    xVars,nVars));
  bdd_recursive_deref(ddManager,temp1);

  /* compute the new TR.
   * TR^{new}(x,w,y) = 
   *    [\exists_{xy}(result(x,u) * TR(x,w,y) * result(y,v))]_{u=x,v=y}
   * result is the new restructured/minimized TR.
   */
  bdd_ref(yCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars));
  bdd_ref(temp = bdd_bdd_and_abstract(ddManager,resultYV,originalTR,yCube));
  bdd_recursive_deref(ddManager,resultYV);
  bdd_recursive_deref(ddManager,yCube);

  bdd_ref(result = bdd_bdd_and_abstract(ddManager,temp,resultXU,xCube));
  bdd_recursive_deref(ddManager,temp);

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

  /* Change the outputs accordingly
   * lambda^{new}_i(x,w) = [\exists_x (lambda_i(x,w) * result(x,u))]_{u=x}
   *
   * lambda_i(x,w) is the ith primary output.
   */
  newOutBdds = array_alloc(bdd_node *,0);
  arrayForEachItem(bdd_node *,*outBdds,i,temp) {
    temp1 = bdd_bdd_and_abstract(ddManager,temp,resultXU,xCube);
    bdd_ref(temp1);
    temp2 = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,nVars);
    bdd_ref(temp2);
    bdd_recursive_deref(ddManager,temp1);
    array_insert_last(bdd_node *,newOutBdds,temp2);
  }
  bdd_recursive_deref(ddManager, xCube);
  bdd_recursive_deref(ddManager,resultXU);

#ifdef RESTR_DIAG
  {
    int flag1,flag2;

    (void) fprintf(vis_stdout,"Old transition relation ...\n");
    flag1 = RestrTestIsDeterministic(ddManager,originalTR,initBdd,
				     xVars,yVars,nVars);
    (void) fprintf(vis_stdout,"New transition relation ...\n");
    flag2 = RestrTestIsDeterministic(ddManager,result,*newInit,
				     xVars,yVars,nVars);
  }
#endif
  
  /* Delete the old array */
  arrayForEachItem(bdd_node *,*outBdds,i,temp) {
    bdd_recursive_deref(ddManager,temp);
  }
  array_free(*outBdds);
  *outBdds = newOutBdds;
  
  return result;

}

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