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

 FileName    [restrDebug.c]

 PackageName [restr]

 Synopsis    [Utility functions to aid in debugging.]

 Description [Utility functions to aid in debugging.]

 SeeAlso     [restrUtil.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 [Print names of network nodes given their id.]

  SideEffects [Print names of network nodes given their id.]

  SeeAlso     []

******************************************************************************/
void
RestrNamePrintByMddId(
  Ntk_Network_t *network,
  array_t 	*array)

{
  char *name;
  int i,id;

  arrayForEachItem(int, array, i, id) {
    name = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(network,id));
    fprintf(vis_stdout, "%s\n",name);
  }
}

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

  Synopsis [Interface function to bdd_print_minterm given an mvf array.]

  SideEffects [Interface function to bdd_print_minterm given an mvf array.]

  SeeAlso     []

******************************************************************************/
void
RestrPrintMvfArray(
  mdd_manager	 *ddManager,
  Mvf_Function_t *mvfArray,
  array_t	 *nodeArray,
  array_t	 *idArray)
{
  int i;
  mdd_t *tempMdd;
  Mvf_Function_t *mvf;
  Ntk_Node_t	*node;

  for(i=0;i<array_n(mvfArray);i++){
    mvf = array_fetch(Mvf_Function_t *, mvfArray, i);
    tempMdd = array_fetch(mdd_t *, mvf, 1);
    if(!(nodeArray == NIL(array_t))) {
      node = array_fetch(Ntk_Node_t *, nodeArray, i);
      fprintf(vis_stdout, "%s ", Ntk_NodeReadName(node));
    }
    if(!(idArray == NIL(array_t))) {
      fprintf(vis_stdout, " %d", array_fetch(int,idArray,i));
    }
    fprintf(vis_stdout, "\n");
    bdd_print_minterm(tempMdd);
  }
}

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

  Synopsis [Prints the variable names of all variables in the manager.]

  SideEffects [Prints the variable names of all variables in the manager]

  SeeAlso     []

******************************************************************************/
void
RestrPrintAllVarNames(
  bdd_manager	*ddManager)
{
  int size, i;
  mvar_type var;
  size = bdd_num_vars((bdd_manager *)ddManager);
  for(i=0;i<size;i++) {
    var = mdd_get_var_by_id(ddManager,i);
    fprintf(vis_stdout," %s",var.name);
  }
  fprintf(vis_stdout,"\n");
}


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

  Synopsis [Print minterms in the onset given a bdd_node *.]

  SideEffects [Print minterms in the onset given a bdd_node *.]

  SeeAlso     []

******************************************************************************/
void
RestrPrintBddNode(
  bdd_manager *manager,
  bdd_node *ddNode)
{
    bdd_t *mdd;
    bdd_node *temp;
    bdd_ref(temp = ddNode);
    mdd = bdd_construct_bdd_t(manager,temp);
    bdd_print_minterm(mdd);
    bdd_free(mdd);
    return;
}

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

  Synopsis [Perform token simulations to check functional equivalence of two
  STGs.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
RestrVerifyFsmEquivBySimulation(
  bdd_manager *ddManager,
  bdd_node *oldTr,
  bdd_node *newTr,
  array_t *outBdds1,
  array_t *outBdds2,
  bdd_node *initBdd1,
  bdd_node *initBdd2,
  bdd_node **xVars,
  bdd_node **yVars,
  bdd_node **piVars,
  int nVars,
  int nPi)
{
  int **sim, N = 11;
  int i,j,numOut1,numOut2;
  bdd_node *lambda1,*lambda2;
  bdd_node **lVars;
  bdd_node *present1,*present2,*next1,*next2;
  bdd_node *out1,*out2;
  bdd_node *input,*inputPre1,*inputPre2;

  sim = ALLOC(int *,N);
  for (i = 0; i < N; i++) {
    sim[i] = ALLOC(int,nPi);
    for (j = 0; j < nPi; j++) {
      sim[i][j] = 0;
    }
  }
  
  numOut1 = array_n(outBdds1);
  numOut2 = array_n(outBdds2);
  assert(numOut1 == numOut2);

  /* New variables to compute output relation */
  lVars = ALLOC(bdd_node *,numOut1);
  for (i = 0; i < numOut1; i++) {
    bdd_ref(lVars[i] = bdd_bdd_new_var(ddManager));
  }

  bdd_ref(lambda1 = bdd_read_one(ddManager));
  bdd_ref(lambda2 = bdd_read_one(ddManager));
  for (i = 0; i < numOut1; i++) {
    bdd_node *temp,*outRel;
    bdd_ref(outRel = bdd_bdd_xnor(ddManager,lVars[i],
				  array_fetch(bdd_node *,outBdds1,i)));
    bdd_ref(temp = bdd_bdd_and(ddManager,lambda1,outRel));
    bdd_recursive_deref(ddManager,outRel);
    bdd_recursive_deref(ddManager,lambda1);
    lambda1 = temp;

    bdd_ref(outRel = bdd_bdd_xnor(ddManager,lVars[i],
				  array_fetch(bdd_node *,outBdds2,i)));
    bdd_ref(temp = bdd_bdd_and(ddManager,lambda2,outRel));
    bdd_recursive_deref(ddManager,outRel);
    bdd_recursive_deref(ddManager,lambda2);
    lambda2 = temp;
  }

  bdd_ref(present1 = initBdd1);
  bdd_ref(present2 = initBdd2);
  /* Simulate the patterns */
  for (i = 0; i < N; i++) {
    bdd_node *temp1;

    bdd_ref(input = bdd_bdd_compute_cube(ddManager,piVars,sim[i],nPi));

    /* Compute next state and outputs for machine 1 */
    bdd_ref(inputPre1 = bdd_bdd_and(ddManager,input,present1));
    bdd_ref(temp1 = bdd_bdd_cofactor(ddManager,oldTr,inputPre1));
    bdd_ref(next1 = bdd_bdd_swap_variables(ddManager,temp1,yVars,xVars,nVars));
    bdd_recursive_deref(ddManager,temp1);
    bdd_recursive_deref(ddManager,present1);
    present1 = next1;
    bdd_ref(out1 = bdd_bdd_cofactor(ddManager,lambda1,inputPre1));
    bdd_recursive_deref(ddManager,inputPre1);

    /* Compute next state and outputs for machine 2 */
    bdd_ref(inputPre2 = bdd_bdd_and(ddManager,input,present2));
    bdd_ref(temp1 = bdd_bdd_cofactor(ddManager,newTr,inputPre2));
    bdd_ref(next2 = bdd_bdd_swap_variables(ddManager,temp1,yVars,xVars,nVars));
    bdd_recursive_deref(ddManager,temp1);
    bdd_recursive_deref(ddManager,present2);
    present2 = next2;
    bdd_ref(out2 = bdd_bdd_cofactor(ddManager,lambda2,inputPre2));
    bdd_recursive_deref(ddManager,inputPre2);
    
    bdd_recursive_deref(ddManager,input);

    if (out1 != out2) {
      (void) fprintf(vis_stdout,"Unequal outputs at i = %d\n",i);
    }
    bdd_recursive_deref(ddManager,out1);
    bdd_recursive_deref(ddManager,out2);
  }

  bdd_recursive_deref(ddManager,present1);
  bdd_recursive_deref(ddManager,present2);
}

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

  Synopsis [Test if the given relation is an equivalence relation.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
RestrTestIsEquivRelation(
  bdd_manager *ddManager,
  bdd_node *rel,
  bdd_node **xVars,
  bdd_node **yVars,
  bdd_node **uVars,
  bdd_node **vVars,
  int nVars)
{
  
  bdd_node *one,*reflex;
  bdd_node *Rxy,*Rvy,*Ruy,*Rux;
  bdd_node *left,*result,*uCube;
  bdd_node **compose;
  int numVars,i;

  numVars = bdd_num_vars(ddManager);
  one = bdd_read_one(ddManager);
  
  /* rel is interms of xVars and uVars */
  /* Test if rel is reflexive: R(x,x) == 1 */
  compose = ALLOC(bdd_node *,numVars);
  for (i = 0; i < numVars; i++) {
    compose[i] = bdd_bdd_ith_var(ddManager,i);
  }
  for (i = 0; i < nVars; i++) {
    int index;
    index = bdd_node_read_index(uVars[i]);
    compose[index] = xVars[i];
  }
  bdd_ref(reflex = bdd_bdd_vector_compose(ddManager,rel,compose));
  if (reflex != one) {
    (void) fprintf(vis_stdout,"Relation is not reflexive.\n");
  } else {
    (void) fprintf(vis_stdout,"Relation IS reflexive.\n");
  }
  bdd_recursive_deref(ddManager,reflex);
  FREE(compose);

  /* Test if rel is symmetric: R(x,u) == R(u,x) */
  bdd_ref(Rxy = bdd_bdd_swap_variables(ddManager,rel,uVars,yVars,nVars));
  bdd_ref(Rvy = bdd_bdd_swap_variables(ddManager,Rxy,xVars,vVars,nVars));
  bdd_ref(Ruy = bdd_bdd_swap_variables(ddManager,Rvy,vVars,uVars,nVars));
  bdd_ref(Rux = bdd_bdd_swap_variables(ddManager,Ruy,yVars,xVars,nVars));
  bdd_recursive_deref(ddManager,Rvy);
  if (Rux != rel) {
    (void) fprintf(vis_stdout,"Relation is not symmetric.\n");
  } else {
    (void) fprintf(vis_stdout,"Relation IS symmetric.\n");
  }
  bdd_recursive_deref(ddManager,Rux);
  
  /* Test if rel is transitive: (\exists_u R(x,u) * R(u,y)) ==> R(x,y) */
  bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
  bdd_ref(left = bdd_bdd_and_abstract(ddManager,rel,Ruy,uCube));
  bdd_recursive_deref(ddManager,Ruy);
  bdd_recursive_deref(ddManager,uCube);
  bdd_ref(result = bdd_bdd_ite(ddManager,left,Rxy,one));
  bdd_recursive_deref(ddManager,Rxy);
  bdd_recursive_deref(ddManager,left);
  if (result != one) {
    (void) fprintf(vis_stdout,"Relation is not transitive.\n");
  } else {
    (void) fprintf(vis_stdout,"Relation IS transitive.\n");
  }
  bdd_recursive_deref(ddManager,result);
}

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

  Synopsis [Print the names of an array of BDD variables.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
RestrPrintVarArrayNames(
  bdd_manager *ddManager,
  bdd_node **xVars,
  int nVars)
{
  int index, i;
  mvar_type var;

  for(i=0;i<nVars;i++) {
    index = bdd_node_read_index(xVars[i]);
    var = mdd_get_var_by_id(ddManager,index);
    fprintf(vis_stdout," %s",var.name);
  }
  fprintf(vis_stdout,"\n");
}

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

  Synopsis [Print an array of character strings.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
RestrPrintNameArray(array_t *nameArray)
{
  int i;
  char *str;
  arrayForEachItem(char *,nameArray,i,str) {
    (void) fprintf(vis_stdout,"%s\n",str);
  }
}

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

  Synopsis [Test if the given relation is deterministic.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
RestrTestIsDeterministic(
  bdd_manager *ddManager,
  bdd_node *tr,
  bdd_node *initBdd,
  bdd_node **xVars,
  bdd_node **yVars,
  int nVars)
{
  bdd_node *cproj2,*ref;
  int flag;

  bdd_ref(ref = bdd_bdd_swap_variables(ddManager,initBdd,xVars,
				       yVars,nVars));
  bdd_ref(cproj2 = bdd_bdd_cprojection(ddManager,tr,ref));
  if (cproj2 != tr) {
    bdd_node *newEdges;
    (void) fprintf(vis_stdout,"** restr diag: Relation is non-deterministic\n");
    /* Let's find out the newly added edges */
    bdd_ref(newEdges = bdd_bdd_and(ddManager,tr,
				   bdd_not_bdd_node(cproj2)));
    (void) fprintf(vis_stdout,"** restr diag: New edges are:\n");
    RestrPrintBddNode(ddManager,newEdges);
    bdd_recursive_deref(ddManager,newEdges);
    flag = 0;
  } else {
    (void) fprintf(vis_stdout,"** restr diag: Relation IS deterministic\n");
    flag = 1;
  }
  bdd_recursive_deref(ddManager,cproj2);
  bdd_recursive_deref(ddManager,ref);
  
  return flag;
}

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