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

  FileName    [eqvMisc.c]

  PackageName [eqv]

  Synopsis    [This file provides some miscellaneous functions for the eqv
               package.]

  Description []

  SeeAlso     []

  Author      [Shaz Qadeer]

  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 "eqvInt.h"

static char rcsid[] UNUSED = "$Id: eqvMisc.c,v 1.10 2009/04/11 01:40:06 fabio Exp $";

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


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


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


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


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


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

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

static boolean NodesMatchUp(Ntk_Node_t *node1, Ntk_Node_t *node2);

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


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


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

  Synopsis    [This function returns a hash table of corresponding primary input
               nodes in network1 and network2.]

  Description [The hash table returned by the function contains corresponding
               primary input nodes in network1 and network2. The correspondence
               is based on the names of the nodes. The following conditions
               constitute an error:
               1) the number of primary inputs in the two networks is different.
               2) there is no primary input in network2 by the same name as
               one occurring in network1.
               3) the two primary inputs in network1 and network2 having the
               same names have different variable types.  
               If an error occurs, NULL is returned.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
st_table *
MapPrimaryInputsByName(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2)
{
  lsGen gen1, gen2;
  Ntk_Node_t *node1, *node2;
  Var_Variable_t *var1, *var2;
  char *name1, *name2;
  boolean flag = FALSE;
  boolean equivalent = TRUE;
  boolean causeOfError = TRUE;
  st_table *inputMap;
  int numValues;
  int i;
  
  if(Ntk_NetworkReadNumPrimaryInputs(network1) !=
           Ntk_NetworkReadNumPrimaryInputs(network2)) {
    error_append("Different number of primary inputs in the two networks\n");
    return NIL(st_table);
  }
  inputMap = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachPrimaryInput(network1, gen1, node1) {
    name1 = Ntk_NodeReadName(node1);
    Ntk_NetworkForEachPrimaryInput(network2, gen2, node2) {
      name2 = Ntk_NodeReadName(node2);
      if (strcmp(name1, name2) == 0) {
	boolean a, b;
        
        var1 = Ntk_NodeReadVariable(node1);
        var2 = Ntk_NodeReadVariable(node2);
	a = Var_VariableTestIsEnumerative(var1);
	b = Var_VariableTestIsEnumerative(var2);
	if((a && !b) || (!a && b)) {
	  error_append("Input ");
          error_append(name1);
          error_append(" and ");
          error_append(name2);
          error_append(" have different variable types\n");
          causeOfError = FALSE;
        }
	else {
          numValues = Var_VariableReadNumValues(var1);
          if(a && b) {
            if(numValues == Var_VariableReadNumValues(var2)) {
              st_insert(inputMap, (char *) node1, (char *) node2);
              flag = TRUE;
            }	
            else {
              error_append("Input ");
              error_append(name1);
              error_append(" and ");
              error_append(name2);
              error_append(" have different range of values\n");
              causeOfError = FALSE;
            }
          }
          else {/* both are symbolic */
            boolean flag2 = TRUE;
            for(i=0; i<numValues; i++) {
              if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
                        Var_VariableReadSymbolicValueFromIndex(var2, i)))
                {
                  flag2 = FALSE;
                  error_append("Input ");
                  error_append(name1);
                  error_append(" and ");
                  error_append(name2);
                  error_append(" have different symbolic values\n");
                  causeOfError = FALSE;
                }
            }
            if(flag2) {
              st_insert(inputMap, (char *) node1, (char *) node2);
              flag = TRUE;
            }
          }
        }
      }
    }

    if(!flag) {
      equivalent = FALSE;    /* name1 did not find a match in network2 */
      if(causeOfError) {
        error_append("Input ");
        error_append(name1);
        error_append(" does not have a match\n");
      }
      else {
        causeOfError = TRUE;
      }
    }
    else {
      flag = FALSE;
    }	
  }
  
  
  if(!equivalent) {
    st_free_table(inputMap);
    return NIL(st_table);
  }
  else {
    return inputMap;
  }
}

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

  Synopsis     [The function returns a hash table of corresponding
  combinational input nodes in network1 and network2.]

  Description  [The hash table returned by the function contains corresponding
               combinational input nodes in network1 and network2. The
               correspondence is based on the names of the nodes. The
               following conditions constitute an error:
               1) the number of combinational inputs in the two networks is
               different.
               2) there is no combinational input in network2 by the same name as
               one occurring in network1.
               3) the two combinational inputs in network1 and network2 having 
               same names have different variable types.  
               If an error occurs, NULL is returned.]

  SideEffects  []

  SeeAlso      []

******************************************************************************/
st_table *
MapCombInputsByName(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2)
{
  lsGen gen1, gen2;
  Ntk_Node_t *node1, *node2;
  Var_Variable_t *var1, *var2;
  char *name1, *name2;
  boolean flag = FALSE;
  boolean equivalent = TRUE;
  boolean causeOfError = TRUE;
  st_table *inputMap;
  int numValues;
  int i;
  
  if(Ntk_NetworkReadNumCombInputs(network1) !=
           Ntk_NetworkReadNumCombInputs(network2)) {
    error_append("Different number of combinational inputs in the two networks\n");
    return NIL(st_table);
  }
  inputMap = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachCombInput(network1, gen1, node1) {
    name1 = Ntk_NodeReadName(node1);
    Ntk_NetworkForEachCombInput(network2, gen2, node2) {
      name2 = Ntk_NodeReadName(node2);
      if (strcmp(name1, name2) == 0) {
	boolean a, b;
        
        var1 = Ntk_NodeReadVariable(node1);
        var2 = Ntk_NodeReadVariable(node2);
	a = Var_VariableTestIsEnumerative(var1);
	b = Var_VariableTestIsEnumerative(var2);
	if((a && !b) || (!a && b)) {
	  error_append("Input ");
          error_append(name1);
          error_append(" and ");
          error_append(name2);
          error_append(" have different variable types\n");
          causeOfError = FALSE;
        }
	else {
          numValues = Var_VariableReadNumValues(var1);
          if(a && b) {
            if(numValues == Var_VariableReadNumValues(var2)) {
              st_insert(inputMap, (char *) node1, (char *) node2);
              flag = TRUE;
            }	
            else {
              error_append("Input ");
              error_append(name1);
              error_append(" and ");
              error_append(name2);
              error_append(" have different range of values\n");
              causeOfError = FALSE;
            }
          }
          else {/* both are symbolic */
            boolean flag2 = TRUE;
            for(i=0; i<numValues; i++) {
              if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
                        Var_VariableReadSymbolicValueFromIndex(var2, i)))
                {
                  flag2 = FALSE;
                  error_append("Input ");
                  error_append(name1);
                  error_append(" and ");
                  error_append(name2);
                  error_append(" have different symbolic values\n");
                  causeOfError = FALSE;
                }
            }
            if(flag2) {
              st_insert(inputMap, (char *) node1, (char *) node2);
              flag = TRUE;
            }
          }
        }
      }
    }

    if(!flag) {
      equivalent = FALSE;    /* name1 did not find a match in network2 */
      if(causeOfError) {
        error_append("Input ");
        error_append(name1);
        error_append(" does not have a match\n");
      }
      else {
        causeOfError = TRUE;
      }
    }
    else {
      flag = FALSE;
    }	
  }
  
  
  if(!equivalent) {
    st_free_table(inputMap);
    return NIL(st_table);
  }
  else {
    return inputMap;
  }
}
  
/**Function********************************************************************

  Synopsis    [This function returns a hash table of corresponding primary
  output nodes in network1 and network2.]

  Description [The hash table returned by the function contains corresponding
               primary output nodes in network1 and network2. The correspondence
               is based on the names of the nodes. The following conditions
               constitute an error:
               1) the number of primary outputs in the two networks is different.
               2) there is no primary output in network2 by the same name as
               one occurring in network1.
               3) the two primary outputs in network1 and network2 having the
               same names have different variable types.  
               If an error occurs, NULL is returned.]
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
st_table *
MapPrimaryOutputsByName(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2)
{
  lsGen gen1, gen2;
  Ntk_Node_t *node1, *node2;
  Var_Variable_t *var1, *var2;
  char *name1, *name2;
  boolean flag = FALSE;
  boolean equivalent = TRUE;
  boolean causeOfError = TRUE;
  st_table *outputMap;
  int numValues;
  int i;
  
  if(Ntk_NetworkReadNumPrimaryOutputs(network1) !=
           Ntk_NetworkReadNumPrimaryOutputs(network2)) {
    error_append("Different number of primary outputs in the two networks\n");
    return NIL(st_table);
  }
  outputMap = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachPrimaryOutput(network1, gen1, node1) {
    name1 = Ntk_NodeReadName(node1);
    Ntk_NetworkForEachPrimaryOutput(network2, gen2, node2) {
      name2 = Ntk_NodeReadName(node2);
      if (strcmp(name1, name2) == 0) {
	boolean a, b;
        
        var1 = Ntk_NodeReadVariable(node1);
        var2 = Ntk_NodeReadVariable(node2);
	a = Var_VariableTestIsEnumerative(var1);
	b = Var_VariableTestIsEnumerative(var2);
	if((a && !b) || (!a && b)) {
	  error_append("Output ");
          error_append(name1);
          error_append(" and ");
          error_append(name2);
          error_append(" have different variable types\n");
          causeOfError = FALSE;
        }
	else {
          numValues = Var_VariableReadNumValues(var1);
          if(a && b) {
            if(numValues == Var_VariableReadNumValues(var2)) {
              st_insert(outputMap, (char *) node1, (char *) node2);
              flag = TRUE;
            }	
            else {
              error_append("Output ");
              error_append(name1);
              error_append(" and ");
              error_append(name2);
              error_append(" have different range of values\n");
              causeOfError = FALSE;
            }
          }
          else {/* both are symbolic */
            boolean flag2 = TRUE;
            for(i=0; i<numValues; i++) {
              if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
                        Var_VariableReadSymbolicValueFromIndex(var2, i)))
                {
                  flag2 = FALSE;
                  error_append("Output ");
                  error_append(name1);
                  error_append(" and ");
                  error_append(name2);
                  error_append(" have different symbolic values\n");
                  causeOfError = FALSE;
                }
            }
            if(flag2) {
              st_insert(outputMap, (char *) node1, (char *) node2);
              flag = TRUE;
            }
          }
        }
        
      }
    }

    if(!flag) {
      equivalent = FALSE;    /* name1 did not find a match in network2 */
      if(causeOfError) {
        error_append("Output ");
        error_append(name1);
        error_append(" does not have a match\n");
      }
      else {
        causeOfError = TRUE;
      }
    }
    else {
      flag = FALSE;
    }	
  }
  
  
  if(!equivalent) {
    st_free_table(outputMap);
    return NIL(st_table);
  }
  else {
    return outputMap;
  }
}

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

  Synopsis    [This function returns a hash table of corresponding
  combinational output nodes in network1 and network2.]

  Description [The hash table returned by the function contains corresponding
               combinational output nodes in network1 and network2. The
               correspondence is based on the names of the nodes. The
               following conditions constitute an error:
               1) the number of combinational outputs in the two networks is
               different.
               2) there is no combinational output in network2 by the same
               name as one occurring in network1.
               3) the two combinational outputs in network1 and network2 having 
               same names have different variable types.  
               If an error occurs, NULL is returned.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
st_table *
MapCombOutputsByName(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2)
{
  lsGen gen1, gen2;
  Ntk_Node_t *node1, *node2;
  Var_Variable_t *var1, *var2;
  char *name1, *name2;
  boolean flag = FALSE;
  boolean equivalent = TRUE;
  boolean causeOfError = TRUE;
  st_table *outputMap;
  int numValues;
  int i;
  
  if(Ntk_NetworkReadNumCombOutputs(network1) !=
     Ntk_NetworkReadNumCombOutputs(network2)) {
    error_append("Different number of combinational outputs in the two networks\n");
    return NIL(st_table);
  }
  outputMap = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachCombOutput(network1, gen1, node1) {
    name1 = Ntk_NodeReadName(node1);
    Ntk_NetworkForEachCombOutput(network2, gen2, node2) {
      name2 = Ntk_NodeReadName(node2);
      if (NodesMatchUp(node1, node2)) {
	boolean a, b;

        var1 = Ntk_NodeReadVariable(node1);
        var2 = Ntk_NodeReadVariable(node2);
	a = Var_VariableTestIsEnumerative(var1);
	b = Var_VariableTestIsEnumerative(var2);
	if((a && !b) || (!a && b)) {
	  error_append("Output ");
          error_append(name1);
          error_append(" and ");
          error_append(name2);
          error_append(" have different variable types\n");
          causeOfError = FALSE;
        }
	else {
          numValues = Var_VariableReadNumValues(var1);
          if(a && b) {
            if(numValues == Var_VariableReadNumValues(var2)) {
              st_insert(outputMap, (char *) node1, (char *) node2);
              flag = TRUE;
            }
            else {
              error_append("Output ");
              error_append(name1);
              error_append(" and ");
              error_append(name2);
              error_append(" have different range of values\n");
              causeOfError = FALSE;
            }
          }
          else {/* both are symbolic */
            boolean flag2 = TRUE;
            for(i=0; i<numValues; i++) {
              if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
                        Var_VariableReadSymbolicValueFromIndex(var2, i)))
                {
                  flag2 = FALSE;
                  error_append("Output ");
                  error_append(name1);
                  error_append(" and ");
                  error_append(name2);
                  error_append(" have different symbolic values\n");
                  causeOfError = FALSE;
                }
            }
            if(flag2) {
              st_insert(outputMap, (char *) node1, (char *) node2);
              flag = TRUE;
	      break;
            }
          }
        }
      }
    }

    if(!flag) {
      equivalent = FALSE;    /* name1 did not find a match in network2 */
      if(causeOfError) {
        error_append("Output ");
        error_append(name1);
        error_append(" does not have a match\n");
      }
      else {
        causeOfError = TRUE;
      }
    }
    else {
      flag = FALSE;
    }	
  }
  
  
  if(!equivalent) {
    st_free_table(outputMap);
    return NIL(st_table);
  }
  else {
    return outputMap;
  }
}

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

  Synopsis    [This function returns the ordering method to be used.]

  SideEffects []
  
  SeeAlso     []

******************************************************************************/
OFT
FindOrderingMethod(void)
{
  return (OFT) NULL;
}

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

  Synopsis    [The function checks whether inputMap and outputMap form valid
               roots and leaves for network1 and network2.]

  Description [inputMap is a hash table of the corresponding leaves in
  network1 and network2. outputMap is a hash table of the corresponding roots
  in network1 and network2. The function checks whether the leaves of each
  network form a complete support of its roots. If this turns out to be false
  for any network, FALSE is returned otherwise TRUE is returned.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
TestRootsAndLeavesAreValid(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2,
  st_table *inputMap,
  st_table *outputMap)
{
  
  st_generator *gen;
  array_t *roots1, *roots2;
  st_table *leaves1, *leaves2;
  Ntk_Node_t *node1, *node2;
  boolean test = TRUE;
  
  roots1 = array_alloc(Ntk_Node_t *, 0);
  roots2 = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(outputMap, gen, &node1, &node2) {
    array_insert_last(Ntk_Node_t *, roots1, node1);
    array_insert_last(Ntk_Node_t *, roots2, node2);
  }
  leaves1 = st_init_table(st_ptrcmp, st_ptrhash);
  leaves2 = st_init_table(st_ptrcmp, st_ptrhash);
  st_foreach_item(inputMap, gen, &node1, &node2) {
    st_insert(leaves1, node1, NULL);
    st_insert(leaves2, node2, NULL);
  }
  if(!Ntk_NetworkTestLeavesCoverSupportOfRoots(network1, roots1,
                                             leaves1)) {
    error_append("Leaves do not form a complete support for roots in network1.\n");
    test = FALSE;
  }
  if(!Ntk_NetworkTestLeavesCoverSupportOfRoots(network2, roots2,
                                             leaves2)) {
    error_append("Leaves do not form a complete support for roots in network2.\n");
    test = FALSE;
  }
  array_free(roots1);
  array_free(roots2);
  st_free_table(leaves1);
  st_free_table(leaves2);
  return test;
}

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

  Synopsis    [This function takes a hash table of names and generates a
               hash table of nodes.]

  Description [The input to the function is a hash table of names of nodes.
               It returns a hash table of nodes corresponding to the names.
               In the hash table names, key is a name in network1 and value
               is a name in network2. Similarly, in the table which is
               returned, key is a node in network1 and value a node in
               network2. If no node by a certain name is found in a network,
               NULL is returned.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
st_table *
MapNamesToNodes(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2,
  st_table *names)
{
  st_table *nodes = st_init_table(st_ptrcmp, st_ptrhash);
  char *name1, *name2;
  Ntk_Node_t *node1, *node2;
  boolean error = FALSE;
  st_generator *gen;
  
  
  st_foreach_item(names, gen, &name1, &name2) {
    if((node1 = Ntk_NetworkFindNodeByName(network1, name1)) ==
       NIL(Ntk_Node_t)) {
      error = TRUE;
      error_append(name1);
      error_append(" not present in network1.\n");
    }
    
    if((node2 = Ntk_NetworkFindNodeByName(network2, name2)) ==
       NIL(Ntk_Node_t)) {
      error = TRUE;
      error_append(name2);
      error_append(" not present in network2.\n");
    }
    st_insert(nodes, (char *) node1, (char *) node2);
  }
  if(error) {
    st_free_table(nodes);
    return NIL(st_table);
  }
  else {
    return nodes;
  }
}

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

  Synopsis    [This function reads an input file containing names of roots and
  leaves, and stores the corresponding names in the two hash tables-
  rootsTable and leavesTable.]
  
  Description [The function returns 0 if there are no roots or leaves in the
               file. It is an error not to have either roots or leaves in the
               file. It returns 1 if there are roots but no leaves, 2 if there
               are leaves but no roots, and 3 if there are both roots and
               leaves.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
ReadRootLeafMap(
  FILE *inputFile,
  st_table *rootsTable,
  st_table *leavesTable)
{
  char *name;
  char *rootName1, *rootName2;
  char *leafName1, *leafName2;
  char c;
  boolean rootsFlag= 0;
  boolean leavesFlag = 0;
  st_generator *gen;
  
  while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
  ungetc(c, inputFile);
  name = ALLOC(char, 20);
  
  if(fscanf(inputFile, "%s", name) == EOF) {
    FREE(name);
    return 0;
    /* both roots and leaves absent */
  }
  if(!strcmp(name, ".roots")) {
    rootsFlag = 1;
    while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
    ungetc(c, inputFile);
    while((fscanf(inputFile, "%s", name) != EOF) && strcmp(name, ".leaves")) {
      rootName1 = ALLOC(char, strlen(name) + 1);
      strcpy(rootName1, name);
      while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
      ungetc(c, inputFile);
      if((fscanf(inputFile, "%s", name) == EOF) || (!strcmp(name, ".leaves"))) {
        FREE(name);
        FREE(rootName1);
        st_foreach_item(rootsTable, gen, &rootName1, &rootName2) {
          FREE(rootName1);
          FREE(rootName2);
          return 0;
        }
      }
      rootName2 = ALLOC(char, strlen(name) + 1);
      strcpy(rootName2, name);
      st_insert(rootsTable, rootName1, rootName2);
      while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
      ungetc(c, inputFile);
      name[0] = '\0'; /* this is to insure that whenever the while loop
                         is terminated, only one of the conditions is false */
    }
  }
  if(!strcmp(name, ".leaves")) {
    leavesFlag = 1;
    while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
    ungetc(c, inputFile);
    while(fscanf(inputFile, "%s", name) != EOF) {
      leafName1 = ALLOC(char, strlen(name) + 1);
      strcpy(leafName1, name);
      while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
      ungetc(c, inputFile);
      if(fscanf(inputFile, "%s", name) == EOF) {
        FREE(name);
        FREE(leafName1);
        st_foreach_item(leavesTable, gen, &leafName1, &leafName2) {
          FREE(leafName1);
          FREE(leafName2);
          return 0;
        }
      }
      leafName2 = ALLOC(char, strlen(name) + 1);
      strcpy(leafName2, name);
      st_insert(leavesTable, leafName1, leafName2);
      while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
      ungetc(c, inputFile);
    }
  }
  FREE(name);
  if(rootsFlag == 1) {
    if(leavesFlag == 1) {
      return 3; /* both leaves and roots present */
    }
    else {
      return 2; /* roots present but leaves absent */
    }
  }
  else {
    if(leavesFlag == 1) {
      return 1; /* roots absent but leaves present */
    }
    else {
      return 0;
    }
  }
}
  
/**Function********************************************************************

  Synopsis    [This function generates the default ordering of leaf nodes.]

  Description [The function checks if network1 has a partition registered with
  it. If there is no partition, The function orders the variables of network1,
  using the option Ord_All_c i.e. orders all the nodes. If a partition exists,
  the existing ordering is left undisturbed. It then copies the mddIds
  of those nodes of network1 which are present in inputMap into
  the corresponding nodes of network2.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
DefaultCommonOrder(
  Ntk_Network_t *network1, 
  Ntk_Network_t *network2,
  st_table *inputMap)
{
  st_generator *gen;
  Ntk_Node_t *node1, *node2;
  int id;
  lsList dummy = (lsList) 0;
  
  if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) == NIL(void)) {
    Ord_NetworkOrderVariables(network1, Ord_RootsByDefault_c,
                              Ord_NodesByDefault_c, FALSE, Ord_All_c,
                              Ord_Unassigned_c, dummy, 0);
  }
  
  st_foreach_item(inputMap, gen, &node1, &node2) {
    id = Ntk_NodeReadMddId(node1);
    Ntk_NodeSetMddId(node2, id);
  }
}
  
      

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

  Synopsis    [This function checks whether the leaves present in leavesTable
  constitute the full set of primary inputs of network1 and network2.]

  Description [leavesTable contains names of corresponding leaves in network1
  and network2. The function returns TRUE if the leaves present in leavesTable
  constitute the full set of primary inputs of network1 and network2. The
  following  conditions result in a return value of FALSE:
  a) there is no node by a name present in leavesTable.
  b) the node with a particular name is not a primary input
  c) the number of leaves is different from the number of primary inputs in
  either network.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
TestLeavesAreValid(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2,
  st_table *leavesTable)

{
  st_generator *gen;
  Ntk_Node_t *node1, *node2;
  char *name1, *name2;
  boolean valid = TRUE;
  int count = 0;
  
  st_foreach_item(leavesTable, gen, &name1, &name2) {
    node1 = Ntk_NetworkFindNodeByName(network1, name1);
    node2 = Ntk_NetworkFindNodeByName(network2, name2);
    if(node1 == NIL(Ntk_Node_t)) {
      error_append(name1);
      error_append(" not found in network1.\n");
      valid = FALSE;
    }
    else {
      if(!Ntk_NodeTestIsPrimaryInput(node1)) {
        error_append(name1);
        error_append(" is not a primary input node\n");
        valid = FALSE;
      }
    }
    
    if(node2 == NIL(Ntk_Node_t)) {
      error_append(name2);
      error_append(" not found in network2.\n");
      valid = FALSE;
    }
    else {
      if(!Ntk_NodeTestIsPrimaryInput(node2)) {
        error_append(name2);
        error_append(" is not a primary input node\n");
        valid = FALSE;
      }
    }
    
    count ++;
  }
  if(valid) {
    if(!((Ntk_NetworkReadNumPrimaryInputs(network1) == count) && (Ntk_NetworkReadNumPrimaryInputs(network2) == count))) {
      error_append("All primary inputs not specified in the input file\n");
      valid = FALSE;
    }
  }
  return valid;
}

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

  Synopsis       [The function checks whether the names present in rootsTable
  have nodes corresponding to them present in network1 and network2.]

  Description    [rootsTable contains names of corresponding roots in network1
  and network2. The function returns TRUE if the roots present in rootsTable
  have nodes corresponding to them in the network1 and network2. Otherwise,
  FALSE is returned.]

  SideEffects    []

  SeeAlso        []

******************************************************************************/
boolean
TestRootsAreValid(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2,
  st_table *rootsTable)

{
  st_generator *gen;
  char *name1, *name2;
  boolean valid = TRUE;
  
  st_foreach_item(rootsTable, gen, &name1, &name2) {
    if(Ntk_NetworkFindNodeByName(network1, name1) == NIL(Ntk_Node_t)) {
      valid = FALSE;
      error_append(name1);
      error_append(" not present in network1.\n");
    }
    
    if(Ntk_NetworkFindNodeByName(network2, name2) == NIL(Ntk_Node_t)) {
      valid = FALSE;
      error_append(name2);
      error_append(" not present in network2.\n");
    }
  }
  return valid;
}

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

  Synopsis           [The function checks whether the partition registered
  with network has vertices corresponding to nodes stored as keys in roots and
  leaves.]

  Description        [The function returns TRUE if all the nodes stored as
                      keys in roots and leaves have corresponding vertices in
                      the partition of network. It returns FALSE otherwise. It
                      is assumed that network has a partition associated with
                      it.]

  SideEffects        []

  SeeAlso            []

******************************************************************************/
boolean
TestPartitionIsValid(
  Ntk_Network_t *network,
  st_table *roots,
  st_table *leaves)
{
  graph_t *partition = Part_NetworkReadPartition(network);
  st_generator *gen;
  char *name;
  Ntk_Node_t *node1, *node2;
  boolean flag = TRUE;
  
  st_foreach_item(roots, gen, &node1, &node2) {
    name = Ntk_NodeReadName(node1);
    if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
      flag = FALSE;
    }
  }
  st_foreach_item(leaves, gen, &node1, &node2) {
    name = Ntk_NodeReadName(node1);
    if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
      flag = FALSE;
    }
  }
  return flag;
}

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

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

  Synopsis    [Check whether two nodes may be matched by name.]

  Description [Check whether two nodes from different networks may be
  matched by name in equivalence verification.  If the two nodes have
  the same names, then they match.  Moreover, if the two nodes are
  latch inputs and the corresponding latches match by name, they also
  match.  This last clause makes comb_verify a lot more useful because
  small changes in Verilog source or in its translation to blif-mv
  usually leave the latch names unchanged, but alter the names of
  the next state variables.]

  SideEffects [none]

  SeeAlso     [MapCombOutputsByName]

******************************************************************************/
static boolean
NodesMatchUp(
  Ntk_Node_t *node1 /* node from network1 */,
  Ntk_Node_t *node2 /* node from network2 */
  )
{
  char *name1, *name2;

  name1 = Ntk_NodeReadName(node1);
  name2 = Ntk_NodeReadName(node2);

  if (strcmp(name1, name2) == 0)
    return TRUE;

  /* Try to match through the state variables. */
  if ((Ntk_NodeTestIsLatchDataInput(node1) &&
      Ntk_NodeTestIsLatchDataInput(node2)) ||
      (Ntk_NodeTestIsLatchInitialInput(node1) &&
       Ntk_NodeTestIsLatchInitialInput(node2))) {
    Ntk_Node_t *latch1, *latch2;
    char *nameLatch1, *nameLatch2;
    array_t *fanout1, *fanout2;

    fanout1 = Ntk_NodeReadFanouts(node1);
    if (array_n(fanout1) != 1) return FALSE;
    fanout2 = Ntk_NodeReadFanouts(node2);
    if (array_n(fanout2) != 1) return FALSE;

    latch1 = array_fetch(Ntk_Node_t *, fanout1, 0);
    assert(Ntk_NodeTestIsLatch(latch1));
    latch2 = array_fetch(Ntk_Node_t *, fanout2, 0);
    assert(Ntk_NodeTestIsLatch(latch2));

    nameLatch1 = Ntk_NodeReadName(latch1);
    nameLatch2 = Ntk_NodeReadName(latch2);

    return (strcmp(nameLatch1, nameLatch2) == 0);
  }

  return FALSE;

} /* NodesMatchUp */