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

  FileName    [spfdSpfd.c]

  PackageName [spfd]

  Synopsis [Routines to perform SPFD computation.]

  Description [Routines to perform SPFD computation.]

  SeeAlso     [spfdProg.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 "spfdInt.h"

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


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


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


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


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


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

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

static bdd_node * ComputeAuxRel(SpfdApplData_t *applData, bdd_node *faninRel, Ntk_Node_t *from, int piSwap);

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


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


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

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

  Synopsis [Given two functions represented by bdd1 and bdd0, compute
  its SPFD.]

  SideEffects [None]

******************************************************************************/
bdd_node *
SpfdNodeComputeSpfdFromOnAndOffSet(
  SpfdApplData_t *applData,
  Ntk_Node_t *regNode,
  bdd_node *bdd1,
  bdd_node *bdd0)
{
  bdd_manager *ddManager = applData->ddManager;
  int numFanin = Ntk_NodeReadNumFanins(regNode);
  bdd_node **yVars,**yAuxVars;
  bdd_node *ddTemp,*rel,*spfd;
  Ntk_Node_t *fanin;
  int j,clean;

  /* If bdd1 and bdd0 are not specified, replace bdd1 and bdd0 by the
     node's local ON-set and OFF-set respectively */
  clean = 0;
  if (bdd1 == NIL(bdd_node) ||
      bdd0 == NIL(bdd_node)) {
    Ntk_Network_t *network;
    network = Ntk_NodeReadNetwork(regNode);
    bdd_ref(bdd1 = SpfdNodeReadLocalBdd(network,regNode));
    bdd_ref(bdd0 = bdd_not_bdd_node(bdd1));
    /* Delete bdd1 and bdd0 at the end.*/
    clean = 1;
  }
  
  /* Array of variables for swapping */
  numFanin = Ntk_NodeReadNumFanins(regNode);
  yVars = ALLOC(bdd_node *,numFanin);
  yAuxVars = ALLOC(bdd_node *,numFanin);
  Ntk_NodeForEachFanin(regNode,j,fanin) {
    yVars[j] = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
    yAuxVars[j] = bdd_bdd_ith_var(ddManager,
				  SpfdNodeReadAuxId(applData,fanin));
  }

  /* spfd is bdd1(y) * bdd0(y') + bdd1(y') * bdd0(y) */
  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,bdd0,
					  yVars,yAuxVars,numFanin));
  bdd_ref(rel = bdd_bdd_and(ddManager,bdd1,ddTemp));
  bdd_recursive_deref(ddManager,ddTemp);
      
  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,rel,
					  yVars,yAuxVars,numFanin));
  bdd_ref(spfd = bdd_bdd_or(ddManager,rel,ddTemp));
  bdd_recursive_deref(ddManager,rel);
  bdd_recursive_deref(ddManager,ddTemp);
  FREE(yVars);
  FREE(yAuxVars);

  if (clean) {
    bdd_recursive_deref(ddManager,bdd1);
    bdd_recursive_deref(ddManager,bdd0);
  }
  return spfd;
} /* End of SpfdNodeComputeSpfdFromOnAndOffSet */


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

  Synopsis [Compute the SPFD of 'from', as the union of SPFDs of its
  fanout wires.]

  SideEffects [None]

******************************************************************************/
bdd_node *
SpfdNodeComputeSpfdFromFanouts(
  SpfdApplData_t *applData,
  Ntk_Node_t *from)
{
  bdd_manager *ddManager = applData->ddManager;
  st_table *currBddReq;
  st_table *wireTable,*wiresRemoved;
  array_t *ordArray;
  bdd_node *result,*var,*varAux,*ddTemp,*ddTemp2;
  bdd_node *wireSpfd,*toSpfd,*fromSpfd,*xCube;
  bdd_node *step1,*faninRel,*faninRelAux,*inter,*final;
  bdd_node **firstCompose,**secondCompose;
  bdd_node *logicZero;
  Ntk_Node_t *fanin,*to;
  int index,i,j;
  int size,piSwap;


  if (Ntk_NodeReadNumFanouts(from) < 1) {
    (void) fprintf(vis_stdout,
		   "** spfd error: Node %s has no fanouts.\n",
		   Ntk_NodeReadName(from));
    return NIL(bdd_node);
  }
  currBddReq = applData->currBddReq;
  xCube = applData->currXCube;
  logicZero = bdd_read_logic_zero(ddManager);

  /* Compute the characteristic function of the fanin relation:
   faninRel = \prod y_i == f_i(X) */
  faninRel = SpfdComputeNodeArrayRelation(applData,currBddReq,NIL(array_t),
					  Ntk_NodeReadFanins(from),
					  TRUE,&piSwap);
  
  /* Convert faninRel(y,pi) to faninRel(\hat{y},pi) */
  faninRelAux = ComputeAuxRel(applData,faninRel,from,piSwap);
    
  /* Compute SPFD wire by wire according to the order specified for
     each fanout node. */
  wireTable = applData->currWireTable;
  wiresRemoved = applData->wiresRemoved;
  bdd_ref(fromSpfd = logicZero);
  Ntk_NodeForEachFanout(from,j,to) {

    bdd_ref(result = bdd_read_one(ddManager));
    ordArray = SpfdNodeReadFaninOrder(applData,to);
    arrayForEachItem(Ntk_Node_t *,ordArray,i,fanin) {
      var = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
      index = SpfdNodeReadAuxId(applData,fanin);
      varAux = bdd_bdd_ith_var(ddManager,index);
	
      if (fanin != from) {
	/* XNOR */
	bdd_ref(ddTemp = bdd_bdd_xnor(ddManager,var,varAux));
      } else {
	/* XOR */
	bdd_ref(ddTemp = bdd_bdd_xor(ddManager,var,varAux));
      }
      bdd_ref(ddTemp2 = bdd_bdd_and(ddManager,result,ddTemp));
      bdd_recursive_deref(ddManager,result);
      bdd_recursive_deref(ddManager,ddTemp);
      result = ddTemp2;
	
      if (fanin == from)
	break;
    }
      
    /* Compute AND of result and the SPFD of 'to'. */
    toSpfd = SpfdNodeReadSpfd(applData,to);
    if (toSpfd == NIL(bdd_node)) {
      (void) fprintf(vis_stderr,
		     "** spfd error: Spfd expected but not found.\n");
      (void) fprintf(vis_stderr, "To node:\n");
      Ntk_NodePrint(vis_stderr, to, TRUE, TRUE);
      (void) fprintf(vis_stderr, "From node:\n");
      Ntk_NodePrint(vis_stderr, from, TRUE, TRUE);
      fflush(vis_stderr);
      assert(0);
    }
    bdd_ref(wireSpfd = bdd_bdd_and(ddManager,toSpfd,result));
    bdd_recursive_deref(ddManager,result);

    /* Convert wireSpfd from fanout space to fanin space */
    /* Prepare the vectors for composition */
    size = bdd_num_vars(ddManager);
    firstCompose = ALLOC(bdd_node *,size);
    secondCompose = ALLOC(bdd_node *,size);
    for (i = 0; i < size; i++) {
      firstCompose[i] = bdd_bdd_ith_var(ddManager,i);
      secondCompose[i] = bdd_bdd_ith_var(ddManager,i);
    }
      
    arrayForEachItem(Ntk_Node_t *,ordArray,i,fanin) {
      int id,auxId;
	
      id = Ntk_NodeReadMddId(fanin);
      auxId = SpfdNodeReadAuxId(applData,fanin);
      st_lookup(currBddReq,(char *)fanin,(char **)&firstCompose[id]);
      secondCompose[auxId] = firstCompose[id];
    }
      
    /* Perform the steps of compose --> existential abstraction twice */
    bdd_ref(step1 = bdd_bdd_vector_compose(ddManager,wireSpfd,firstCompose));
    bdd_recursive_deref(ddManager,wireSpfd);
    FREE(firstCompose);
    bdd_ref(inter = bdd_bdd_and_abstract(ddManager,faninRel,step1,xCube));
    bdd_recursive_deref(ddManager,step1);
    
    /* The second of compose --> existential abstraction steps */
    bdd_ref(ddTemp = bdd_bdd_vector_compose(ddManager,inter,secondCompose));
    bdd_recursive_deref(ddManager,inter);
    FREE(secondCompose);
    bdd_ref(final = bdd_bdd_and_abstract(ddManager,faninRelAux,
					 ddTemp,xCube));
    bdd_recursive_deref(ddManager,ddTemp);

    /* Now 'final' is in the fanin space */
    if (final == logicZero) {
      st_table *sinkTable;
      Ntk_Node_t *tempNode;
      boolean add;

      /* Check if this wire has already been removed. If yes, skip */
      add = TRUE;
      if (st_lookup(wiresRemoved,(char *)from,&sinkTable) &&
	  st_lookup(sinkTable,(char *)to,&tempNode)) {
	add = FALSE;
      }

      if (add) {
        if (spfdVerbose > 2)
	  (void) fprintf(vis_stdout,
			 "** spfd info: wire %s --> %s has empty spfd.\n",
			 Ntk_NodeReadName(from),Ntk_NodeReadName(to));
	
	/* Add to the wireTable */
	if (st_lookup(wireTable,(char *)from,&sinkTable)) {
	  st_insert(sinkTable,(char *)to,(char *)to);
	} else {
	  sinkTable = st_init_table(st_ptrcmp,st_ptrhash);
	  st_insert(sinkTable,(char *)to,(char *)to);
	  st_insert(wireTable,(char *)from,(char *)sinkTable);
	}
      }
    }
    
    bdd_ref(ddTemp = bdd_bdd_or(ddManager,fromSpfd,final));
    bdd_recursive_deref(ddManager,fromSpfd);
    bdd_recursive_deref(ddManager,final);
    
    fromSpfd = ddTemp;
  }
  bdd_recursive_deref(ddManager,faninRel);
  bdd_recursive_deref(ddManager,faninRelAux);
    
  /* Swap variables for fromSpfd if necessary */
  if (piSwap) { /* If we have used alternate PI ids */
    ddTemp = SpfdSwapPiAndAltPi(applData,fromSpfd);
    bdd_recursive_deref(ddManager,fromSpfd);
    fromSpfd = ddTemp;
  }
  
  return fromSpfd;
  
} /* End of SpfdNodeComputeSpfdFromFanouts */


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

  Synopsis [Compute the strongly connected components in the SPFD of
  regNode. 'tempVars' are extra variables required during this
  computation. For detailed description please refer to:

  Subarnarekha Sinha and Robert K. Brayton. Implementation and use of
  SPFDs in optimizaing Boolean networks. In International Conference
  on Computer Aided Design, 1998.]

  SideEffects [None]

******************************************************************************/
st_table *
SpfdNodeComputeSCCs(
  SpfdApplData_t *applData,
  Ntk_Node_t *regNode,
  bdd_node **tempVars)
{
  bdd_manager *ddManager = applData->ddManager;
  st_table *inUseVars = applData->currInUseVars;
  Ntk_Node_t *fanin;
  st_table *SCC;
  bdd_node *spfd,*spfd2,*auxCube;
  bdd_node *ddTemp1,*ddTemp2,*logicZero,*faninCube;
  bdd_node *Ny,*E1y,*E0y;
  bdd_node *from,*To,*new_,*reached;
  bdd_node **faninVars,**auxVars;
  int i,numFanin,varsAllocated;

  numFanin = Ntk_NodeReadNumFanins(regNode);
  SCC = st_init_table(st_ptrcmp,st_ptrhash);
  spfd = SpfdNodeReadSpfd(applData,regNode);
  logicZero = bdd_read_logic_zero(ddManager);

  if (spfd == logicZero)
    return SCC;
  
  varsAllocated = 0;
  /* Allocate variables if necessary */
  if (tempVars == NIL(bdd_node *)) {
    tempVars = SpfdAllocateTemporaryVariables(ddManager,inUseVars,numFanin);
    varsAllocated = 1;
  }
  
  faninVars = ALLOC(bdd_node *,numFanin);
  auxVars = ALLOC(bdd_node *,numFanin);
  Ntk_NodeForEachFanin(regNode,i,fanin) {
    faninVars[i] = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
    auxVars[i] = bdd_bdd_ith_var(ddManager,
				 SpfdNodeReadAuxId(applData,fanin));
  }

  bdd_ref(auxCube = bdd_bdd_compute_cube(ddManager,auxVars,
					 NIL(int),numFanin));
  /* Compute spfd2 = \exists_{\hat{y}} spfd(y,\hat{y}) *
     spfd(\hat{y},\tilde{y}) */
  bdd_ref(ddTemp1 = bdd_bdd_swap_variables(ddManager,spfd,faninVars,
					   auxVars,numFanin));
  bdd_ref(ddTemp2 = bdd_bdd_swap_variables(ddManager,ddTemp1,faninVars,
					   tempVars,numFanin));
  bdd_recursive_deref(ddManager,ddTemp1);
  bdd_ref(spfd2 = bdd_bdd_and_abstract(ddManager,spfd,ddTemp2,auxCube));
  bdd_recursive_deref(ddManager,ddTemp2);

  /* SCC computation */
  bdd_ref(faninCube = bdd_bdd_compute_cube(ddManager,faninVars,
					   NIL(int),numFanin));
  /* Compute N(y) = \exists_{\hat{y}} spfd(y,\hat{y}) */
  bdd_ref(Ny = bdd_bdd_exist_abstract(ddManager,spfd,auxCube));
  bdd_recursive_deref(ddManager,auxCube);

  while (Ny != logicZero) {
    /* To compute E1(y) perform the fixpoint image computation */
    bdd_ref(from = bdd_bdd_pick_one_minterm(ddManager,Ny,faninVars,numFanin));
    bdd_ref(reached = from);
    do {
      bdd_ref(ddTemp1 = bdd_bdd_and_abstract(ddManager,spfd2,from,faninCube));
      bdd_recursive_deref(ddManager,from);
      bdd_ref(To = bdd_bdd_swap_variables(ddManager,ddTemp1,tempVars,
					  faninVars,numFanin));
      bdd_recursive_deref(ddManager,ddTemp1);
      bdd_ref(new_ = bdd_bdd_and(ddManager,To,bdd_not_bdd_node(reached)));
      bdd_recursive_deref(ddManager,To);
      bdd_ref(ddTemp1 = bdd_bdd_or(ddManager,reached,new_));
      bdd_recursive_deref(ddManager,reached);
      reached = ddTemp1;
      from = new_;
    } while (new_ != logicZero);

    E1y = reached;
    
    /* E_0(y) = \exists_{\hat{y}} spfd(y,\hat{y}) * E_1(y) */
    bdd_ref(ddTemp1 = bdd_bdd_and_abstract(ddManager,spfd,E1y,faninCube));
    bdd_ref(E0y = bdd_bdd_swap_variables(ddManager,ddTemp1,auxVars,
					 faninVars,numFanin));
    bdd_recursive_deref(ddManager,ddTemp1);
    
    /* Update Ny: Ny = Ny * (E1y + E0y)' */
    bdd_ref(ddTemp1 = bdd_bdd_or(ddManager,E1y,E0y));
    bdd_ref(ddTemp2 = bdd_bdd_and(ddManager,Ny,bdd_not_bdd_node(ddTemp1)));
    bdd_recursive_deref(ddManager,ddTemp1);
    bdd_recursive_deref(ddManager,Ny);
    Ny = ddTemp2;

    /* Store E1y and E0y in an st_table */
    st_insert(SCC,(char *)E1y,(char *)E0y);
  }
  bdd_recursive_deref(ddManager,faninCube);
  bdd_recursive_deref(ddManager,Ny);
  
  FREE(auxVars);
  FREE(faninVars);

  if (varsAllocated) {
    long id;
    for (i = 0; i < numFanin; i++) {
      id = (long) bdd_node_read_index(tempVars[i]);
      st_delete(inUseVars,&id,NIL(char *));
    }
    FREE(tempVars);
  }
  
  return SCC;

} /* End of SpfdNodeComputeSCCs */

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

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

  Synopsis [Convert faninRel which is interms of Y, to Y', the
  auxillary variables.]

  SideEffects [None]

******************************************************************************/
static bdd_node *
ComputeAuxRel(
  SpfdApplData_t *applData,
  bdd_node *faninRel,
  Ntk_Node_t *from,
  int piSwap)
{
  bdd_node **fromVars,**toVars;
  int numFi = Ntk_NodeReadNumFanins(from);
  int k,altId;
  Ntk_Node_t *fanin;
  bdd_node *faninRelAux;
  st_table *piAltVars;
  bdd_manager *ddManager = applData->ddManager;
  
  piAltVars = applData->currPiAltVars;
  
  /* Collect variables for swapping. */
  fromVars = ALLOC(bdd_node *,numFi);
  toVars = ALLOC(bdd_node *,numFi);
  Ntk_NodeForEachFanin(from,k,fanin) {
    int id = Ntk_NodeReadMddId(fanin);
    if (piSwap && st_lookup(piAltVars,(char *)(long)id,&altId)) {
      fromVars[k] = bdd_bdd_ith_var(ddManager,altId);
    } else {
      fromVars[k] = bdd_bdd_ith_var(ddManager,id);
    }
    toVars[k] = bdd_bdd_ith_var(ddManager,SpfdNodeReadAuxId(applData,fanin));
  }
  bdd_ref(faninRelAux = bdd_bdd_swap_variables(ddManager,faninRel,fromVars,
					       toVars,numFi));
  FREE(fromVars);
  FREE(toVars);

  return faninRelAux;
  
} /* End of ComputeAuxRel */