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

  FileName    [imgTfmUtil.c]

  PackageName [img]

  Synopsis    [Routines for image computation using transition function method.]

  SeeAlso     []

  Author      [In-Ho Moon]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado.
  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 COLORADO 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
  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF COLORADO 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 COLORADO HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

******************************************************************************/
#include "imgInt.h"

static char rcsid[] UNUSED = "$Id: imgTfmUtil.c,v 1.23 2005/04/23 14:30:55 jinh Exp $";

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

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

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

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

static	double	*signatures; /* used in finding dependent variables */

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

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

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

static int SignatureCompare(int *ptrX, int *ptrY);
static int CompareBddPointer(const void *e1, const void *e2);

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


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


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


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

  Synopsis    [Constrains a function vector with respect to a constraint.]

  Description [Constrains a function vector with respect to a constraint.]

  SideEffects []

******************************************************************************/
void
ImgVectorConstrain(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint,
		   array_t *relationArray, array_t **newVector, mdd_t **cube,
		   array_t **newRelationArray, mdd_t **cofactorCube,
		   mdd_t **abstractCube, boolean singleVarFlag)
{
  mdd_t			*new_, *res, *old, *tmp;
  ImgComponent_t	*comp, *comp1;
  array_t		*vector1;
  int			i, index;
  int			dynStatus, dynOff;
  bdd_reorder_type_t	dynMethod;
  st_table		*equivTable;
  int			*ptr, *regularPtr;
  int			n, pos;
  mdd_t			*cofactor, *abstract, *nsVar, *constIntermediate;
  array_t		*tmpRelationArray;
  int			size;

  old = mdd_one(info->manager);
  vector1 = array_alloc(ImgComponent_t *, 0);
  dynStatus = 0;

  if (singleVarFlag)
    dynOff = 0;
  else
    dynOff = 1;
  if (dynOff) {
    dynStatus = bdd_reordering_status(info->manager, &dynMethod);
    if (dynStatus != 0)
      bdd_dynamic_reordering_disable(info->manager);
  }

  if (relationArray) {
    cofactor = mdd_one(info->manager);
    abstract = mdd_one(info->manager);
  } else {
    cofactor = NIL(mdd_t);
    abstract = NIL(mdd_t);
  }

  if (info->nIntermediateVars) {
    size = ImgVectorFunctionSize(vector);
    if (size == array_n(vector))
      constIntermediate = NIL(mdd_t);
    else
      constIntermediate = mdd_one(info->manager);
  } else
    constIntermediate = NIL(mdd_t);

  n = 0;
  equivTable = st_init_table(st_ptrcmp, st_ptrhash);
  index = (int)bdd_top_var_id(constraint);
  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (!bdd_is_tautology(constraint, 1)) {
      if (singleVarFlag) {
	if (comp->support[index])
	  res = bdd_cofactor(comp->func, constraint);
	else
	  res = mdd_dup(comp->func);
      } else
	res = bdd_cofactor(comp->func, constraint);
    } else
      res = mdd_dup(comp->func);
    if (bdd_is_tautology(res, 1)) {
      if (comp->intermediate) {
	tmp = constIntermediate;
	constIntermediate = mdd_and(tmp, comp->var, 1, 1);
	mdd_free(tmp);
	mdd_free(res);
	continue;
      }
      new_ = mdd_and(comp->var, old, 1, 1);
      mdd_free(old);
      mdd_free(res);
      old = new_;
      if (cofactor) {
	nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	tmp = cofactor;
	cofactor = mdd_and(tmp, nsVar, 1, 1);
	mdd_free(tmp);
	mdd_free(nsVar);
      }
    } else if (bdd_is_tautology(res, 0)) {
      if (comp->intermediate) {
	tmp = constIntermediate;
	constIntermediate = mdd_and(tmp, comp->var, 1, 0);
	mdd_free(tmp);
	mdd_free(res);
	continue;
      }
      new_ = mdd_and(comp->var, old, 0, 1);
      mdd_free(old);
      mdd_free(res);
      old = new_;
      if (cofactor) {
	nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	tmp = cofactor;
	cofactor = mdd_and(tmp, nsVar, 1, 0);
	mdd_free(tmp);
	mdd_free(nsVar);
      }
    } else {
      if (comp->intermediate) {
	comp1 = ImgComponentAlloc(info);
	comp1->var = mdd_dup(comp->var);
	comp1->func = res;
	comp1->intermediate = 1;
	if (mdd_equal(res, comp->func))
	  ImgSupportCopy(info, comp1->support, comp->support);
	else
	  ImgComponentGetSupport(comp1);
	array_insert_last(ImgComponent_t *, vector1, comp1);
	n++;
	continue;
      }
      ptr = (int *)bdd_pointer(res);
      regularPtr = (int *)((unsigned long)ptr & ~01);
      if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
	comp1 = array_fetch(ImgComponent_t *, vector1, pos);
	if (mdd_equal(res, comp1->func))
	  tmp = mdd_xnor(comp->var, comp1->var);
	else
	  tmp = mdd_xor(comp->var, comp1->var);
	new_ = mdd_and(tmp, old, 1, 1);
	mdd_free(tmp);
	mdd_free(old);
	mdd_free(res);
	old = new_;
	if (abstract) {
	  nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	  tmp = abstract;
	  abstract = mdd_and(tmp, nsVar, 1, 1);
	  mdd_free(tmp);
	  mdd_free(nsVar);
	}
      } else {
	comp1 = ImgComponentAlloc(info);
	comp1->var = mdd_dup(comp->var);
	comp1->func = res;
	if (mdd_equal(res, comp->func))
	  ImgSupportCopy(info, comp1->support, comp->support);
	else
	  ImgComponentGetSupport(comp1);
	array_insert_last(ImgComponent_t *, vector1, comp1);
	st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
	n++;
      }
    }
  }
  st_free_table(equivTable);

  if (dynOff && dynStatus != 0) {
    bdd_dynamic_reordering(info->manager, dynMethod,
			   BDD_REORDER_VERBOSITY_DEFAULT);
  }

  if (constIntermediate) {
    if (!bdd_is_tautology(constIntermediate, 1)) {
      mdd_t	*tmpCofactor, *tmpAbstract;

      if (relationArray) {
	vector1 = ImgComposeConstIntermediateVars(info, vector1,
						  constIntermediate,
						  &tmpCofactor, &tmpAbstract,
						  &old, NIL(mdd_t *));
	if (!bdd_is_tautology(tmpCofactor, 1)) {
	  tmp = cofactor;
	  cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
	  mdd_free(tmp);
	}
	mdd_free(tmpCofactor);
	if (!bdd_is_tautology(tmpAbstract, 1)) {
	  tmp = abstract;
	  abstract = mdd_and(tmp, tmpAbstract, 1, 1);
	  mdd_free(tmp);
	}
	mdd_free(tmpAbstract);
	tmp = cofactor;
	cofactor = mdd_and(tmp, constIntermediate, 1, 1);
	mdd_free(tmp);
      } else {
	vector1 = ImgComposeConstIntermediateVars(info, vector1,
						  constIntermediate,
						  NIL(mdd_t *), NIL(mdd_t *),
						  &old, NIL(mdd_t *));
      }
    }
    mdd_free(constIntermediate);
  }

  if (info->option->sortVectorFlag)
    array_sort(vector1, CompareBddPointer);

  if (relationArray && newRelationArray) {
    if (singleVarFlag) {
      *newRelationArray = relationArray;
      tmp = cofactor;
      cofactor = mdd_and(tmp, constraint, 1, 1);
      mdd_free(tmp);
    } else
      *newRelationArray = ImgGetConstrainedRelationArray(info, relationArray,
							 constraint);
  }
  if (cofactorCube && abstractCube) {
    if (cofactor)
      *cofactorCube = cofactor;
    if (abstract)
      *abstractCube = abstract;
  } else {
    if (cofactor) {
      if (bdd_is_tautology(cofactor, 1))
	mdd_free(cofactor);
      else {
	tmpRelationArray = *newRelationArray;
	*newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray,
							  cofactor);
	mdd_free(cofactor);
	if (tmpRelationArray != relationArray)
	  mdd_array_free(tmpRelationArray);
      }
    }
    if (abstract) {
      if (bdd_is_tautology(abstract, 1))
	mdd_free(abstract);
      else {
	tmpRelationArray = *newRelationArray;
	*newRelationArray = ImgGetAbstractedRelationArray(info->manager,
							  tmpRelationArray,
							abstract);
	mdd_free(abstract);
	if (tmpRelationArray != relationArray)
	  mdd_array_free(tmpRelationArray);
      }
    }
  }

  *newVector = vector1;
  *cube = old;
}


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

  Synopsis    [Minimizes a function vector and a from set with respect to an
  essential cube.]

  Description [Minimizes a function vector and a from set with respect to an
  essential cube. This function is called during eliminating dependent
  variables.]

  SideEffects []

******************************************************************************/
mdd_t *
ImgVectorMinimize(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint,
		  mdd_t *from, array_t *relationArray, array_t **newVector,
		  mdd_t **cube, array_t **newRelationArray,
		  mdd_t **cofactorCube, mdd_t **abstractCube)
{
  mdd_t			*new_, *res, *old, *tmp, *newFrom;
  ImgComponent_t	*comp, *comp1;
  array_t		*vector1;
  int			i;
  st_table		*equivTable;
  int			*ptr, *regularPtr;
  int			n, pos;
  mdd_t			*cofactor, *abstract, *nsVar, *constIntermediate;
  array_t		*tmpRelationArray;
  int			size;

  if (from)
    newFrom = mdd_dup(from);
  else
    newFrom = NIL(mdd_t);
  if (cube)
    old = mdd_one(info->manager);
  else
    old = NIL(mdd_t);
  assert(newVector)
  vector1 = array_alloc(ImgComponent_t *, 0);

  if (relationArray) {
    cofactor = mdd_one(info->manager);
    abstract = mdd_one(info->manager);
  } else {
    cofactor = NIL(mdd_t);
    abstract = NIL(mdd_t);
  }

  if (info->nIntermediateVars) {
    size = ImgVectorFunctionSize(vector);
    if (size == array_n(vector))
      constIntermediate = NIL(mdd_t);
    else
      constIntermediate = mdd_one(info->manager);
  } else
    constIntermediate = NIL(mdd_t);

  n = 0;
  equivTable = st_init_table(st_ptrcmp, st_ptrhash);
  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    res = bdd_minimize(comp->func, constraint);
    if (bdd_is_tautology(res, 1)) {
      if (comp->intermediate) {
	tmp = constIntermediate;
	constIntermediate = mdd_and(tmp, comp->var, 1, 1);
	mdd_free(tmp);
	mdd_free(res);
	continue;
      }
      if (newFrom) {
	tmp = newFrom;
	newFrom = bdd_cofactor(tmp, comp->var);
	mdd_free(tmp);
      }
      if (old) {
	new_ = mdd_and(comp->var, old, 1, 1);
	mdd_free(old);
	mdd_free(res);
	old = new_;
      }
      if (cofactor) {
	nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	tmp = cofactor;
	cofactor = mdd_and(tmp, nsVar, 1, 1);
	mdd_free(tmp);
	mdd_free(nsVar);
      }
    } else if (bdd_is_tautology(res, 0)) {
      if (comp->intermediate) {
	tmp = constIntermediate;
	constIntermediate = mdd_and(tmp, comp->var, 1, 0);
	mdd_free(tmp);
	mdd_free(res);
	continue;
      }
      if (newFrom) {
	tmp = newFrom;
	new_ = mdd_not(comp->var);
	newFrom = bdd_cofactor(tmp, new_);
	mdd_free(tmp);
	mdd_free(new_);
      }
      if (old) {
	new_ = mdd_and(comp->var, old, 0, 1);
	mdd_free(old);
	mdd_free(res);
	old = new_;
      }
      if (cofactor) {
	nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	tmp = cofactor;
	cofactor = mdd_and(tmp, nsVar, 1, 0);
	mdd_free(tmp);
	mdd_free(nsVar);
      }
    } else {
      if (comp->intermediate) {
	comp1 = ImgComponentAlloc(info);
	comp1->var = mdd_dup(comp->var);
	comp1->func = res;
	comp1->intermediate = 1;
	if (mdd_equal(res, comp->func))
	  ImgSupportCopy(info, comp1->support, comp->support);
	else
	  ImgComponentGetSupport(comp1);
	array_insert_last(ImgComponent_t *, vector1, comp1);
	n++;
	continue;
      }
      ptr = (int *)bdd_pointer(res);
      regularPtr = (int *)((unsigned long)ptr & ~01);
      if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
	comp1 = array_fetch(ImgComponent_t *, vector1, pos);
	if (newFrom) {
	  if (mdd_equal(res, comp1->func)) {
	    tmp = newFrom;
	    newFrom = bdd_compose(tmp, comp->var, comp1->var);
	    mdd_free(tmp);
	  } else {
	    tmp = newFrom;
	    new_ = mdd_not(comp1->var);
	    newFrom = bdd_compose(tmp, comp->var, new_);
	    mdd_free(tmp);
	    mdd_free(new_);
	  }
	}
	if (old) {
	  if (mdd_equal(res, comp1->func))
	    tmp = mdd_xnor(comp->var, comp1->var);
	  else
	    tmp = mdd_xor(comp->var, comp1->var);
	  new_ = mdd_and(tmp, old, 1, 1);
	  mdd_free(tmp);
	  mdd_free(old);
	  old = new_;
	}
	mdd_free(res);
	if (abstract) {
	  nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	  tmp = abstract;
	  abstract = mdd_and(tmp, nsVar, 1, 1);
	  mdd_free(tmp);
	  mdd_free(nsVar);
	}
      } else {
	comp1 = ImgComponentAlloc(info);
	comp1->var = mdd_dup(comp->var);
	comp1->func = res;
	if (mdd_equal(res, comp->func))
	  ImgSupportCopy(info, comp1->support, comp->support);
	else
	  ImgComponentGetSupport(comp1);
	array_insert_last(ImgComponent_t *, vector1, comp1);
	st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
	n++;
      }
    }
  }
  st_free_table(equivTable);

  if (constIntermediate) {
    if (!bdd_is_tautology(constIntermediate, 1)) {
      mdd_t	*tmpCofactor, *tmpAbstract;

      if (relationArray) {
	vector1 = ImgComposeConstIntermediateVars(info, vector1,
						  constIntermediate,
						  &tmpCofactor, &tmpAbstract,
						  &old, NIL(mdd_t *));
	if (!bdd_is_tautology(tmpCofactor, 1)) {
	  tmp = cofactor;
	  cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
	  mdd_free(tmp);
	}
	mdd_free(tmpCofactor);
	if (!bdd_is_tautology(tmpAbstract, 1)) {
	  tmp = abstract;
	  abstract = mdd_and(tmp, tmpAbstract, 1, 1);
	  mdd_free(tmp);
	}
	mdd_free(tmpAbstract);
	tmp = cofactor;
	cofactor = mdd_and(tmp, constIntermediate, 1, 1);
	mdd_free(tmp);
      } else {
	vector1 = ImgComposeConstIntermediateVars(info, vector1,
						  constIntermediate,
						  NIL(mdd_t *), NIL(mdd_t *),
						  &old, NIL(mdd_t *));
      }
    }
    mdd_free(constIntermediate);
  }

  if (info->option->sortVectorFlag)
    array_sort(vector1, CompareBddPointer);

  if (newRelationArray)
    *newRelationArray = relationArray;
  if (cofactorCube && abstractCube) {
    if (cofactor) {
      if (bdd_is_tautology(cofactor, 1)) {
	*cofactorCube = mdd_dup(constraint);
	mdd_free(cofactor);
      } else {
	tmp = cofactor;
	cofactor = mdd_and(tmp, constraint, 1, 1);
	mdd_free(tmp);
	*cofactorCube = cofactor;
      }
    }
    if (abstract)
      *abstractCube = abstract;
  } else {
    if (cofactor) {
      if (bdd_is_tautology(cofactor, 1))
	mdd_free(cofactor);
      else {
	tmp = cofactor;
	cofactor = mdd_and(tmp, constraint, 1, 1);
	mdd_free(tmp);
	if (newRelationArray) {
	  *newRelationArray = ImgGetCofactoredRelationArray(relationArray,
							    cofactor);
	} else
	  ImgCofactorRelationArray(relationArray, cofactor);
	mdd_free(cofactor);
      }
    }
    if (abstract) {
      if (bdd_is_tautology(abstract, 1))
	mdd_free(abstract);
      else {
	if (newRelationArray) {
	  tmpRelationArray = *newRelationArray;
	  *newRelationArray = ImgGetAbstractedRelationArray(info->manager,
							    tmpRelationArray,
							    abstract);
	  if (tmpRelationArray != relationArray)
	    mdd_array_free(tmpRelationArray);
	} else
	  ImgAbstractRelationArray(info->manager, relationArray, abstract);
	mdd_free(abstract);
      }
    }
  }

  if (*newVector == vector)
    ImgVectorFree(vector);
  *newVector = vector1;
  if (cube)
    *cube = old;

  return(newFrom);
}


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

  Synopsis    [Frees a function vector.]

  Description [Frees a function vector.]

  SideEffects []

******************************************************************************/
void
ImgVectorFree(array_t *vector)
{
  int    		i;
  ImgComponent_t	*comp;

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    ImgComponentFree(comp);
  }
  array_free(vector);
}


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

  Synopsis    [Returns the number of functions in a vector.]

  Description [Returns the number of functions in a vector. Excludes the
  number of intermediate functions.]

  SideEffects []

******************************************************************************/
int
ImgVectorFunctionSize(array_t *vector)
{
  ImgComponent_t	*comp;
  int			i, size;

  size = 0;
  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (!comp->intermediate)
      size++;
  }

  return(size);
}


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

  Synopsis    [Returns the shared BDD size of a vector.]

  Description [Returns the shared BDD size of a vector.]

  SideEffects []

******************************************************************************/
long
ImgVectorBddSize(array_t *vector)
{
  array_t		*nodeArray;
  ImgComponent_t	*comp;
  int			i, size;

  nodeArray = array_alloc(mdd_t *, 0);
  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    array_insert_last(mdd_t *, nodeArray, comp->func);
  }
  size = bdd_size_multiple(nodeArray);
  array_free(nodeArray);

  return(size);
}


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

  Synopsis    [Copies a vector.]

  Description [Copies a vector.]

  SideEffects []

******************************************************************************/
array_t *
ImgVectorCopy(ImgTfmInfo_t *info, array_t *vector)
{
  array_t		*newVector;
  ImgComponent_t	*comp, *newComp;
  int			i;

  newVector = array_alloc(ImgComponent_t *, 0);
  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    newComp = ImgComponentCopy(info, comp);
    array_insert_last(ImgComponent_t *, newVector, newComp);
  }
  return(newVector);
}


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

  Synopsis    [Allocates a component.]

  Description [Allocates a component.]

  SideEffects []

******************************************************************************/
ImgComponent_t *
ImgComponentAlloc(ImgTfmInfo_t *info)
{
  ImgComponent_t	*comp;

  comp = ALLOC(ImgComponent_t, 1);
  memset(comp, 0, sizeof(ImgComponent_t));
  comp->support = ALLOC(char, info->nVars);
  ImgSupportClear(info, comp->support);
  comp->id = info->nComponents++;
  return(comp);
}


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

  Synopsis    [Copies a component]

  Description [Copies a component]

  SideEffects []

******************************************************************************/
ImgComponent_t *
ImgComponentCopy(ImgTfmInfo_t *info, ImgComponent_t *comp)
{
  ImgComponent_t	*newComp;

  newComp = ImgComponentAlloc(info);
  newComp->func = mdd_dup(comp->func);
  newComp->var = mdd_dup(comp->var);
  ImgSupportCopy(info, newComp->support, comp->support);
  newComp->intermediate = comp->intermediate;
  return(newComp);
}


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

  Synopsis    [Frees a component.]

  Description [Frees a component.]

  SideEffects []

******************************************************************************/
void
ImgComponentFree(ImgComponent_t *comp)
{
  if (comp->func)
    mdd_free(comp->func);
  if (comp->var != NULL)
    mdd_free(comp->var);
  FREE(comp->support);
  FREE(comp);
}


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

  Synopsis    [Gets the supports of a component.]

  Description [Gets the supports of a component.]

  SideEffects []

******************************************************************************/
void
ImgComponentGetSupport(ImgComponent_t *comp)
{
  int		index;
  var_set_t	*supportVarSet;

  supportVarSet = bdd_get_support(comp->func);
  for (index = 0; index < supportVarSet->n_elts; index++) {
    if (var_set_get_elt(supportVarSet, index) == 1)
      comp->support[index] = 1;
  }
  var_set_free(supportVarSet);
}


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

  Synopsis    [Copies the supports of a component.]

  Description [Copies the supports of a component. Here support is an array
  of char.]

  SideEffects []

******************************************************************************/
void
ImgSupportCopy(ImgTfmInfo_t *info, char *dsupport, char *ssupport)
{
  memcpy(dsupport, ssupport, sizeof(char) * info->nVars);
}


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

  Synopsis    [Clears a support array.]

  Description [Clears a support array.]

  SideEffects []

******************************************************************************/
void
ImgSupportClear(ImgTfmInfo_t *info, char *support)
{
  memset(support, 0, sizeof(char) * info->nVars);
}


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

  Synopsis    [Prints a support array.]

  Description [Prints a support array.]

  SideEffects []

******************************************************************************/
void
ImgSupportPrint(ImgTfmInfo_t *info, char *support)
{
  int	i;

  for (i = 0; i < info->nVars; i++) {
   if (support[i])
     printf("*");
   else
     printf(".");
  }
  printf("\n");
}


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

  Synopsis    [Returns the number of support of a support array.]

  Description [Returns the number of support of a support array.]

  SideEffects []

******************************************************************************/
int
ImgSupportCount(ImgTfmInfo_t *info, char *support)
{
  int	i, nSupports;

  nSupports = 0;
  for (i = 0; i < info->nVars; i++) {
   if (support[i])
     nSupports++;
  }
  return(nSupports);
}


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

  Synopsis    [Constrains a relation array with respect to a constraint.]

  Description [Constrains a relation array with respect to a constraint.
  Returns new relation array.]

  SideEffects []

******************************************************************************/
array_t *
ImgGetConstrainedRelationArray(ImgTfmInfo_t *info, array_t *relationArray,
				mdd_t *constraint)
{
  array_t		*constrainedRelationArray;
  int			dynStatus;
  bdd_reorder_type_t	dynMethod;

  dynStatus = bdd_reordering_status(info->manager, &dynMethod);
  if (dynStatus != 0)
    bdd_dynamic_reordering_disable(info->manager);

  constrainedRelationArray = ImgGetCofactoredRelationArray(relationArray,
							   constraint);

  if (dynStatus != 0) {
    bdd_dynamic_reordering(info->manager, dynMethod,
			   BDD_REORDER_VERBOSITY_DEFAULT);
  }

  return(constrainedRelationArray);
}


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

  Synopsis    [Cofactors a relation array with respect to a function.]

  Description [Cofactors a relation array with respect to a function.
  Returns new relation array.]

  SideEffects []

******************************************************************************/
array_t *
ImgGetCofactoredRelationArray(array_t *relationArray, mdd_t *func)
{
  int		i;
  array_t	*cofactoredRelationArray;
  mdd_t		*relation, *cofactoredRelation;

  if (bdd_is_tautology(func, 1))
    return(mdd_array_duplicate(relationArray));

  cofactoredRelationArray = array_alloc(mdd_t *, 0);

  for (i = 0; i < array_n(relationArray); i++) {
    relation = array_fetch(mdd_t *, relationArray, i);
    cofactoredRelation = bdd_cofactor(relation, func);
    if (bdd_is_tautology(cofactoredRelation, 1))
      mdd_free(cofactoredRelation);
    else
      array_insert_last(mdd_t *, cofactoredRelationArray, cofactoredRelation);
  }

  return(cofactoredRelationArray);
}


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

  Synopsis    [Cofactors a relation array with respect to a function.]

  Description [Cofactors a relation array with respect to a function.]

  SideEffects []

******************************************************************************/
void
ImgCofactorRelationArray(array_t *relationArray, mdd_t *func)
{
  int		i;
  mdd_t		*relation, *cofactoredRelation;

  if (bdd_is_tautology(func, 1))
    return;

  for (i = 0; i < array_n(relationArray); i++) {
    relation = array_fetch(mdd_t *, relationArray, i);
    cofactoredRelation = bdd_cofactor(relation, func);
    if (mdd_equal(cofactoredRelation, relation))
      mdd_free(cofactoredRelation);
    else {
      mdd_free(relation);
      array_insert(mdd_t *, relationArray, i, cofactoredRelation);
    }
  }
}


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

  Synopsis    [Smoothes a relation array with respect to a cube.]

  Description [Smoothes a relation array with respect to a cube.]

  SideEffects []

******************************************************************************/
array_t *
ImgGetAbstractedRelationArray(mdd_manager *manager, array_t *relationArray,
			      mdd_t *cube)
{
  int		i;
  array_t	*abstractedRelationArray;
  mdd_t		*relation, *abstractedRelation;
  array_t	*varsArray;

  if (bdd_is_tautology(cube, 1))
    return(mdd_array_duplicate(relationArray));

  abstractedRelationArray = array_alloc(mdd_t *, 0);

  if (bdd_get_package_name() != CUDD)
    varsArray = mdd_get_bdd_support_vars(manager, cube);
  else /* to remove uninitialized variable warning*/
    varsArray = NIL(array_t);
  for (i = 0; i < array_n(relationArray); i++) {
    relation = array_fetch(mdd_t *, relationArray, i);
    if (bdd_get_package_name() == CUDD)
      abstractedRelation = bdd_smooth_with_cube(relation, cube);
    else
      abstractedRelation = bdd_smooth(relation, varsArray);
    if (bdd_is_tautology(abstractedRelation, 1))
      mdd_free(abstractedRelation);
    else
      array_insert_last(mdd_t *, abstractedRelationArray, abstractedRelation);
  }
  if (bdd_get_package_name() != CUDD)
    mdd_array_free(varsArray);

  return(abstractedRelationArray);
}


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

  Synopsis    [Smoothes a relation array with respect to a cube.]

  Description [Smoothes a relation array with respect to a cube.]

  SideEffects []

******************************************************************************/
void
ImgAbstractRelationArray(mdd_manager *manager, array_t *relationArray,
			 mdd_t *cube)
{
  int		i;
  mdd_t		*relation, *abstractedRelation;
  array_t	*varsArray;

  if (bdd_is_tautology(cube, 1))
    return;

  if (bdd_get_package_name() != CUDD)
    varsArray = mdd_get_bdd_support_vars(manager, cube);
  else /* to remove uninitialized variable warning*/
    varsArray = NIL(array_t);
  for (i = 0; i < array_n(relationArray); i++) {
    relation = array_fetch(mdd_t *, relationArray, i);
    if (bdd_get_package_name() == CUDD)
      abstractedRelation = bdd_smooth_with_cube(relation, cube);
    else
      abstractedRelation = bdd_smooth(relation, varsArray);
    if (mdd_equal(abstractedRelation, relation))
      mdd_free(abstractedRelation);
    else {
      mdd_free(relation);
      array_insert(mdd_t *, relationArray, i, abstractedRelation);
    }
  }
  if (bdd_get_package_name() != CUDD)
    mdd_array_free(varsArray);
}


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

  Synopsis    [Cofactors and smooths a relation array.]

  Description [Cofactors and smooths a relation array. Returns new
  relation array.]

  SideEffects []

******************************************************************************/
array_t *
ImgGetCofactoredAbstractedRelationArray(mdd_manager *manager,
					array_t *relationArray,
					mdd_t *cofactorCube,
					mdd_t *abstractCube)
{
  int		i;
  array_t	*newRelationArray = array_alloc(mdd_t *, 0);
  mdd_t		*relation, *newRelation, *tmpRelation;
  array_t	*varsArray;

  if (bdd_get_package_name() != CUDD)
    varsArray = mdd_get_bdd_support_vars(manager, abstractCube);
  else /* to remove uninitialized variable warning*/
    varsArray = NIL(array_t);
  for (i = 0; i < array_n(relationArray); i++) {
    relation = array_fetch(mdd_t *, relationArray, i);
    tmpRelation = bdd_cofactor(relation, cofactorCube);
    if (bdd_get_package_name() == CUDD)
      newRelation = bdd_smooth_with_cube(tmpRelation, abstractCube);
    else
      newRelation = bdd_smooth(tmpRelation, varsArray);
    mdd_free(tmpRelation);
    if (bdd_is_tautology(newRelation, 1))
      mdd_free(newRelation);
    else
      array_insert_last(mdd_t *, newRelationArray, newRelation);
  }
  if (bdd_get_package_name() != CUDD)
    mdd_array_free(varsArray);

  return(newRelationArray);
}


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

  Synopsis    [Smothes and cofactors a relation array.]

  Description [Smothes and cofactors a relation array. Returns new
  relation array.]

  SideEffects []

******************************************************************************/
array_t *
ImgGetAbstractedCofactoredRelationArray(mdd_manager *manager,
					array_t *relationArray,
					mdd_t *cofactorCube,
					mdd_t *abstractCube)
{
  int		i;
  array_t	*newRelationArray = array_alloc(mdd_t *, 0);
  mdd_t		*relation, *newRelation, *tmpRelation;
  array_t	*varsArray;

  if (bdd_get_package_name() != CUDD)
    varsArray = mdd_get_bdd_support_vars(manager, abstractCube);
  else /* to remove uninitialized variable warning*/
    varsArray = NIL(array_t);
  for (i = 0; i < array_n(relationArray); i++) {
    relation = array_fetch(mdd_t *, relationArray, i);
    if (bdd_get_package_name() == CUDD)
      tmpRelation = bdd_smooth_with_cube(relation, abstractCube);
    else
      tmpRelation = bdd_smooth(relation, varsArray);
    newRelation = bdd_cofactor(tmpRelation, cofactorCube);
    mdd_free(tmpRelation);
    if (bdd_is_tautology(newRelation, 1))
      mdd_free(newRelation);
    else
      array_insert_last(mdd_t *, newRelationArray, newRelation);
  }
  if (bdd_get_package_name() != CUDD)
    mdd_array_free(varsArray);

  return(newRelationArray);
}


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

  Synopsis    [Constrains a function vector with respect to a constraint.]

  Description [Constrains a function vector with respect to a constraint.
  Returns new function vector.]

  SideEffects []

******************************************************************************/
array_t *
ImgGetConstrainedVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint)
{
  array_t		*constrainedVector;
  int			dynStatus;
  bdd_reorder_type_t	dynMethod;

  dynStatus = bdd_reordering_status(info->manager, &dynMethod);
  if (dynStatus != 0)
    bdd_dynamic_reordering_disable(info->manager);

  constrainedVector = ImgGetCofactoredVector(info, vector, constraint);

  if (dynStatus != 0) {
    bdd_dynamic_reordering(info->manager, dynMethod,
			   BDD_REORDER_VERBOSITY_DEFAULT);
  }

  return(constrainedVector);
}


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

  Synopsis    [Cofactors a function vector with respect to a function.]

  Description [Cofactors a function vector with respect to a function.
  Returns new function vector.]

  SideEffects []

******************************************************************************/
array_t *
ImgGetCofactoredVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *func)
{
  int			i;
  array_t		*cofactoredVector = array_alloc(ImgComponent_t *, 0);
  ImgComponent_t	*comp, *cofactoredComp;
  mdd_t			*cofactoredFunc;

  if (bdd_is_tautology(func, 1))
    return(ImgVectorCopy(info, vector));

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    cofactoredFunc = bdd_cofactor(comp->func, func);
    cofactoredComp = ImgComponentAlloc(info);
    cofactoredComp->var = mdd_dup(comp->var);
    cofactoredComp->func = cofactoredFunc;
    cofactoredComp->intermediate = comp->intermediate;
    if (mdd_equal(cofactoredFunc, comp->func))
      ImgSupportCopy(info, cofactoredComp->support, comp->support);
    else
      ImgComponentGetSupport(cofactoredComp);
    array_insert_last(ImgComponent_t *, cofactoredVector, cofactoredComp);
  }

  return(cofactoredVector);
}


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

  Synopsis    [Cofactors a function vector with respect to a function.]

  Description [Cofactors a function vector with respect to a function.]

  SideEffects []

******************************************************************************/
void
ImgCofactorVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *func)
{
  int			i;
  ImgComponent_t	*comp;
  mdd_t			*cofactoredFunc;

  if (bdd_is_tautology(func, 1))
    return;

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    cofactoredFunc = bdd_cofactor(comp->func, func);
    if (mdd_equal(cofactoredFunc, comp->func))
      mdd_free(cofactoredFunc);
    else {
      mdd_free(comp->func);
      comp->func = cofactoredFunc;
      ImgSupportClear(info, comp->support);
      ImgComponentGetSupport(comp);
    }
  }
}


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

  Synopsis    [Eliminates dependent variables from transition function.]

  Description [Eliminates dependent variables from a transition
  function.  Returns a simplified copy of the given states if successful;
  NULL otherwise.]

  SideEffects [vector is also modified.]

  SeeAlso     []

******************************************************************************/
mdd_t *
ImgTfmEliminateDependVars(ImgTfmInfo_t *info, array_t *vector,
			  array_t *relationArray, mdd_t *states,
			  array_t **newVector,
			  mdd_t **dependRelations)
{
  int			i, j;
  int			howMany = 0;
			/* number of latches that can be eliminated */
  mdd_t			*var, *newStates, *abs, *positive, *phi;
  mdd_t			*tmp, *relation;
  int			nVars;
  int			nSupports; /* vars in the support of the state set */
  int			*candidates; /* vars to be considered for elimination */
  double		minStates;
  ImgComponent_t	*comp, *newComp;

  if (dependRelations) {
    *dependRelations = mdd_one(info->manager);
    *newVector = array_alloc(ImgComponent_t *, 0);
  }
  newStates = mdd_dup(states);
  nVars = info->nVars;

  candidates = ALLOC(int, nVars);
  if (candidates == NULL)
    return(NULL);

  comp = ImgComponentAlloc(info);
  comp->func = newStates;
  ImgComponentGetSupport(comp);
  nSupports = 0;
  for (i = 0 ; i < nVars; i++) {
    if (comp->support[i]) {
      candidates[nSupports] = i;
      nSupports++;
    }
  }
  comp->func = NIL(mdd_t);
  ImgComponentFree(comp);

  /* The signatures of the variables in a function are the number
  ** of minterms of the positive cofactors with respect to the
  ** variables themselves. */
  signatures = bdd_cof_minterm(newStates);
  if (signatures == NULL) {
    FREE(candidates);
    return(NULL);
  }
  /* We now extract a positive quantity which is higher for those
  ** variables that are closer to being essential. */
  minStates = signatures[nSupports];
  for (i = 0; i < nSupports; i++) {
    double z = signatures[i] / minStates - 1.0;
    signatures[i] = (z < 0.0) ? -z : z;    /* make positive */
  }
  qsort((void *)candidates, nSupports, sizeof(int),
      (int (*)(const void *, const void *))SignatureCompare);
  FREE(signatures);

  /* Now process the candidates in the given order. */
  for (i = 0; i < nSupports; i++) {
    var = bdd_var_with_index(info->manager, candidates[i]);
    if (bdd_var_is_dependent(newStates, var)) {
      abs = bdd_smooth_with_cube(newStates, var);
      if (abs == NULL)
	return(NULL);
      positive = bdd_cofactor(newStates, var);
      if (positive == NULL)
	return(NULL);
      phi = Img_MinimizeImage(positive, abs, Img_DefaultMinimizeMethod_c,
			      TRUE); 
      if (phi == NULL)
	return(NULL);
      mdd_free(positive);
      if (bdd_size(phi) < IMG_MAX_DEP_SIZE) {
	howMany++;
	if (dependRelations) {
	  for (j = 0; j < array_n(vector); j++) {
	    comp = array_fetch(ImgComponent_t *, vector, j);
	    if (mdd_equal(comp->var, var))
	      continue;
	    newComp = ImgComponentCopy(info, comp);
	    array_insert_last(ImgComponent_t *, *newVector, newComp);
	  }
	} else {
	  for (j = 0; j < array_n(vector); j++) {
	    comp = array_fetch(ImgComponent_t *, vector, j);
	    tmp = bdd_compose(comp->func, var, phi);
	    if (tmp == NULL)
	      return(NULL);
	    mdd_free(comp->func);
	    comp->func = tmp;
	    ImgSupportClear(info, comp->support);
	    ImgComponentGetSupport(comp);
	  }
	}
	if (relationArray) {
	  for (j = 0; j < array_n(relationArray); j++) {
	    relation = array_fetch(mdd_t *, relationArray, j);
	    if (dependRelations)
	      tmp = bdd_smooth_with_cube(relation, var);
	    else
	      tmp = bdd_compose(relation, var, phi);
	    mdd_free(relation);
	    array_insert(mdd_t *, relationArray, j, tmp);
	  }
	}
	mdd_free(newStates);
	newStates = abs;
	if (dependRelations) {
	  relation = mdd_xnor(var, phi);
	  tmp = mdd_and(*dependRelations, relation, 1, 1);
	  mdd_free(*dependRelations);
	  mdd_free(relation);
	  *dependRelations = tmp;
	}
      } else {
	mdd_free(abs);
      }
      mdd_free(phi);
    }
  }
  FREE(candidates);

  if (howMany) {
    if (info->imageVerbosity > 0)
      (void)fprintf(vis_stdout, "Eliminated %d vars.\n", howMany);
    info->averageFoundDependVars = (info->averageFoundDependVars *
			(float)info->nFoundDependVars + (float)howMany) /
			(float)(info->nFoundDependVars + 1);
    info->nFoundDependVars++;
  }

  info->nPrevEliminatedFwd = howMany;
  return(newStates);
} /* end of TfmEliminateDependVars */


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

  Synopsis    [Checks whether there is a constant function of intermediate
  variables.]

  Description [Checks whether there is a constant function of intermediate
  variables.]

  SideEffects []

******************************************************************************/
int
ImgExistConstIntermediateVar(array_t *vector)
{
  int			i;
  ImgComponent_t	*comp;

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (comp->intermediate) {
      if (mdd_is_tautology(comp->func, 1) || mdd_is_tautology(comp->func, 0))
	return(1);
    }
  }
  return(0);
}


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

  Synopsis    [Returns a function composed all intermediate variables.]

  Description [Returns a function composed all intermediate variables.]

  SideEffects []

******************************************************************************/
mdd_t *
ImgGetComposedFunction(array_t *vector)
{
  ImgComponent_t	*comp;
  mdd_t			*func, *newFunc;
  int			i;
  array_t		*varArray, *funcArray;

  assert(ImgVectorFunctionSize(vector) == 1);

  /* no intermediate variables */
  if (array_n(vector) == 1) {
    comp = array_fetch(ImgComponent_t *, vector, 0);
    newFunc = mdd_dup(comp->func);
    return(newFunc);
  }

  func = NIL(mdd_t);
  varArray = array_alloc(mdd_t *, 0);
  funcArray = array_alloc(mdd_t *, 0);

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (comp->intermediate) {
      array_insert_last(mdd_t *, varArray, comp->var);
      array_insert_last(mdd_t *, funcArray, comp->func);
      continue;
    }
    func = comp->func;
  }

  newFunc = bdd_vector_compose(func, varArray, funcArray);
  array_free(varArray);
  array_free(funcArray);
  return(newFunc);
}


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

  Synopsis    [Returns the first latch component.]

  Description [Returns the first latch component.]

  SideEffects []

******************************************************************************/
ImgComponent_t *
ImgGetLatchComponent(array_t *vector)
{
  ImgComponent_t	*comp;
  int			i;

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (!comp->intermediate)
      return(comp);
  }
  return(NIL(ImgComponent_t));
}


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

  Synopsis    [Compose the constant intermediate variable functions.]

  Description [Compose the constant intermediate variable functions.]

  SideEffects []

******************************************************************************/
array_t *
ImgComposeConstIntermediateVars(ImgTfmInfo_t *info, array_t *vector,
				mdd_t *constIntermediate,
				mdd_t **cofactorCube, mdd_t **abstractCube,
				mdd_t **and_, mdd_t **from)
{
  int			i, n, pos;
  array_t		*tmpVector, *cofactoredVector;
  mdd_t			*cofactor, *abstract;
  mdd_t			*curConstIntermediate, *newConstIntermediate;
  mdd_t			*tmp, *new_, *func, *varNot, *nsVar;
  ImgComponent_t	*comp, *comp1;
  st_table		*equivTable;
  int			*ptr, *regularPtr;

  if (cofactorCube)
    cofactor = mdd_one(info->manager);
  else
    cofactor = NIL(mdd_t);
  if (abstractCube)
    abstract = mdd_one(info->manager);
  else
    abstract = NIL(mdd_t);

  cofactoredVector = vector;
  tmpVector = cofactoredVector;
  curConstIntermediate = constIntermediate;

  while (!bdd_is_tautology(curConstIntermediate, 1)) {
    newConstIntermediate = mdd_one(info->manager);
    n = 0;
    equivTable = st_init_table(st_ptrcmp, st_ptrhash);
    cofactoredVector = array_alloc(ImgComponent_t *, 0);
    for (i = 0; i < array_n(tmpVector); i++) {
      comp = array_fetch(ImgComponent_t *, tmpVector, i);
      func = bdd_cofactor(comp->func, curConstIntermediate);

      if (comp->intermediate) {
	if (mdd_is_tautology(func, 1)) {
	  tmp = newConstIntermediate;
	  newConstIntermediate = mdd_and(tmp, comp->var, 1, 1);
	  mdd_free(tmp);
	  mdd_free(func);
	  continue;
	} else if (mdd_is_tautology(func, 0)) {
	  tmp = newConstIntermediate;
	  newConstIntermediate = mdd_and(tmp, comp->var, 1, 0);
	  mdd_free(tmp);
	  mdd_free(func);
	  continue;
	}

	comp1 = ImgComponentAlloc(info);
	comp1->var = mdd_dup(comp->var);
	comp1->func = func;
	comp1->intermediate = 1;
	if (mdd_equal(func, comp->func))
	  ImgSupportCopy(info, comp1->support, comp->support);
	else
	  ImgComponentGetSupport(comp1);
	array_insert_last(ImgComponent_t *, cofactoredVector, comp1);
	n++;
	continue;
      }

      if (mdd_is_tautology(func, 1)) {
	if (cofactor) {
	  nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	  tmp = cofactor;
	  cofactor = mdd_and(tmp, nsVar, 1, 1);
	  mdd_free(tmp);
	  mdd_free(nsVar);
	}
	if (and_) {
	  tmp = *and_;
	  *and_ = mdd_and(tmp, comp->var, 1, 1);
	  mdd_free(tmp);
	}
	if (from) {
	  tmp = *from;
	  *from = bdd_cofactor(tmp, comp->var);
	  mdd_free(tmp);
	}
	mdd_free(func);
      } else if (mdd_is_tautology(func, 0)) {
	if (cofactor) {
	  nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	  tmp = cofactor;
	  cofactor = mdd_and(tmp, nsVar, 1, 0);
	  mdd_free(tmp);
	  mdd_free(nsVar);
	}
	if (and_) {
	  tmp = *and_;
	  *and_ = mdd_and(tmp, comp->var, 1, 0);
	  mdd_free(tmp);
	}
	if (from) {
	  tmp = *from;
	  varNot = bdd_not(comp->var);
	  *from = bdd_cofactor(tmp, varNot);
	  mdd_free(tmp);
	  mdd_free(varNot);
	}
	mdd_free(func);
      } else {
	ptr = (int *)bdd_pointer(func);
	regularPtr = (int *)((unsigned long)ptr & ~01);
	if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
	  comp1 = array_fetch(ImgComponent_t *, cofactoredVector, pos);
	  if (and_) {
	    if (mdd_equal(func, comp1->func))
	      tmp = mdd_xnor(comp->var, comp1->var);
	    else
	      tmp = mdd_xor(comp->var, comp1->var);
	    new_ = mdd_and(tmp, *and_, 1, 1);
	    mdd_free(tmp);
	    mdd_free(*and_);
	    mdd_free(func);
	    *and_ = new_;
	  }
	  if (abstract) {
	    nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	    tmp = abstract;
	    abstract = mdd_and(tmp, nsVar, 1, 1);
	    mdd_free(tmp);
	    mdd_free(nsVar);
	  }
	  if (from) {
	    tmp = *from;
	    *from = bdd_compose(tmp, comp->var, comp1->var);
	    mdd_free(tmp);
	  }
	} else {
	  comp1 = ImgComponentAlloc(info);
	  comp1->var = mdd_dup(comp->var);
	  comp1->func = func;
	  if (mdd_equal(func, comp->func))
	    ImgSupportCopy(info, comp1->support, comp->support);
	  else
	    ImgComponentGetSupport(comp1);
	  array_insert_last(ImgComponent_t *, cofactoredVector, comp1);
	  st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
	  n++;
	}
      }
    }

    if (curConstIntermediate != constIntermediate)
      mdd_free(curConstIntermediate);
    curConstIntermediate = newConstIntermediate;

    if (cofactor) {
      tmp = cofactor;
      cofactor = mdd_and(tmp, curConstIntermediate, 1, 1);
      mdd_free(tmp);
    }

    st_free_table(equivTable);
    ImgVectorFree(tmpVector);
    tmpVector = cofactoredVector;
  }

  if (curConstIntermediate != constIntermediate)
    mdd_free(curConstIntermediate);

  if (cofactorCube)
    *cofactorCube = cofactor;
  if (abstractCube)
    *abstractCube = abstract;

  return(cofactoredVector);
}


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

  Synopsis    [Returns the number of BDD supports in a function.]

  Description [Returns the number of BDD supports in a function.]

  SideEffects []

******************************************************************************/
int
ImgCountBddSupports(mdd_t *func)
{
  int		index, nSupports = 0;
  var_set_t	*supportVarSet;

  supportVarSet = bdd_get_support(func);
  for (index = 0; index < supportVarSet->n_elts; index++) {
    if (var_set_get_elt(supportVarSet, index) == 1)
      nSupports++;
  }
  var_set_free(supportVarSet);
  return(nSupports);
}


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

  Synopsis    [Quick checking whether the results of constrain between two
  functions are constant.]

  Description [Quick checking whether the results of constrain between two
  functions are constant. Assumes that 1) f1 != f2 and f1 != f2', and
  2) neither f1 nor f2 is constant.]

  SideEffects []

******************************************************************************/
void
ImgCheckConstConstrain(mdd_t *f1, mdd_t *f2, int *f21p, int *f21n)
{
  if (mdd_lequal(f1, f2, 1, 1)) { /* f2 > f1 */
    *f21p = 1;
    *f21n = 2;
  } else if (mdd_lequal(f2, f1, 1, 0)) { /* f2&f1=0 -> f2 < f1' */
    *f21p = 0;
    *f21n = 2;
  } else if (mdd_lequal(f1, f2, 0, 1)) { /* f2 > f1' */
    *f21p = 2;
    *f21n = 1;
  } else if (mdd_lequal(f2, f1, 1, 1)) { /* f2&f1'=0 -> f2 < f1 */
    *f21p = 2;
    *f21n = 0;
  } else {
    *f21p = 2;
    *f21n = 2;
  }
}


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

  Synopsis    [Checks whether the result of constrain is constant.]

  Description [Checks whether the result of constrain is constant.]

  SideEffects []

******************************************************************************/
int
ImgConstConstrain(mdd_t *func, mdd_t *constraint)
{
  if (mdd_lequal(constraint, func, 1, 1)) /* func | constraint = 1 */
    return(1);
  if (mdd_lequal(func, constraint, 1, 0)) /* func | constraint = 0 */
    return(0);
  return(2); /* non-constant */
}


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

  Synopsis    [Prints vector dependencies with support.]

  Description [Prints vector dependencies with support.]

  SideEffects []

******************************************************************************/
void
ImgPrintVectorDependency(ImgTfmInfo_t *info, array_t *vector, int verbosity)
{
  int			i, j, index, nFuncs, nSupports;
  int			nLambdaLatches, nConstLatches, nIntermediateVars;
  int			count, countStates, total;
  int			start, end;
  char			*support, line[80];
  ImgComponent_t	*comp;

  if (verbosity == 0 || (!vector))
    return;

  support = ALLOC(char, sizeof(char) * info->nVars);
  memset(support, 0, sizeof(char) * info->nVars);

  count = countStates = 0;
  nFuncs = array_n(vector);
  for (i = 0; i < nFuncs; i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    for (j = 0; j < info->nVars; j++) {
      if (comp->support[j]) {
	support[j] = 1;
	count++;
	if (!st_lookup(info->quantifyVarsTable, (char *)(long)j, NIL(char *)))
	  countStates++;
      }
    }
  }
  nSupports = 0;
  for (i = 0; i < info->nVars; i++) {
    if (support[i])
      nSupports++;
  }
  nLambdaLatches = 0;
  nConstLatches = 0;
  nIntermediateVars = 0;
  for (i = 0; i < nFuncs; i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    index = bdd_top_var_id(comp->var);
    if (!support[index])
      nLambdaLatches++;
    if (ImgSupportCount(info, comp->support) == 0)
      nConstLatches++;
    if (comp->intermediate)
      nIntermediateVars++;
  }
  fprintf(vis_stdout, "** tfm info: #vars = %d(%d)\n",
	  info->nVars - nFuncs + nIntermediateVars, info->nVars);
  fprintf(vis_stdout, "** tfm info: #input vars = %d\n",
	  info->nVars - (nFuncs - nIntermediateVars) * 2 - nIntermediateVars);
  fprintf(vis_stdout, "** tfm info: #funcs = %d\n", nFuncs);
  fprintf(vis_stdout, "** tfm info: #lambda funcs = %d\n", nLambdaLatches);
  fprintf(vis_stdout, "** tfm info: #constant funcs = %d\n", nConstLatches);
  fprintf(vis_stdout, "** tfm info: #intermediate funcs = %d\n",
	  nIntermediateVars);
  fprintf(vis_stdout,
	  "Shared size of transition function vector is %10ld BDD nodes\n",
	  ImgVectorBddSize(vector));
  total = nFuncs * nFuncs;
  fprintf(vis_stdout,
"** tfm info: support distribution (state variables) = %.2f%%(%d out of %d)\n",
	  (float)countStates / (float)total * 100.0, countStates, total);
  total = nFuncs * nSupports;
  fprintf(vis_stdout,
"** tfm info: support distribution (all variables) = %.2f%% (%d out of %d)\n",
	  (float)count / (float)total * 100.0, count, total);

  if (verbosity < 3) {
    FREE(support);
    return;
  }

  fprintf(vis_stdout, "*** function list ***\n");
  for (i = 0; i < nFuncs; i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    index = bdd_top_var_id(comp->var);
    fprintf(vis_stdout, "[%d] index = %d\n", i, index);
  }

  start = 0;
  end = 74;
  if (end >= nFuncs)
    end = nFuncs - 1;
  while (1) {
    fprintf(vis_stdout, "========================================");
    fprintf(vis_stdout, "========================================\n");
    fprintf(vis_stdout, "     1234567890123456789012345678901234567890");
    fprintf(vis_stdout, "12345678901234567890123456789012345\n");
    fprintf(vis_stdout, "----------------------------------------");
    fprintf(vis_stdout, "----------------------------------------\n");
    for (i = 0; i < info->nVars; i++) {
      if (!support[i])
	continue;
      if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
	continue;
      for (j = start; j <= end; j++) {
	comp = array_fetch(ImgComponent_t *, vector, j);
	if (comp->support[i])
	  line[j - start] = '1';
	else
	  line[j - start] = '.';
      }
      line[j - start] = '\0';
      fprintf(vis_stdout, "%4d %s\n", i, line);
    }
    if (end >= nFuncs - 1)
      break;
    start += 75;
    end += 75;
    if (end >= nFuncs)
      end = nFuncs - 1;
  }
  FREE(support);
}


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

  Synopsis    [Returns the percent of non-zero elements in dependency matrix.]

  Description [Returns the percent of non-zero elements in dependency matrix.]

  SideEffects []

******************************************************************************/
float
ImgPercentVectorDependency(ImgTfmInfo_t *info, array_t *vector, int length,
			   int *nLongs)
{
  int			i, j, index, nFuncs, nSupports, nLambdaLatches;
  int			count, total;
  char			*support;
  ImgComponent_t	*comp;
  float			percent;
  int			*occurs;

  support = ALLOC(char, sizeof(char) * info->nVars);
  memset(support, 0, sizeof(char) * info->nVars);
  occurs = ALLOC(int, sizeof(int) * info->nVars);
  memset(occurs, 0, sizeof(int) * info->nVars);

  count = 0;
  nFuncs = array_n(vector);
  for (i = 0; i < nFuncs; i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    for (j = 0; j < info->nVars; j++) {
      if (comp->support[j]) {
	support[j] = 1;
	count++;
	occurs[i]++;
      }
    }
  }
  nSupports = 0;
  for (i = 0; i < info->nVars; i++) {
    if (support[i])
      nSupports++;
  }
  nLambdaLatches = 0;
  for (i = 0; i < nFuncs; i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    index = bdd_top_var_id(comp->var);
    if (!support[index])
      nLambdaLatches++;
  }
  FREE(support);

  *nLongs = 0;
  for (i = 0; i < info->nVars; i++) {
    if (occurs[i] >= length)
      (*nLongs)++;
  }

  total = (nFuncs - nLambdaLatches) * nSupports;
  percent = (float)count / (float)total * 100.0;
  return(percent);
}


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

  Synopsis    [Writes a gnuplot file with support matrix.]

  Description [Writes a gnuplot file with support matrix.]

  SideEffects []

******************************************************************************/
void
ImgWriteSupportMatrix(ImgTfmInfo_t *info, array_t *vector,
		      array_t *relationArray, char *string)
{
  int			i, j, id, nFuncs, nRelations, nRows, nSupports;
  int			*row, col, varType;
  char			*support, **relationSupport;
  ImgComponent_t	*comp;
  FILE			*fout;
  mdd_t			*relation, *var;
  char			*filename;

  support = ALLOC(char, sizeof(char) * info->nVars);
  memset(support, 0, sizeof(char) * info->nVars);
  nRows = 0;
  if (vector)
    nRows += array_n(vector);
  if (relationArray)
    nRows += array_n(relationArray);
  row = ALLOC(int, sizeof(int) * nRows);
  if (string)
    filename = string;
  else
    filename = "support.mat";
  fout = fopen(filename, "w");

  nRows = 0;
  if (vector) {
    nFuncs = array_n(vector);
    for (i = 0; i < nFuncs; i++) {
      comp = array_fetch(ImgComponent_t *, vector, i);
      if (ImgSupportCount(info, comp->support) == 0) {
	row[i] = -1;
	continue;
      }
      row[i] = nRows;
      nRows++;
      if (info->option->writeSupportMatrixWithYvars) {
	var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	id = (int)bdd_top_var_id(var);
	support[id] = 1;
	mdd_free(var);
      }
      for (j = 0; j < info->nVars; j++) {
	if (comp->support[j])
	  support[j] = 1;
      }
    }
  } else
    nFuncs = 0;

  relationSupport = 0;
  if (relationArray && array_n(relationArray) > 0) {
    comp = ImgComponentAlloc(info);
    nRelations = 0;
    relationSupport = ALLOC(char *, sizeof(char *) * array_n(relationArray));
    for (i = 0; i < array_n(relationArray); i++) {
      relation = array_fetch(mdd_t *, relationArray, i);
      comp->func = relation;
      ImgSupportClear(info, comp->support);
      ImgComponentGetSupport(comp);
      if (ImgSupportCount(info, comp->support) <= 1) {
	row[i + nFuncs] = -1;
	relationSupport[i] = NIL(char);
	continue;
      }
      row[i + nFuncs] = nRows;
      nRows++;
      for (j = 0; j < info->nVars; j++) {
	if (comp->support[j])
	  support[j] = 1;
      }
      relationSupport[i] = ALLOC(char, sizeof(char) * info->nVars);
      memcpy(relationSupport[i], comp->support, sizeof(char) * info->nVars);
      nRelations++;
    }
    comp->func = NIL(mdd_t);
    ImgComponentFree(comp);
  } else
    nRelations = 0;

  nSupports = 0;
  for (i = 0; i < info->nVars; i++) {
    if (support[i]) {
      if (!info->option->writeSupportMatrixWithYvars &&
	  st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
	continue;
      }
      nSupports++;
    }
  }

  col = 0;
  for (i = 0; i < info->nVars; i++) {
    if (!support[i])
      continue;
    if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
      if (info->option->writeSupportMatrixWithYvars)
	varType = 3;
      else
	continue;
    } else if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
      varType = 2;
    else
      varType = 1;
    for (j = 0; j < nFuncs; j++) {
      comp = array_fetch(ImgComponent_t *, vector, j);
      if (comp->support[i]) {
	if (info->option->writeSupportMatrixReverseRow) {
	  if (info->option->writeSupportMatrixReverseCol) {
	    fprintf(fout, "%d %d %d\n", nSupports - col, nRows - row[j],
		    varType);
	  } else
	    fprintf(fout, "%d %d %d\n", col + 1, nRows - row[j], varType);
	} else {
	  if (info->option->writeSupportMatrixReverseCol)
	    fprintf(fout, "%d %d %d\n", nSupports - col, row[j] + 1, varType);
	  else
	    fprintf(fout, "%d %d %d\n", col + 1, row[j] + 1, varType);
	}
      } else if (varType == 3) {
	var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	id = (int)bdd_top_var_id(var);
	mdd_free(var);
	if (id == i) {
	  if (info->option->writeSupportMatrixReverseRow) {
	    if (info->option->writeSupportMatrixReverseCol)
	      fprintf(fout, "%d %d 3\n", nSupports - col, nRows - row[j]);
	    else
	      fprintf(fout, "%d %d 3\n", col + 1, nRows - row[j]);
	  } else {
	    if (info->option->writeSupportMatrixReverseCol)
	      fprintf(fout, "%d %d 3\n", nSupports - col, row[j] + 1);
	    else
	      fprintf(fout, "%d %d 3\n", col + 1, row[j] + 1);
	  }
	}
      }
    }
    if (relationArray) {
      for (j = 0; j < array_n(relationArray); j++) {
	if (relationSupport[j] && relationSupport[j][i]) {
	  if (info->option->writeSupportMatrixReverseRow) {
	    if (info->option->writeSupportMatrixReverseCol) {
	      fprintf(fout, "%d %d %d\n", nSupports - col,
		      nRows - row[j + nFuncs], varType);
	    } else {
	      fprintf(fout, "%d %d %d\n", col + 1, nRows - row[j + nFuncs],
		      varType);
	    }
	  } else {
	    if (info->option->writeSupportMatrixReverseCol) {
	      fprintf(fout, "%d %d %d\n", nSupports - col, row[j + nFuncs] + 1,
		      varType);
	    } else {
	      fprintf(fout, "%d %d %d\n", col + 1, row[j + nFuncs] + 1,
		      varType);
	    }
	  }
	}
      }
    }
    col++;
  }
  fclose(fout);
  FREE(support);
  FREE(row);
  if (nRelations) {
    for (i = 0; i < nRelations; i++)
      FREE(relationSupport[i]);
    FREE(relationSupport);
  }
}


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


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

  Synopsis    [Comparison function used by qsort.]

  Description [Comparison function used by qsort to order the
  variables according to their signatures.]

  SideEffects [None]

******************************************************************************/
static int
SignatureCompare(int *ptrX, int *ptrY)
{
  if (signatures[*ptrY] > signatures[*ptrX])
    return(1);
  if (signatures[*ptrY] < signatures[*ptrX])
    return(-1);
  return(0);
} /* end of SignatureCompare */


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

  Synopsis    [Compares two function BDD pointers of components.]

  Description [Compares two function BDD pointers of components.]

  SideEffects []

******************************************************************************/
static int
CompareBddPointer(const void *e1, const void *e2)
{
  ImgComponent_t	*c1, *c2;
  unsigned long		ptr1, ptr2;

  c1 = *((ImgComponent_t **)e1);
  c2 = *((ImgComponent_t **)e2);

  ptr1 = (unsigned long)bdd_pointer(c1->func);
  ptr2 = (unsigned long)bdd_pointer(c2->func);

  if (ptr1 > ptr2)
    return(1);
  else if (ptr1 < ptr2)
    return(-1);
  else
    return(0);
}