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

  FileName    [ordIo.c]

  PackageName [ord]

  Synopsis    [Routines to read and write variable orderings.]

  Author      [Adnan Aziz, Tom Shiple]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

******************************************************************************/

#include "ordInt.h"

static char rcsid[] UNUSED = "$Id: ordIo.c,v 1.15 2004/07/28 20:42:10 jinh Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
/*
 * States of the state machine used to parse the input node list file.
 */
#define STATE_TEST 0 /* next char is in first column */
#define STATE_WAIT 1 /* wait until end of line '\n' is reached */
#define STATE_IN   2 /* parsing a node name */

/*
 * Maximum permissible length of a node name in the input node list file.
 */
#define MAX_NAME_LENGTH 32768


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

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

static array_t * NodeBuildBddLevelArrayFromNtkNode(Ntk_Node_t * node);
static array_t * NodeBuildBddIdArrayFromNtkNode(Ntk_Node_t * node);
static int IntegersCompare(const void * obj1, const void * obj2);
static int NodesCompareBddLevelArray(lsGeneric node1, lsGeneric node2);
static array_t * NodeReadBddLevelArray(Ntk_Node_t * node);
static void NodeSetBddLevelArray(Ntk_Node_t * node, array_t * bddLevelArray);
static boolean NameStringProcess(char * nameString, Ntk_Network_t * network, lsList nodeList, int verbose);

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


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

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

  Synopsis    [Prints to a file the current ordering of MDD variables.]

  Description [Prints to a file all the nodes specified by orderType.
  OrderType can be one of Ord_All_c, Ord_InputAndLatch_c or
  Ord_NextStateNode_c (see ord.h for the meaning of these types).  For each
  node, prints the following: name, node type, MDD id, number of values in the
  range of the node output, and a list of the levels (in the current ordering)
  of the BDD variables that constitute this multi-valued variable.  The nodes
  are printed to the file in ascending order of the lowest level corresponding
  BDD variable. If there exists a node in the class specified by orderType
  that doesn't have an mddId, then the routine writes a message to
  error_string, and returns 0.  In all other cases, it writes to the file and
  then returns 1.  It is the responsibility of the user to close the file.]

  SideEffects []

******************************************************************************/
int
Ord_NetworkPrintVariableOrder(
  FILE * fp,
  Ntk_Network_t * network,
  Ord_OrderType  orderType /* Ord_All_c, Ord_InputAndLatch_c or Ord_NextStateNode_c */)
{
  lsGen        gen;
  lsList       nodeList;
  Ntk_Node_t  *node;
  int          maxNameLength;
  time_t       now;
  struct tm   *nowStructPtr;
  char        *nowTxt;

  assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c)
         || (orderType == Ord_NextStateNode_c));

  /*
   * First, build up a list of all the nodes covered by orderType.
   */
  if (orderType == Ord_All_c) {
    nodeList = lsCopy(Ntk_NetworkReadNodes(network),
		      (lsGeneric (*) (lsGeneric)) NULL);
  }
  else {
    nodeList = lsCreate();
    Ntk_NetworkForEachNode(network, gen, node) {
      if (Ntk_NodeTestIsNextStateNode(node)
          || ((orderType == Ord_InputAndLatch_c) && Ntk_NodeTestIsCombInput(node))) {
        (void) lsNewEnd(nodeList, (lsGeneric) node, LS_NH);
      }
    }
  }
  
  /*
   * As a sanity check, make sure that all the variables in orderType have an
   * MDD id.
   */
  lsForEachItem(nodeList, gen, node) {
    if (Ntk_NodeReadMddId(node) == NTK_UNASSIGNED_MDD_ID) {
      error_append("node ");
      error_append(Ntk_NodeReadName(node));
      error_append(" not ordered\n");

      (void) lsFinish(gen);
      (void) lsDestroy(nodeList, (void (*) (lsGeneric)) NULL);
      return (0);
    }
  }

  /*
   * For each node in nodeList, get the array of levels of the BDD variables
   * which make up the MDD variable of node.
   */
  lsForEachItem(nodeList, gen, node) {
    array_t *bddLevelArray = NodeBuildBddLevelArrayFromNtkNode(node);

    NodeSetBddLevelArray(node, bddLevelArray);
  }

  /*
   * Sort the nodes of nodeList in ascending order of the lowest level BDD
   * variable corresponding to a node's MDD variable.
   */
  (void) lsSort(nodeList, NodesCompareBddLevelArray);

  /*
   * Compute the maximum length of a node name, for pretty printing.
   */
  maxNameLength = 0;
  lsForEachItem(nodeList, gen, node) {
    int nameLength = strlen(Ntk_NodeReadName(node));
    maxNameLength = (nameLength > maxNameLength) ? nameLength : maxNameLength;
  }
  
  /*
   * Write out the header for the output file.
   */
  now = time(0);
  nowStructPtr = localtime(& now);
  nowTxt = asctime(nowStructPtr);
  
  (void) fprintf(fp, "# %s\n", Vm_VisReadVersion());
  (void) fprintf(fp, "# network name: %s\n", Ntk_NetworkReadName(network));
  (void) fprintf(fp, "# generated: %s", nowTxt);
  (void) fprintf(fp, "#\n");
  (void) fprintf(fp, "# %-*s type            mddId vals levs\n",
                 maxNameLength, "name");
  
  /*
   * Write out the nodes in order.
   */
  lsForEachItem(nodeList, gen, node) {
    int i;
    array_t *bddLevelArray = NodeReadBddLevelArray(node);
    char *nodeType = Ntk_NodeObtainTypeAsString(node);
    
    (void) fprintf(fp, "%-*s  %-16s %5d %4d ",
                   maxNameLength,
                   Ntk_NodeReadName(node),
                   nodeType,
                   Ntk_NodeReadMddId(node),
                   Var_VariableReadNumValues(Ntk_NodeReadVariable(node)));
    FREE(nodeType);

    (void) fprintf(fp, "(");
    for (i = 0; i < array_n(bddLevelArray); i++) {
      int level = array_fetch(int, bddLevelArray, i);
      
      if (i == 0) {
        (void) fprintf(fp, "%d", level);
      }
      else {
        (void) fprintf(fp, ", %d", level);
      }
    }
    (void) fprintf(fp, ")\n");
    array_free(bddLevelArray);
  }

  (void) lsDestroy(nodeList, (void (*) (lsGeneric)) NULL);
  return (1);
}
  

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

  Synopsis    [Returns a name array of combinational input variables in order.]

  SideEffects []

******************************************************************************/
char **
Ord_NetworkGetCombInputNamesInOrder(
  Ntk_Network_t *network)
{
  lsGen		gen;
  lsList	nodeList;
  Ntk_Node_t	*node;
  int		i;
  char		**names;

  i = 0;
  nodeList = lsCreate();
  Ntk_NetworkForEachNode(network, gen, node) {
    if (Ntk_NodeTestIsCombInput(node)) {
      (void) lsNewEnd(nodeList, (lsGeneric) node, LS_NH);
      i++;
    }
  }

  names = (char **)ALLOC(char *, i);
  if (!names)
    return(NULL);
  
  /*
   * For each node in nodeList, get the array of levels of the BDD variables
   * which make up the MDD variable of node.
   */
  lsForEachItem(nodeList, gen, node) {
    array_t *bddLevelArray = NodeBuildBddLevelArrayFromNtkNode(node);

    NodeSetBddLevelArray(node, bddLevelArray);
  }

  /*
   * Sort the nodes of nodeList in ascending order of the lowest level BDD
   * variable corresponding to a node's MDD variable.
   */
  (void) lsSort(nodeList, NodesCompareBddLevelArray);

  /*
   * Write out the nodes in order.
   */
  i = 0;
  lsForEachItem(nodeList, gen, node) {
    names[i] = (char *)malloc(strlen(Ntk_NodeReadName(node)) + 1);
    strcpy(names[i], Ntk_NodeReadName(node));
    i++;
  }

  (void) lsDestroy(nodeList, (void (*) (lsGeneric)) NULL);
  return(names);
}


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

  Synopsis    [Returns a list of nodes corresponding to the names in a file.]

  Description [Parses a file and builds a node list corresponding to the names
  found in the first "column" of each line of the file.  Any line starting
  with the comment character '#' or white space is ignored.  If a name is
  found for which there doesn't exist a corresponding node in network, then a
  message is written to error_string, the partial node list is freed, and the
  function returns FALSE; otherwise, it returns TRUE, and a pointer to a list
  is returned.]

  Comment [The parser consists of 3 states.  See the documentation
  accompanying the #defines defining the state names.]
  
  SideEffects []

******************************************************************************/
boolean
Ord_FileReadNodeList(
  FILE * fp,
  Ntk_Network_t * network,
  lsList * nodeList /* of Ntk_Node_t , for return */,
  int verbose)
{
  int     c;
  int     state;
  int     curPosition = 0;
  boolean status;
  char    nameString[MAX_NAME_LENGTH];
  boolean returnFlag = TRUE;
  
  *nodeList = lsCreate();

  state = STATE_TEST;
  while ((c = fgetc(fp)) != EOF) {

    switch (state) {
        case STATE_TEST:
          /* At start of a new line. */
          if (c == '#') {
            /* Line starting with comment character; wait for newline */
            state = STATE_WAIT;
          }
          else if ((c == ' ') || (c == '\t')) {
            /* Line starting with white space; wait for newline */
            state = STATE_WAIT;
          }
          else if (c == '\n') {
            /* Line starting newline; go to next line */
            state = STATE_TEST;
          }
          else {
            /* Assume starting a node name. */
            curPosition = 0;
            nameString[curPosition++] = c;
            state = STATE_IN;
          }
          break;
        case STATE_WAIT:
          /*
           * Waiting for the newline character.
           */
          state = (c == '\n') ? STATE_TEST : STATE_WAIT;
          break;
        case STATE_IN:
          /*
           * Parsing a node name.  If white space reached, then terminate the
           * node name and process it.  Else, continue parsing.
           */
          if ((c == ' ') || (c == '\n') || (c == '\t')) {
            nameString[curPosition] = '\0';
            status = NameStringProcess(nameString, network, *nodeList, verbose);
            if (status == FALSE) {
              returnFlag = FALSE;
            }
            state = (c == '\n') ? STATE_TEST : STATE_WAIT;
          }
          else {
            nameString[curPosition++] = c;
            if (curPosition >= MAX_NAME_LENGTH) {
              error_append("maximum node name length exceeded");
              returnFlag = FALSE;
            }
            state = STATE_IN; /* redundant, but be explicit */
          }
          break;
        default:
          fail("unrecognized state");
    }
  }

  /*
   * Handle case where EOF terminates a name.
   */
  if (state == STATE_IN) {
    nameString[curPosition] = '\0';
    status = NameStringProcess(nameString, network, *nodeList, verbose);
    if (status == FALSE) {
      returnFlag = FALSE;
    }
  }

  if (returnFlag) {
    return TRUE;
  }
  else {
    (void) lsDestroy(*nodeList, (void (*) (lsGeneric)) NULL);
    return FALSE;
  }
}


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


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

  Synopsis    [Makes new variable order.]

  Description [Makes new variable order. Returns 1 if not successful.]

  SideEffects []

******************************************************************************/
int
OrdMakeNewVariableOrder(mdd_manager *mddMgr, lsList suppliedNodeList,
		     int group, int verbose)
{
  int		i, nVars;
  int		*invPerm = NIL(int);
  int		*groupInfo = NIL(int);
  int		length, bddId, mvLen;
  lsGen		gen;
  Ntk_Node_t	*node;
  array_t	*bddIdArray;
  char		*name = NIL(char), *prevName = NIL(char), *longName;
  int		len1, len2, minLen;

  nVars = bdd_num_vars(mddMgr);
  invPerm = ALLOC(int, nVars);

  length = 0;
  if (group) {
    prevName = NIL(char);
    groupInfo = ALLOC(int, nVars);
    memset(groupInfo, 0, sizeof(int) * nVars);
  }
  lsForEachItem(suppliedNodeList, gen, node) {
    bddIdArray = NodeBuildBddIdArrayFromNtkNode(node);
    mvLen = array_n(bddIdArray);
    if (group) {
      name = Ntk_NodeReadName(node);
      if (prevName) {
	len1 = strlen(prevName);
	len2 = strlen(name);
	if (len1 < len2) {
	  minLen = len1;
	  longName = name;
	} else {
	  minLen = len2;
	  longName = prevName;
	}
	if (strncmp(name, prevName, minLen) == 0) {
	  if (strcmp(longName + minLen, "$NS") == 0)
	    groupInfo[length - mvLen] = mvLen * 2;
	}
      }
    }
    for (i = 0; i < mvLen; i++) {
      bddId = array_fetch(int, bddIdArray, i);
      invPerm[length] = bddId;
      length++;
    }
    array_free(bddIdArray);
    if (group)
      prevName = name;
  }

  if (length != nVars) {
    fprintf(vis_stderr,
	    "** ord error: the number of variables does not match\n");
    FREE(invPerm);
    if (group)
      FREE(groupInfo);
    return(1);
  }

  bdd_discard_all_var_groups(mddMgr);
  bdd_shuffle_heap(mddMgr, invPerm);

  if (group) {
    mdd_t	*var;

    for (i = 0; i < nVars; i++) {
      if (groupInfo[i]) {
	var = bdd_var_with_index(mddMgr, invPerm[i]);
	bdd_new_var_block(var, groupInfo[i]);
	i += groupInfo[i] - 1;
      }
    }
    FREE(groupInfo);
  }

  FREE(invPerm);
  return(0);
}


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

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

  Synopsis    [Gets the levels of the BDD variables corresponding to the MDD
  variable of a node.]

  Description [Returns an array (of int's) of the levels of the BDD variables
  corresponding to the MDD variable of a node.  The level of a BDD variable is
  it place in the current variable ordering of the BDD manager.  The returned
  array is sorted in ascending order.  It is the responsibility of the caller
  to free this array.]

  SideEffects []

******************************************************************************/
static array_t *
NodeBuildBddLevelArrayFromNtkNode(
  Ntk_Node_t * node)
{
  int            i;
  Ntk_Network_t *network       = Ntk_NodeReadNetwork(node);
  mdd_manager   *mddManager    = Ntk_NetworkReadMddManager(network);
  array_t       *mvarArray     = mdd_ret_mvar_list(mddManager);
  int            mddId         = Ntk_NodeReadMddId(node);
  mvar_type      mv;
  array_t       *bddLevelArray;

  mv            = array_fetch(mvar_type, mvarArray, mddId);
  bddLevelArray = array_alloc(int, mv.encode_length);

  for (i = 0; i < mv.encode_length; i++) {
    int    bddId    = mdd_ret_bvar_id(&mv, i);
    bdd_t *varBdd   = bdd_get_variable((bdd_manager *) mddManager, bddId);
    int    varLevel = (int) bdd_top_var_level((bdd_manager *) mddManager, varBdd);

    bdd_free(varBdd);
    array_insert_last(int, bddLevelArray, varLevel);
  }
  array_sort(bddLevelArray, IntegersCompare);

  return (bddLevelArray);
}


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

  Synopsis    [Gets the indices of the BDD variables corresponding to the MDD
  variable of a node.]

  Description [Returns an array (of int's) of the indices of the BDD variables
  corresponding to the MDD variable of a node. It is the responsibility of the
  caller to free this array.]

  SideEffects []

******************************************************************************/
static array_t *
NodeBuildBddIdArrayFromNtkNode(
  Ntk_Node_t * node)
{
  int            i, bddId;
  Ntk_Network_t *network    = Ntk_NodeReadNetwork(node);
  mdd_manager   *mddManager = Ntk_NetworkReadMddManager(network);
  array_t       *mvarArray  = mdd_ret_mvar_list(mddManager);
  int            mddId      = Ntk_NodeReadMddId(node);
  mvar_type      mv;
  array_t       *bddIdArray;

  mv         = array_fetch(mvar_type, mvarArray, mddId);
  bddIdArray = array_alloc(int, mv.encode_length);

  for (i = 0; i < mv.encode_length; i++) {
    bddId = mdd_ret_bvar_id(&mv, i);
    array_insert_last(int, bddIdArray, bddId);
  }

  return (bddIdArray);
}


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

  Synopsis    [Used to sort an array of integers in ascending order.]

  SideEffects []

******************************************************************************/
static int
IntegersCompare(
  const void * obj1,
  const void * obj2)
{
  int int1 = *(int *) obj1;
  int int2 = *(int *) obj2;
  
  if (int1 < int2) {
    return -1;
  }
  else if (int1 == int2) {
    return 0;
  }
  else {
    return 1;
  }
}


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

  Synopsis    [Used to sort an array of nodes in ascending order of lowest BDD
  level.]

  SideEffects []

******************************************************************************/
static int
NodesCompareBddLevelArray(
  lsGeneric node1,
  lsGeneric node2)
{
  array_t *bddLevelArray1 = NodeReadBddLevelArray((Ntk_Node_t *) node1);
  array_t *bddLevelArray2 = NodeReadBddLevelArray((Ntk_Node_t *) node2);
  int      firstLevel1    = array_fetch(int, bddLevelArray1, 0);
  int      firstLevel2    = array_fetch(int, bddLevelArray2, 0);
  
  if (firstLevel1 < firstLevel2) {
    return -1;
  }
  else if (firstLevel1 == firstLevel2) {
    return 0;
  }
  else {
    return 1;
  }
}


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

  Synopsis    [Gets the BDD level array of a node.]

  SideEffects []

  SeeAlso     [NodeSetBddLevelArray NodesCompareBddLevelArray]

******************************************************************************/
static array_t *
NodeReadBddLevelArray(
  Ntk_Node_t * node)
{
  return ((array_t *) Ntk_NodeReadUndef(node));
}


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

  Synopsis    [Sets the BDD level array of a node.]

  SideEffects []

  SeeAlso     [NodeReadBddLevelArray]

******************************************************************************/
static void
NodeSetBddLevelArray(
  Ntk_Node_t * node,
  array_t * bddLevelArray)
{
  Ntk_NodeSetUndef(node, (void *) bddLevelArray);
}


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

  Synopsis    [Processes the name of a node.]

  Description [Processes the name of a node. If there is no node in network
  with name nameString, then the function writes a message in error_string,
  and returns FALSE.  If the corresponding node is found, then the node is
  added to the end of nodeList; else, nothing is done.  In either case, TRUE
  is returned.]

  SideEffects []

******************************************************************************/
static boolean
NameStringProcess(
  char * nameString,
  Ntk_Network_t * network,
  lsList  nodeList,
  int verbose)
{
  Ntk_Node_t *node = Ntk_NetworkFindNodeByActualName(network, nameString);

  if (node == NIL(Ntk_Node_t)) {
    error_append("Node not found for name: ");
    error_append(nameString);
    error_append("\n");
    return FALSE;
  }

  if (verbose > 1) {
    (void) fprintf(vis_stdout, "Reading node: %s\n", Ntk_NodeReadName(node));
  }

  (void) lsNewEnd(nodeList, (lsGeneric) node, LS_NH);  
  return TRUE;
}