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

  FileName    [varVariable.c]

  PackageName [var]

  Synopsis    [Routines to access the MV-variable data structure.]

  Description []

  SeeAlso     []

  Author      [Yuji Kukimoto]

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

static char rcsid[] UNUSED = "$Id: varVariable.c,v 1.6 2009/01/18 01:58:09 fabio Exp $";

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


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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


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


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

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

static int _VarVariableSetType(Var_Variable_t *var, int type);
static int _VarVariableResetType(Var_Variable_t *var, int type);
static char * _VarTypeDecode(int type);
static array_t * _VarStringArrayDup(array_t *array);
static void _VarStringArrayFree(array_t *array);

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


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

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

  Synopsis    [Adds range/symbolic value information to a variable.]

  Description [Adds range/symbolic value information to a variable. This
  function is typically called when a .mv construct is encountered for
  a variable which is already defined by either .inputs or .outputs.
  The arguments of this function are a pointer to a variable, the number
  of values the variable can take, and an array of symbolic value names
  stored as character strings. If the variable is an enumerative variable,
  then the last argument should be set to NIL(array_t). It is the user's
  responsibility to free the array and its strings since the function
  creates a copy of the strings internally. Returns 1 if success.
  Otherwise returns 0.]

  SideEffects []

  SeeAlso     [Var_VariableAlloc Var_VariableFree]

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

boolean
Var_VariableAddRangeInfo(
  Var_Variable_t * var,
  int numValues,
  array_t * symValArray)
{
  int i;
  char *symValue;
  st_table *valueToIndex;

  if (var->indexToValue != NIL(array_t) || var->numValues != 2){
    error_append("Error: The range of variable ");
    error_append(var->name);
    error_append(" has been already set.\n");
    return 0;
  }

  if (symValArray != NIL(array_t)){
    if (numValues != array_n(symValArray)){
      error_append("Error: Mismatch of range and # of symbolic values.\n");
      return 0;
    }
    valueToIndex = st_init_table(strcmp,st_strhash);
    var->indexToValue = _VarStringArrayDup(symValArray);
    for (i=0; i < numValues; i++) {
      symValue = array_fetch(char *,var->indexToValue,i);
      if (st_insert(valueToIndex,symValue,(char *)((long)i))) {
        error_append("Error: Invalid argument for Var_VariableAddRangeInfo().\n");
        error_append("- Symbolic value ");
        error_append(symValue);
        error_append(" is redefined.\n");
        st_free_table(valueToIndex);
        return 0;
      }
    }
    var->valueToIndex = valueToIndex;
  }
  var->numValues = numValues;
  return 1;
}


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

  Synopsis    [Expands the range of a variable.]

  Description [Expands the range of a variable. Designed for the table 
  determinization routine.]

  SideEffects []

  SeeAlso     [Var_VariableReduceRange]

******************************************************************************/
boolean
Var_VariableExpandRange(
  Var_Variable_t *var,
  int numValues)
{
  if (numValues <= var->numValues){
    error_append("Error: A range can only be expanded.\n");
    return 0;
  }
  if (var->indexToValue != NIL(array_t)){
    int i;
    char *dummyName;

    for (i=var->numValues; i < numValues; i++){
      /* put empty strings for expanded range */
      dummyName = ALLOC(char,1);
      *dummyName = '\0';
      array_insert_last(char *,var->indexToValue,dummyName);
    }
  }
  var->numValues = numValues;
  return 1;
} 

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

  Synopsis    [Reduces the range of a variable.]

  Description [Reduces the range of a variable. Designed for Abstraction. If
  numValues is greater than the current range of var, then 
  Var_VariableExpandRange will be called and returned.]

  SideEffects []

  SeeAlso     [Var_VariableExpandRange]

******************************************************************************/
boolean
Var_VariableReduceRange(
  Var_Variable_t *var,
  int numValues)
{
  if(numValues > var->numValues){
    return Var_VariableExpandRange(var,numValues);
  }
  else if (var->indexToValue != NIL(array_t)){
    error_append("Error: Cannot reduce the range of a symbolic variable.\n");
    return 0;
  }

  var->numValues = numValues;
  return 1;
}

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

  Synopsis    [Allocates a new variable.]

  Description [Allocates a new variable. This function is typically
  invoked when a .inputs or a .outputs is encountered in the parser.
  The arguments of this function are a pointer to the hnode to which
  a new variable belongs to and a name of the variable. The name string
  is copied for internal use. The user is responsible for freeing
  the original string. The new variable is set to a binary variable
  without any symbolic value definition, i.e. it is defined as a binary
  enumerative variable. The user can update this range information
  by calling Var_VariableAddRangeInfo(). Returns a pointer to
  the variable if success. Otherwise, NIL(Var_Variable_t) is returned. ]

  SideEffects []

  SeeAlso     [Var_VariableAddRangeInfo Var_VariableFree]

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

Var_Variable_t *
Var_VariableAlloc(
  Hrc_Node_t *hnode, 
  char *name)
{
  Var_Variable_t *var;

  var = ALLOC(Var_Variable_t,1);
  var->name = util_strsav(name);
  var->hnode = hnode;
  if (hnode != NIL(Hrc_Node_t)){
    if ( Hrc_NodeAddVariable(hnode,var) == 0 ){
      Var_VariableFree(var);
      return NIL(Var_Variable_t);
    }
  }
  var->type = 0;
  /* assume that this is a Boolean variable w/o symbolic value definition */
  var->numValues = 2;
  var->numFanoutTables = 0;
  var->indexToValue = NIL(array_t);
  var->valueToIndex = NIL(st_table);
  var->typeIdentifier = NIL(char);
  var->undef = NIL(void);
  return var;
}

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

  Synopsis    [Frees a variable.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableAlloc]

******************************************************************************/
void
Var_VariableFree(Var_Variable_t *var)
{
  if (var->hnode != NIL(Hrc_Node_t)){
    Hrc_NodeDeleteVariable(var->hnode,var);
  }
  FREE(var->name);
  if (var->indexToValue != NIL(array_t)){
    _VarStringArrayFree(var->indexToValue);
  }
  if (var->valueToIndex != NIL(st_table)){
    st_free_table(var->valueToIndex);
  }
  if (var->typeIdentifier != NIL(char)){
    FREE(var->typeIdentifier);
  }
  FREE(var);
}

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

  Synopsis    [Duplicates a variable. ]

  Description [Duplicates a variable. The second argument hnode is a new hnode
  to which a duplicated variable belongs.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Var_Variable_t *
Var_VariableDup(
  Var_Variable_t *var,
  Hrc_Node_t *hnode)
{
  Var_Variable_t *varDup;

  varDup = Var_VariableAlloc(hnode,var->name);
  varDup->type = var->type;
  varDup->hnode = hnode;
  varDup->numFanoutTables = var->numFanoutTables;
  if (Var_VariableAddRangeInfo(varDup,var->numValues,var->indexToValue) == 0){
    return NIL(Var_Variable_t);
  }
  if (var->typeIdentifier != NIL(char)){
    varDup->typeIdentifier = util_strsav(var->typeIdentifier);
  }
  return varDup;
}

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

  Synopsis    [Returns a pointer to the name of a variable.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
char *
Var_VariableReadName(Var_Variable_t *var)
{
  return var->name;
}

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

  Synopsis    [Returns 1 if a variable is a primary input. Otherwise returns 0.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableSetPI]

******************************************************************************/
boolean
Var_VariableTestIsPI(Var_Variable_t *var)
{
  return (((var->type) & VarPI) ? 1:0);
}

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

  Synopsis    [Returns 1 if a variable is a primary output. Otherwise returns 0.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableSetPO]

******************************************************************************/
boolean
Var_VariableTestIsPO(Var_Variable_t *var)
{
  return (((var->type) & VarPO) ? 1:0);
}

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

  Synopsis    [Returns 1 if a variable is a present state variable. Otherwise returns 0.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableSetPS]

******************************************************************************/
boolean
Var_VariableTestIsPS(Var_Variable_t *var)
{
  return (((var->type) & VarPS) ? 1:0);
}

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

  Synopsis    [Returns 1 if a variable is a next state variable. Otherwise returns 0.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableSetNS]

******************************************************************************/
boolean
Var_VariableTestIsNS(Var_Variable_t *var)
{
  return (((var->type) & VarNS) ? 1:0);
}

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

  Synopsis    [Returns 1 if a variable is a subcircuit input. Otherwise returns 0.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableSetSI]

******************************************************************************/
boolean
Var_VariableTestIsSI(Var_Variable_t *var)
{
  return (((var->type) & VarSI) ? 1:0);
}

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

  Synopsis    [Returns 1 if a variable is a subcircuit output. Otherwise returns 0.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableSetSO]

******************************************************************************/
boolean
Var_VariableTestIsSO(Var_Variable_t *var)
{
  return (((var->type) & VarSO) ? 1:0);
}

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

  Synopsis    [Returns 1 if the value type of a variable is symbolic and 0
  otherwise.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableTestIsEnumerative]

******************************************************************************/
boolean
Var_VariableTestIsSymbolic(Var_Variable_t *var)
{
  if (var->indexToValue != NIL(array_t)){
    return 1;
  }
  return 0;
}

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

  Synopsis    [Returns 1 if the value type of a variable is enumerative and 0
  otherwise.]

  Description []

  SideEffects []

  SeeAlso     [Var_VariableTestIsSymbolic]

******************************************************************************/
boolean
Var_VariableTestIsEnumerative(Var_Variable_t *var)
{
  if (var->indexToValue == NIL(array_t)){
    return 1;
  }
  return 0;
}

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

  Synopsis    [Returns 1 if a variable is enumerative *and* a value is
  in the range of the variable. Returns 0 otherwise.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
Var_VariableTestIsValueInRange(
  Var_Variable_t *var,
  int value)
{
  if (var->indexToValue != NIL(array_t)){
    return 0;
  }
  if (value >= 0 && value < var->numValues){
    return 1;
  }
  return 0;
}

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

  Synopsis    [Returns the number of values a variable can take.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Var_VariableReadNumValues(Var_Variable_t *var)
{
  return var->numValues;
}

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

  Synopsis    [Returns the number of fanout tables.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Var_VariableReadNumFanoutTables(Var_Variable_t *var)
{
  return var->numFanoutTables;
}

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

  Synopsis    [Increments the number of fanout tables.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Var_VariableIncrementNumFanoutTables(Var_Variable_t *var)
{
  (var->numFanoutTables)++;
}

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

  Synopsis    [Resets the number of fanout tables.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Var_VariableResetNumFanoutTables(
  Var_Variable_t* var)
{
  var->numFanoutTables = 0;
}


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

  Synopsis    [Returns the name of the symbolic value associated with an integer index.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
char *
Var_VariableReadSymbolicValueFromIndex(
  Var_Variable_t *var,
  int i)
{
  assert(var->indexToValue != NIL(array_t));
  return array_fetch(char *,var->indexToValue,i);
}

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

  Synopsis    [Returns the integer index associated with the name of a symbolic value.]

  Description [Returns the integer index associated with a symbolic value. If
  a given symbolic name is not valid, the routine returns -1.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Var_VariableReadIndexFromSymbolicValue(
  Var_Variable_t *var,
  char *symbolicValue)
{
  int  isFound;
  int  index;

  assert(var->valueToIndex != NIL(st_table));
  isFound = st_lookup_int(var->valueToIndex,symbolicValue,&index);
  return( isFound ? index : -1);
}

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

  Synopsis    [Returns the hnode to which a variable belongs.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
Hrc_Node_t *
Var_VariableReadHnode(Var_Variable_t *var)
{
  return var->hnode;
}

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

  Synopsis    [Returns a pointer to the type identifier of a variable.]

  Description [Reads the type identifier for the variable.  Type identifiers are
  defined in blif-mv using the .type statement. 
  Example: .type color red white blue 
           .mv flag_colors type=color]

  SideEffects []

  SeeAlso     []

******************************************************************************/
char *
Var_VariableReadTypeIdentifier(Var_Variable_t *var)
{
  return var->typeIdentifier;
}


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

  Synopsis    [Returns a pointer to the user field of a variable.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void *
Var_VariableReadUndef(Var_Variable_t *var)
{
  return var->undef;
}

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

  Synopsis    [Changes the name of a variable.]

  Description [Changes the name of a variable. Returns 1 if success, otherwise
  returns 0.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
Var_VariableChangeName(
  Var_Variable_t *var,
  char *name)
{
  if (var->hnode != NIL(Hrc_Node_t)){
    if (Hrc_NodeDeleteVariable(var->hnode,var) == 0){
      /* this variable should have been in the hnode */
      return 0;
    }
  }
  FREE(var->name);
  var->name = util_strsav(name); 
  if (var->hnode != NIL(Hrc_Node_t)){
    if (Hrc_NodeAddVariable(var->hnode,var) == 0){
      /* there is a node with the new name in the hnode already */
      return 0;
    }
  }
  return 1;
}

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

  Synopsis    [Sets the PI-field of a variable.]

  Description [Sets the PI-field of a variable. Returns 1 upon success. 
  Returns 0 if the variable is
  already set as a PI. Returns -1 if a type error occurs. This function is used when 
  a variable is defined in .inputs *and* the variable is already declared
  in .mv. ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsPI]

******************************************************************************/
int
Var_VariableSetPI(Var_Variable_t *var)
{
  return _VarVariableSetType(var,VarPI);
}

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

  Synopsis    [Sets the PO-field of a variable.]

  Description [Sets the PO-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is
  already set as a PO. Returns -1 if a type error occurs. This function is used when
  a variable is defined in .outputs *and* the variable is already declared
  in .mv. ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsPO]

******************************************************************************/
int
Var_VariableSetPO(Var_Variable_t *var)
{
  return _VarVariableSetType(var,VarPO);
}

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

  Synopsis    [Sets the PS-field of a variable.]

  Description [Sets the PS-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is
  already set as a PS. Returns -1 if a type error occurs. This function is used when
  a variable is defined in .latch *and* the variable is already declared
  in .mv. ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsPS]

******************************************************************************/
int
Var_VariableSetPS(Var_Variable_t *var)
{
  return _VarVariableSetType(var,VarPS);
}

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

  Synopsis    [Sets the NS-field of a variable.]

  Description [Sets the NS-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is
  already set as an NS. Returns -1 if a type error occurs. This function is used when
  a variable is defined in .latch *and* the variable is already declared
  in .mv. ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsNS]

******************************************************************************/
int
Var_VariableSetNS(Var_Variable_t *var)
{
  return _VarVariableSetType(var,VarNS);
}

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

  Synopsis    [Sets the SI-field of a variable.]

  Description [Sets the SI-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is
  already set as an SI. Returns -1 if a type error occurs.]

  SideEffects []

  SeeAlso     [Var_VariableTestIsSI]

******************************************************************************/
int
Var_VariableSetSI(Var_Variable_t *var)
{
  return _VarVariableSetType(var,VarSI);
}

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

  Synopsis    [Sets the SO-field of a variable.]

  Description [Sets the SO-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is
  already set as an SO. Returns -1 if a type error occurs.]

  SideEffects []

  SeeAlso     [Var_VariableTestIsSO]

******************************************************************************/
int
Var_VariableSetSO(Var_Variable_t *var)
{
  return _VarVariableSetType(var,VarSO);
}

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

  Synopsis    [Resets the PI-field of a variable.]

  Description [Resets the PI-field of a variable. Returns 1 upon success. 
  Returns 0 if the variable is not set to PI.
  ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsPI]

******************************************************************************/
int
Var_VariableResetPI(Var_Variable_t *var)
{
  return _VarVariableResetType(var,VarPI);
}

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

  Synopsis    [Resets the PO-field of a variable.]

  Description [Resets the PO-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is not set to PO.
  ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsPO]

******************************************************************************/
int
Var_VariableResetPO(Var_Variable_t *var)
{
  return _VarVariableResetType(var,VarPO);
}

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

  Synopsis    [Resets the PS-field of a variable.]

  Description [Resets the PS-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is not set to PS.
  ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsPS]

******************************************************************************/
int
Var_VariableResetPS(Var_Variable_t *var)
{
  return _VarVariableResetType(var,VarPS);
}

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

  Synopsis    [Resets the NS-field of a variable.]

  Description [Resets the NS-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is not set to NS.
  ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsNS]

******************************************************************************/
int
Var_VariableResetNS(Var_Variable_t *var)
{
  return _VarVariableResetType(var,VarNS);
}

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

  Synopsis    [Resets the SI-field of a variable.]

  Description [Resets the SI-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is not set to SI.
  ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsSI]

******************************************************************************/
int
Var_VariableResetSI(Var_Variable_t *var)
{
  return _VarVariableResetType(var,VarSI);
}

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

  Synopsis    [Resets the SO-field of a variable.]

  Description [Resets the SO-field of a variable. Returns 1 upon success.
  Returns 0 if the variable is not set to SO.
  ]

  SideEffects []

  SeeAlso     [Var_VariableTestIsSO]

******************************************************************************/
int
Var_VariableResetSO(Var_Variable_t *var)
{
  return _VarVariableResetType(var,VarSO);
}

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

  Synopsis    [Resets all the types of a variable.]

  Description [Resets all the types of a variable.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Var_VariableResetAllTypes(Var_Variable_t *var)
{
  var->type = 0;
}


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

  Synopsis    [Sets the type identifier for the variable.]

  Description [Sets the type identifier for the variable.  Type identifiers are
  defined in blif-mv using the .type statement.  
  Example: .type color red white blue
           .mv flag_colors type=color]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Var_VariableSetTypeIdentifier(
  Var_Variable_t *var,
  char *typeIdentifier)
{
  if (var->typeIdentifier != NIL(char)){
    FREE(var->typeIdentifier);
  }
  var->typeIdentifier = util_strsav(typeIdentifier);
}

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

  Synopsis    [Given two variables, checks to see if the two variables refer
  to the identical signal once a hierarchy is flattened out. Returns 1 if 
  they are identical. Otherwise returns 0. If the two variables do not
  belong to the same hierarchy manager, it also returns 0 with an error
  message sent to error_string.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
Var_VariablesTestIdentical(
  Var_Variable_t *var1, 
  Var_Variable_t *var2)
{
  Hrc_Manager_t *hmgr1, *hmgr2;
  Hrc_Node_t *hnode1, *hnode2, *rootNode;
  Var_Variable_t *varCanonical1, *varCanonical2;

  hnode1 = Var_VariableReadHnode(var1);
  hnode2 = Var_VariableReadHnode(var2);
  hmgr1 = Hrc_NodeReadManager(hnode1);
  hmgr2 = Hrc_NodeReadManager(hnode2);

  if (hmgr1 != hmgr2){
    error_append("Error: Variables ");
    error_append(Var_VariableReadName(var1));
    error_append(" and ");
    error_append(Var_VariableReadName(var2));
    error_append(" are not under the same manager.\n");
    return 0;
  }
  /* if two variables reside in the same hnode */
  if (hnode1 == hnode2){
    if (var1 == var2){
      return 1;
    }
    return 0;
  }

  /* otherwise */
  rootNode = Hrc_ManagerReadRootNode(hmgr1);
 
  varCanonical1 = Hrc_VariableFindActualFromFormal(hnode1,var1,rootNode);
  varCanonical2 = Hrc_VariableFindActualFromFormal(hnode2,var2,rootNode);
  if (varCanonical1 == varCanonical2){
    return 1;
  }
  return 0;
}


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

  Synopsis    [Checks to see if two variables are defined over the same domain.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
Var_VariablesTestHaveSameDomain(
  Var_Variable_t *var1, 
  Var_Variable_t *var2)
{
  array_t *indexToValue1, *indexToValue2;
  char *value1, *value2;
  int i;

  if (var1->numValues != var2->numValues)
    return 0;
  indexToValue1 = var1->indexToValue;
  indexToValue2 = var2->indexToValue;
  if (indexToValue1 == NIL(array_t) || indexToValue2 == NIL(array_t))
    return 1;
  for (i=0; i < array_n(indexToValue1); i++){
    value1 = array_fetch(char *,indexToValue1,i);
    value2 = array_fetch(char *,indexToValue2,i);
    if (strcmp(value1,value2)){
      return 0;    
    }
  }
  return 1;
}

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

  Synopsis    [Checks to see if there is no type violation. Returns 1 if
  no violation exists. Otherwise returns 0.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
Var_VariableTestTypeConsistency(Var_Variable_t *var)
{
  /* checking PI/PO */
  if ((var->type & 03) == 03){
    error_append("Error: Variable ");
    error_append(Var_VariableReadName(var));
    error_append(" is of type PI/PO.\n");
    return 0;
  }
  /* checking PI/PS */
  if ((var->type & 05) == 05){
    error_append("Error: Variable ");
    error_append(Var_VariableReadName(var));
    error_append(" is of type PI/PS.\n");
    return 0;
  }
  /* checking PI/SO */
  if ((var->type & 041) == 041){
    error_append("Error: Variable ");
    error_append(Var_VariableReadName(var));
    error_append(" is of type PI/SO.\n");
    return 0;
  }
  return 1;
}

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

  Synopsis    [Checks to see if two variables have the same type identifier]

  Description [Returns 1 if var1 and var2 have the same type identifier,
  0 otherwise.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
Var_VariablesTestHaveSameTypeIdentifier(
  Var_Variable_t *var1,
  Var_Variable_t *var2)
{
  if (var1->typeIdentifier == NIL(char) && var2->typeIdentifier == NIL(char)){
    return 1;
  }
  if (var1->typeIdentifier == NIL(char) || var2->typeIdentifier == NIL(char)){
    return 0;
  }
  if (strcmp(var1->typeIdentifier,var2->typeIdentifier) == 0 ){
    return 1;
  }
  return 0;
}


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

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

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

  Synopsis    [Sets the type field of a variable. Returns 0 if the variable is
  already set as a given type. If the variable is newly set to the type, it 
  returns 1. If a type violation occurs after this setting, -1 is returned.
  Type can be set either VarPI, VarPO, VarPS, VarNS, VarSI and VarSO.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
_VarVariableSetType(Var_Variable_t *var,int type)
{
/*
  if (var->type & type){
    error_append("Warning: Variable ");
    error_append(Var_VariableReadName(var));
    error_append(" is already set to ");
    error_append(_VarTypeDecode(type));
    error_append(".\n");
     return 0;
  }
*/
  var->type |= type;
  if (Var_VariableTestTypeConsistency(var) == 0){
     return -1;
  }
  return 1;
}

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

  Synopsis    [Resets the type field of a variable. Returns 0 if the variable is
  not set as a given type, i.e. there is no need for resetting the type. 
  Otherwise, returns 1. 
  Type can be set either VarPI, VarPO, VarPS, VarNS, VarSI and VarSO.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
_VarVariableResetType(Var_Variable_t *var,int type)
{
/*
  if (var->type & type){
    error_append("Warning: Variable ");
    error_append(Var_VariableReadName(var));
    error_append(" is already set to ");
    error_append(_VarTypeDecode(type));
    error_append(".\n");
     return 0;
  }
*/
  if ((var->type & type) == 0){
    return 0;
  }
  var->type &= ~type;
  return 1;
}

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

  Synopsis    [Returns the character string corresponding to a type encoded
               in an integer. Note that SI and SO are filtered out.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static char *
_VarTypeDecode(int type)
{
  /* suppress information on SI/SO for simplicity */
  type &= 017;
  switch(type){
    case 00:
      return "Internal";
    case 01: 
      return "PI";
    case 02: 
      return "PO";
    case 03: 
      error_append("Error: Strange type PI/PO.\n");
      return "PI/PO";
    case 04: 
      return "PS";
    case 05:
      error_append("Error: Strange type PI/PS.\n");
      return "PI/PS";
    case 06:
      return "PO/PS";
    case 07:
      error_append("Error: Strange type PI/PO/PS.\n");
      return "PI/PO/PS";
    case 010: 
      return "NS";
    case 011:
      return "PI/NS";
    case 012:
      return "PO/NS";
    case 013:
      error_append("Error: Strange type PI/PO/NS.\n");
      return "PI/PO/NS";
    case 014:
      return "PS/NS";
    case 015:
      error_append("Error: Strange type PI/PS/NS.\n");
      return "PI/PS/NS";
    case 016:
      return "PO/PS/NS";
    case 017:
      error_append("Error: Strange type PI/PO/PS/NS.\n");
      return "PI/PO/PS/NS";
    default: 
      fail("Strange type in VarTypeDecode().\n");
      return NIL(char); /* not reached */
  }
}

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

  Synopsis    [Duplicates an array of strings.]

  Description [Duplicates an array of strings. Strings themselves are also
  copied over to the new array.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static array_t *
_VarStringArrayDup(array_t *array)
{
  int i;
  char *symbol,*newSymbol;
  array_t *newArray;

  newArray = array_alloc(char *,0);
  for (i=0; i < array_n(array); i++) {
    symbol = array_fetch(char *, array, i);
    newSymbol = util_strsav(symbol);
    array_insert_last(char *,newArray,newSymbol);
  }
  return newArray;
}

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

  Synopsis    [Frees an array of strings.]

  Description [Frees an array of strings. Strings themselves are also
  freed.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
_VarStringArrayFree(array_t *array)
{
  int i;
  char *symbol;

  for (i=0; i < array_n(array); i++) {
    symbol = array_fetch(char *, array, i);
    FREE(symbol);
  }
  array_free(array);
}