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

 FileName    [restrUtil.c]

 PackageName [restr]

 Synopsis    [Support functions used in the package.]

 Description [Support functions used in the package.]

 SeeAlso     [restrDebug.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 [Returns the primary output node array for the given network.]

  Description [Returns the primary output node array for the given network.]

  SideEffects [None]

  SeeAlso     [RestrGetNextStateArray]

******************************************************************************/
array_t *
RestrGetOutputArray(Ntk_Network_t *network)
{
    lsGen		 gen;
    Ntk_Node_t	*node;
    array_t	*outputArray;

    outputArray = array_alloc(char *, 0);
    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
	array_insert_last(char *, outputArray, Ntk_NodeReadName(node));
    }

    return outputArray;
}

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

  Synopsis [Computes the product 
  \prod_{i=0}^{i=n-1} funArray_{i}(x) \equiv funArray_{i}(y)]

  Description [Computes the product 
  \prod_{i=0}^{i=n-1} funArray_{i}(x) \equiv funArray_{i}(y).
  
  funArray is an array of BDDs and each has xVars in its
  support. nVars is the number of xVars and yVars.]

  SideEffects [None]

  SeeAlso     [RestrComputeTRWithIds]

******************************************************************************/
bdd_node *
RestrCreateProductOutput(
  bdd_manager	*ddManager,
  array_t	*funArray,
  bdd_node	**xVars,
  bdd_node	**yVars,
  int		nVars)
{
  bdd_node	*ddtemp, *ddtemp1;
  bdd_node	*fn, *result;
  int 		i, num = array_n(funArray);

  bdd_ref(result = bdd_read_one(ddManager));

  for(i = 0; i < num; i++) {

    ddtemp = array_fetch(bdd_node *, funArray, i);;

    ddtemp1 = bdd_bdd_swap_variables(ddManager,ddtemp,xVars,yVars,nVars);
    bdd_ref(ddtemp1);
    fn = bdd_bdd_xnor(ddManager,ddtemp1,ddtemp);
    bdd_ref(fn);
    bdd_recursive_deref(ddManager,ddtemp1);
    ddtemp1 = bdd_bdd_and(ddManager,result,fn);
    bdd_ref(ddtemp1);
    bdd_recursive_deref(ddManager,fn);
    bdd_recursive_deref(ddManager,result);
    result = ddtemp1;
  }

  return result;
}

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

  Synopsis [The function computes the following relations:
  \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) and 
  \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) \wedge (v_i \equiv f_i(u)) and 
  returns them in an array.]

  Description [The function computes the following relations:
  \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) and 
  \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) \wedge (v_i \equiv f_i(u)) and 
  returns them in an array.
  
  nextBdds is an array of nVar BDDs and has xVars in its
  support. xVars, yVars, uVars and vVars are arrays of BDD variables.]

  SideEffects [None]

  SeeAlso     [RestrCreateProductOutput]

******************************************************************************/
array_t *
RestrComputeTRWithIds(
  bdd_manager	*ddManager,
  array_t	*nextBdds,
  bdd_node	**xVars,
  bdd_node	**yVars,
  bdd_node	**uVars,
  bdd_node	**vVars,
  int		nVars)
{
  bdd_node	*ddtemp1, *ddtemp2;
  bdd_node	*oldTR, *fn;
  array_t 	*composite;
  int 		 i;


  /* First compute oldTR(x,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) */
  bdd_ref(oldTR = bdd_read_one(ddManager));

  for(i = 0; i < nVars; i++) {
    ddtemp2  = array_fetch(bdd_node *, nextBdds, i);

    fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
    bdd_ref(fn);
    ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
    bdd_ref(ddtemp1);
    bdd_recursive_deref(ddManager,fn);
    bdd_recursive_deref(ddManager,oldTR);
    oldTR = ddtemp1;
  }
  
  /* fn(u,v) = oldTR(x-->u,y-->v) */
  ddtemp2 = bdd_bdd_swap_variables(ddManager,oldTR,xVars,uVars,nVars);
  bdd_ref(ddtemp2);
  fn = bdd_bdd_swap_variables(ddManager,ddtemp2,yVars,vVars,nVars);
  bdd_ref(fn);
  bdd_recursive_deref(ddManager,ddtemp2);
  ddtemp1 = bdd_bdd_and(ddManager,fn,oldTR);
  bdd_ref(ddtemp1);
  bdd_recursive_deref(ddManager,fn);

  /* Return both the relations */
  composite = array_alloc(bdd_node *,0);
  array_insert_last(bdd_node *,composite,oldTR);
  array_insert_last(bdd_node *,composite,ddtemp1);

  return composite;
}

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

  Synopsis [This function returns the state equivalence relation for an FSM.]

  Description [This function returns the state equivalence relation
  for an FSM. Lambda is the primary output relation and TR is the
  state transition relation of the product machine. Lambda has xVars,
  uVars and piVars in its support. TR has piVars, xVars,yVars,uVars
  and vVars in its support. nPi is the number of piVars and nVars is
  the number of xVars. xVars, yVars, uVars and vVars are all of the
  same size, i.e., nVars. The returned BDD is a function of xVars and
  uVars.

  For more information on the algorithm, please refer to "Dont care
  minimization of multi-level sequential logic networks", ICCAD 90.]

  SideEffects [None]

  SeeAlso     [RestrComputeEquivRelationUsingCofactors]

******************************************************************************/
bdd_node *
RestrGetEquivRelation(
  bdd_manager   	*mgr,
  bdd_node        *Lambda,
  bdd_node        *tranRelation,
  bdd_node	**xVars,
  bdd_node	**yVars,
  bdd_node	**uVars,
  bdd_node	**vVars,
  bdd_node	**piVars,
  int		  nVars,
  int		  nPi,
  boolean restrVerbose)

{
    bdd_node *initialEsp, *espK;
    bdd_node *espKPlusOne;
    bdd_node *inputCube, *nextCube;
    bdd_node **allPreVars, **allNexVars;
    bdd_node *temp;
    int i,depth;

    allPreVars = ALLOC(bdd_node *, 2*nVars);
    allNexVars = ALLOC(bdd_node *, 2*nVars);
    for(i = 0; i < nVars;i++) {
	allPreVars[i] = xVars[i];
	allNexVars[i] = yVars[i];
    } 
    for(i = 0; i < nVars;i++) {
	allPreVars[i+nVars] = uVars[i];
	allNexVars[i+nVars] = vVars[i];
    } 

    nextCube = bdd_bdd_compute_cube(mgr,allNexVars,NIL(int),2*nVars);
    bdd_ref(nextCube);

    inputCube = bdd_bdd_compute_cube(mgr,piVars,NIL(int),nPi);
    bdd_ref(inputCube);

    initialEsp = bdd_bdd_univ_abstract(mgr,Lambda,inputCube);
    bdd_ref(initialEsp);

    espK = bdd_bdd_swap_variables(mgr,initialEsp,allPreVars,
				 allNexVars,2*nVars);
    bdd_ref(espK);
    
    depth = 0;
    do {
	bdd_node *image, *temp1;
	image = bdd_bdd_and_abstract(mgr,tranRelation, espK, nextCube);
	bdd_ref(image);

	temp1 = bdd_bdd_univ_abstract(mgr,image,inputCube);
	bdd_ref(temp1);
	bdd_recursive_deref(mgr,image);

	espKPlusOne = bdd_bdd_and(mgr,temp1,initialEsp);
	bdd_ref(espKPlusOne);
	bdd_recursive_deref(mgr,temp1);
	temp1 = bdd_bdd_swap_variables(mgr,espKPlusOne,allPreVars,
				     allNexVars,2*nVars);
	bdd_ref(temp1);
	bdd_recursive_deref(mgr,espKPlusOne);
	espKPlusOne = temp1;
	
	if (espKPlusOne == espK) {
	  break;
	}
	bdd_recursive_deref(mgr,espK);
	espK = espKPlusOne;
	depth++;
    } while (1);

    if (restrVerbose)
      (void) fprintf(vis_stdout,"** restr info: EQ. relation computation depth = %d\n",
		     depth);

    bdd_recursive_deref(mgr,espKPlusOne);
    bdd_recursive_deref(mgr,initialEsp);
    bdd_recursive_deref(mgr,inputCube);
    bdd_recursive_deref(mgr,nextCube);

    bdd_ref(temp = bdd_bdd_swap_variables(mgr,espK,allNexVars,
					  allPreVars,2*nVars));
    bdd_recursive_deref(mgr,espK);
    espK = temp;

    FREE(allPreVars);
    FREE(allNexVars);

    return espK;
}

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

  Synopsis [This function returns the state equivalence relation for an FSM.]

  Description [This function returns the state equivalence relation
  for an FSM. Lambda is the primary output relation and TR is the
  state transition relation of the product machine. Lambda has xVars,
  uVars and piVars in its support. TR has piVars, xVars,yVars,uVars
  and vVars in its support. nPi is the number of piVars and nVars is
  the number of xVars. xVars, yVars, uVars and vVars are all of the
  same size, i.e., nVars. The returned BDD is a function of xVars and
  uVars.

  For more information on the algorithm, please refer to "Extending Equivalence
  Class Computation to Large FSMs", ICCD 96.]

  SideEffects []

  SeeAlso     [RestrGetEquivRelation]

******************************************************************************/
bdd_node *
RestrComputeEquivRelationUsingCofactors(
  bdd_manager  	*mgr,
  bdd_node      *Lambda,
  bdd_node      *TR,
  bdd_node	**xVars,
  bdd_node	**yVars,
  bdd_node	**uVars,
  bdd_node	**vVars,
  bdd_node	**piVars,
  int		  nVars,
  int		  nPi,
  boolean         restrVerbose)

{
  bdd_node *espKxu, *espKyv, *espKPlusOne, *espKMinusOne;
  bdd_node *espKCofKMinusOne;
  bdd_node *inputCube, *nextCube;
  bdd_node *tranRelation;
  bdd_node *newTran;
  bdd_node **allPreVars, **allNexVars;
  int i,depth;

  bdd_ref(tranRelation = TR);

  allPreVars = ALLOC(bdd_node *, 2*nVars);
  allNexVars = ALLOC(bdd_node *, 2*nVars);
  for(i = 0; i < nVars;i++) {
    allPreVars[i] = xVars[i];
    allNexVars[i] = yVars[i];
  } 
  for(i = 0; i < nVars;i++) {
    allPreVars[i+nVars] = uVars[i];
    allNexVars[i+nVars] = vVars[i];
  } 

  /* nextCube is a cube of yVars and vVars */
  nextCube = bdd_bdd_compute_cube(mgr,allNexVars,NIL(int),2*nVars);
  bdd_ref(nextCube);

  /* inputCube is a cube of piVars */
  inputCube = bdd_bdd_compute_cube(mgr,piVars,NIL(int),nPi);
  bdd_ref(inputCube);

  /* espKxu = \forall_{piVars} Lambda */
  espKxu = bdd_bdd_univ_abstract(mgr,Lambda,inputCube);
  bdd_ref(espKxu);

  espKyv = bdd_bdd_swap_variables(mgr,espKxu,allPreVars,
				  allNexVars,2*nVars);
  bdd_ref(espKyv);
  bdd_ref(espKMinusOne = bdd_read_one(mgr));
  bdd_ref(espKPlusOne = bdd_read_one(mgr));

  /* The following loop is essentially the following:
   * E_{k+1} = E_k \wedge (\forall_x(func)) where
   * func = \exists_{yv} ((TR \downarrow E_k) \wedge (E_k \downarrow E_{k-1}))
   */
  depth = 0;
  while (1) {
    bdd_node *image, *temp1;
	
    bdd_recursive_deref(mgr, espKPlusOne);
    bdd_ref(espKCofKMinusOne = bdd_bdd_constrain(mgr, espKyv, 
						 espKMinusOne));
    bdd_recursive_deref(mgr, espKMinusOne);
    bdd_ref(espKMinusOne = espKyv);

    bdd_ref(newTran = bdd_bdd_constrain(mgr, tranRelation, espKxu));

    image = bdd_bdd_and_abstract(mgr,newTran, espKCofKMinusOne, nextCube);
    bdd_ref(image);
    bdd_recursive_deref(mgr, newTran);
    bdd_recursive_deref(mgr, espKCofKMinusOne);

    temp1 = bdd_bdd_univ_abstract(mgr,image,inputCube);
    bdd_ref(temp1);
    bdd_recursive_deref(mgr,image);
    espKPlusOne = bdd_bdd_and(mgr,temp1,espKxu);
    bdd_ref(espKPlusOne);
    bdd_recursive_deref(mgr,temp1);

    if (espKPlusOne == espKxu) {
      bdd_recursive_deref(mgr,espKMinusOne);
      bdd_recursive_deref(mgr,espKxu);
      bdd_recursive_deref(mgr,espKyv);
      bdd_recursive_deref(mgr,tranRelation);
      bdd_recursive_deref(mgr,inputCube);
      bdd_recursive_deref(mgr,nextCube);
      FREE(allPreVars);
      FREE(allNexVars);
      if (restrVerbose) {
	(void) fprintf(vis_stdout,"** restr info: EQ. relation computation depth = %d\n",
		       depth);
      }
      return espKPlusOne;
    }

    bdd_recursive_deref(mgr, espKxu);
    bdd_ref(espKxu = espKPlusOne);
    bdd_recursive_deref(mgr, espKyv);
    espKyv = bdd_bdd_swap_variables(mgr,espKxu,allPreVars,
				    allNexVars,2*nVars);
    bdd_ref(espKyv);
	
    depth++;
  }

}

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

  Synopsis [Returns the BDD for the augmented tr.]

  Description [Returns the BDD for the augmented tr. The procedure of
  augmentation is as follows: If there exists a pair (x,y) in tr and a
  pair (y,v) in equivRelation, then the augmented tr has an additional
  pair (x,v) added to it. The newly added edges are called 'ghost
  edges'. Moreover, tr is a function of xVars and yVars, while
  equivRelation is a function of yVars and vVars. nVars is the size of
  yVars and vVars each. The returned BDD has the same support
  variables as tr.

  The boolean formulation is:

  T^a(x,y) = \exists_z E(y,z) \wedge T(x,z)]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
bdd_node *
RestrComputeTrWithGhostEdges(
  bdd_manager *mgr,
  bdd_node **yVars,
  bdd_node **vVars,
  bdd_node *tr,
  bdd_node *equivRelation,
  int nVars)
{
  bdd_node *abstractCube;
  bdd_node *temp;
  bdd_node *ghostTR;

  abstractCube = bdd_bdd_compute_cube(mgr,yVars,NIL(int),nVars);
  bdd_ref(abstractCube);

  temp = bdd_bdd_and_abstract(mgr,tr,equivRelation,abstractCube);
  bdd_ref(temp);
  bdd_recursive_deref(mgr,abstractCube);

  ghostTR = bdd_bdd_swap_variables(mgr,temp,vVars,yVars,nVars);
  bdd_ref(ghostTR);
  bdd_recursive_deref(mgr,temp);

  return ghostTR;
}

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

  Synopsis [Returns a 0-1 ADD containing minterms such that the
  discriminant for those minterms in f is greater than that in g.]

  Description [Returns a 0-1 ADD containing minterms such that the
  discriminant for those minterms in f is greater than that in g.]

  SideEffects [None]

  SeeAlso     [cuddAddApply.c]
******************************************************************************/
bdd_node *
RestrAddMaximum(
  bdd_manager *ddManager,
  bdd_node **f,
  bdd_node **g)
{
  bdd_node *plusInf;
  bdd_node *zero, *one;

  zero = bdd_read_zero(ddManager);
  one = bdd_read_one(ddManager);
  plusInf = bdd_read_plus_infinity(ddManager);

  if(*g == plusInf) {
    return zero;
  }

  if(bdd_is_constant(*f) && bdd_is_constant(*g)) {
    if(bdd_add_value(*f) > bdd_add_value(*g)) {
      return one;
    } else {
      return zero;
    }
  }
  return NULL;
}


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

  Synopsis [Returns a 0-1 ADD containing minterms such that the
  discriminant for those minterms in f is equal to that in g.]

  Description [Returns a 0-1 ADD containing minterms such that the
  discriminant for those minterms in f is equal to that in g.]

  SideEffects [None]

  SeeAlso     [cuddAddApply.c]

******************************************************************************/
bdd_node *
RestrAddEqual(
  bdd_manager *ddManager,
  bdd_node **f,
  bdd_node **g)
{
  bdd_node *zero, *one;

  zero = bdd_read_zero(ddManager);
  one = bdd_read_one(ddManager);

  if(*f == *g) {
    return one;
  }

  if(bdd_is_constant(*f) && bdd_is_constant(*g)) {
      return zero;
  }
  return NULL;
}

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

  Synopsis [Given an array of BDD ids, return the array of
  corresponding BDDs.]

  Description [Given an array of BDD ids, return the array of
  corresponding BDDs.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
bdd_node **
RestrBddNodeArrayFromIdArray(
  bdd_manager	*ddManager,
  array_t	*idArray)
{
  bdd_node **xvars;
  int i,id;
  int nvars = array_n(idArray);

  xvars = ALLOC(bdd_node *, nvars);
  if (xvars == NULL)
    return NULL;

  for(i = 0; i < nvars; i++) {
    id = array_fetch(int,idArray,i);
    xvars[i] = bdd_bdd_ith_var(ddManager,id);
    bdd_ref(xvars[i]);
  }
  return xvars;
}

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

  Synopsis    [Calculate the average bit change in the STG.]

  Description [Calculate the average bit change in the STG. probTR is an ADD
  representing the absolute transition probability matrix of the STG.
  xVars and yVars are the present and next state variables respectively. nVars
  is the number of state variables. 

  average bit change = (\exists^+_x(probTr * HD(x,y))). ]

  SideEffects [None]

  SeeAlso []
******************************************************************************/
double 
RestrAverageBitChange(
  bdd_manager *manager,
  bdd_node *probTR,
  bdd_node **xVars,
  bdd_node **yVars,
  int nVars)
{
  bdd_node *diff, *cube, *PA, *QA;
  bdd_node **vars;
  double Mean;
  int i;

  vars = ALLOC(bdd_node *,2*nVars);
  for (i = 0; i < nVars; i++) {
    vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(xVars[i]));
    bdd_ref(vars[i]);
  }
  for (i = nVars; i < 2*nVars; i++) {
    vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(yVars[i-nVars]));
    bdd_ref(vars[i]);
  }

  cube = bdd_add_compute_cube(manager,vars,NIL(int),2*nVars);
  bdd_ref(cube);

  /* Calculate the Hamming distance ADD. This ADD represents the hamming
   * distance between two vectors represented by xVars and yVars.
   */
  bdd_ref(diff = bdd_add_hamming(manager,xVars,yVars,nVars));
  bdd_ref(PA = bdd_add_apply(manager,bdd_add_times,probTR,diff));
  bdd_recursive_deref(manager,diff);
  
  /* And now add and abstract all the variables.*/
  bdd_ref(QA = bdd_add_exist_abstract(manager,PA,cube));
  bdd_recursive_deref(manager,PA);
  bdd_recursive_deref(manager,cube);
  Mean = (double)bdd_add_value(QA);
  bdd_recursive_deref(manager,QA); 

  for (i = 0; i < 2*nVars; i++) {
    bdd_recursive_deref(manager,vars[i]);
  }
  FREE(vars);
  return Mean;
}

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

  Synopsis [Create an extra set of auxillary BDD variables--corresponding to
  present and next state variables of the network--required during
  restructuring.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
array_t *
RestrCreateNewStateVars(
  Ntk_Network_t *network,
  bdd_manager *ddManager,
  bdd_node **xVars,
  bdd_node **yVars)

{
  Ntk_Node_t *node1;
  char *name, *name1;
  array_t *varValues;
  array_t *nameArray;
  int i,id,index;
  int nVars = Ntk_NetworkReadNumLatches(network);

  array_t *uVarIds, *vVarIds;
  array_t *result;

  varValues = array_alloc(int, 0);
  nameArray = array_alloc(char *,0);    
  uVarIds = array_alloc(int, 0);
  vVarIds = array_alloc(int, 0);
  result = array_alloc(array_t *, 0);

  id = bdd_num_vars(ddManager);

  for (i = 0; i < nVars; i++) {
    index = bdd_node_read_index(yVars[i]);
    node1 = Ntk_NetworkFindNodeByMddId(network,index);
    name = Ntk_NodeReadName(node1);
    name1 = util_strcat3(name,"$NTK2","");
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name1);
    array_insert_last(int, vVarIds, id);
    id++;

    index = bdd_node_read_index(xVars[i]);
    node1 = Ntk_NetworkFindNodeByMddId(network,index);
    name = Ntk_NodeReadName(node1);
    name1 = util_strcat3(name,"$NTK2","");
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name1);
    array_insert_last(int, uVarIds, id);
    id++;

  }
  mdd_create_variables(ddManager,varValues,nameArray,NIL(array_t));

  arrayForEachItem(char *,nameArray,i,name) {
    FREE(name);
  }
  array_free(nameArray);
  array_free(varValues);

  array_insert_last(array_t *, result, uVarIds);
  array_insert_last(array_t *, result, vVarIds);

  return result;
}


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

  Synopsis    [In the absence of initial order of the variables, this
  function assings MDD Ids to the input, present state and next state
  variables.]

  Description [In the absence of initial order of the variables, this
  function assigns MDD Ids to the input, present state and next state
  variables.

  This procedure is NOT currently used and is here for future purposes.]

  SideEffects [The BDD manager is changed accordingly.]

  SeeAlso []
******************************************************************************/
void
RestrSetInitialOrder(
  Ntk_Network_t *network,
  bdd_manager	*ddManager)

{
  Ntk_Node_t *node, *node1;
  lsGen	gen;
  char *name;
  array_t	*varValues;
  array_t	*nameArray;
  int		id;

  varValues = array_alloc(int,0);
  nameArray = array_alloc(char *,0);

  id = 0;
  Ntk_NetworkForEachLatch(network,gen,node) {
    node1 = Ntk_NodeReadShadow(node);
    name = util_strsav(Ntk_NodeReadName(node1));
    Ntk_NodeSetMddId(node1,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;

    name = util_strsav(Ntk_NodeReadName(node));
    Ntk_NodeSetMddId(node,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;
  }

  Ntk_NetworkForEachPrimaryInput(network,gen,node) {
    name = util_strsav(Ntk_NodeReadName(node));
    Ntk_NodeSetMddId(node,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;
  }

  mdd_create_variables(ddManager,varValues,nameArray,NIL(array_t));

  id = 0;
  arrayForEachItem(char *, nameArray, id, name) {
    FREE(name);
  }
  array_free(nameArray);
  array_free(varValues);

}