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

  FileName    [imgHybrid.c]

  PackageName [img]

  Synopsis    [Routines for hybrid image computation.]

  Description [The hybrid image computation method combines transition function
  and relation methods, in other words, combines splitting and conjunction
  methods.]

  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: imgHybrid.c,v 1.27 2008/11/27 02:19:53 fabio Exp $";

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

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

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

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

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

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

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

static float ComputeSupportLambda(ImgTfmInfo_t *info, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, mdd_t *from, array_t *vector, int newRelationFlag, int preFlag, float *improvedLambda);

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


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


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

  Synopsis    [Prints the options for hybrid image computation.]

  Description [Prints the options for hybrid image computation.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Img_PrintHybridOptions(void)
{
  ImgTfmOption_t	*options;
  char			dummy[80];

  options = ImgTfmGetOptions(Img_Hybrid_c);

  switch (options->hybridMode) {
  case 0 :
    sprintf(dummy, "with only transition function");
    break;
  case 1 :
    sprintf(dummy, "with both transition function and relation");
    break;
  case 2 :
    sprintf(dummy, "with only transition relation");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "HYB: hybrid_mode = %d (%s)\n",
	  options->hybridMode, dummy);

  switch (options->trSplitMethod) {
  case 0 :
    sprintf(dummy, "support");
    break;
  case 1 :
    sprintf(dummy, "estimate BDD size");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "HYB: hybrid_tr_split_method = %d (%s)\n",
	  options->trSplitMethod, dummy);

  if (options->buildPartialTR)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_build_partial_tr = %s\n", dummy);

  fprintf(vis_stdout, "HYB: hybrid_partial_num_vars = %d\n",
	  options->nPartialVars);

  switch (options->partialMethod) {
  case 0 :
    sprintf(dummy, "BDD size");
    break;
  case 1 :
    sprintf(dummy, "support");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "HYB: hybrid_partial_method = %d (%s)\n",
	  options->partialMethod, dummy);

  if (options->delayedSplit)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_delayed_split = %s\n", dummy);

  fprintf(vis_stdout, "HYB: hybrid_split_min_depth = %d\n",
	  options->splitMinDepth);
  fprintf(vis_stdout, "HYB: hybrid_split_max_depth = %d\n",
	  options->splitMaxDepth);
  fprintf(vis_stdout, "HYB: hybrid_pre_split_min_depth = %d\n",
	  options->preSplitMinDepth);
  fprintf(vis_stdout, "HYB: hybrid_pre_split_max_depth = %d\n",
	  options->preSplitMaxDepth);

  fprintf(vis_stdout, "HYB: hybrid_lambda_threshold = %.2f\n",
	  options->lambdaThreshold);
  fprintf(vis_stdout, "HYB: hybrid_pre_lambda_threshold = %.2f\n",
	  options->preLambdaThreshold);
  fprintf(vis_stdout, "HYB: hybrid_conjoin_vector_size = %d\n",
	  options->conjoinVectorSize);
  fprintf(vis_stdout, "HYB: hybrid_conjoin_relation_size = %d\n",
	  options->conjoinRelationSize);
  fprintf(vis_stdout, "HYB: hybrid_conjoin_relation_bdd_size = %d\n",
	  options->conjoinRelationBddSize);
  fprintf(vis_stdout, "HYB: hybrid_improve_lambda = %.2f\n",
	  options->improveLambda);
  fprintf(vis_stdout, "HYB: hybrid_improve_vector_size = %d\n",
	  options->improveVectorSize);
  fprintf(vis_stdout, "HYB: hybrid_improve_vector_bdd_size = %.2f\n",
	  options->improveVectorBddSize);

  switch (options->decideMode) {
  case 0 :
    sprintf(dummy, "use only lambda");
    break;
  case 1 :
    sprintf(dummy, "lambda + special check");
    break;
  case 2 :
    sprintf(dummy, "lambda + improvement");
    break;
  case 3 :
    sprintf(dummy, "use all");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "HYB: hybrid_decide_mode = %d (%s)\n",
	  options->decideMode, dummy);

  if (options->reorderWithFrom)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_reorder_with_from = %s\n", dummy);

  if (options->preReorderWithFrom)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_pre_reorder_with_from = %s\n", dummy);

  switch (options->lambdaMode) {
  case 0 :
    sprintf(dummy, "total lifetime with ps/pi variables");
    break;
  case 1 :
    sprintf(dummy, "active lifetime with ps/pi variables");
    break;
  case 2 :
    sprintf(dummy, "total lifetime with ps/ns/pi variables");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "HYB: hybrid_lambda_mode = %d (%s)\n",
	  options->lambdaMode, dummy);

  switch (options->preLambdaMode) {
  case 0 :
    sprintf(dummy, "total lifetime with ns/pi variables");
    break;
  case 1 :
    sprintf(dummy, "active lifetime with ps/pi variables");
    break;
  case 2 :
    sprintf(dummy, "total lifetime with ps/ns/pi variables");
    break;
  case 3 :
    sprintf(dummy, "total lifetime with ps/pi variables");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "HYB: hybrid_pre_lambda_mode = %d (%s)\n",
	  options->preLambdaMode, dummy);

  if (options->lambdaWithFrom)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_lambda_with_from = %s\n", dummy);

  if (options->lambdaWithTr)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_lambda_with_tr = %s\n", dummy);

  if (options->lambdaWithClustering)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_lambda_with_clustering = %s\n", dummy);

  if (options->synchronizeTr)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_synchronize_tr = %s\n", dummy);

  if (options->imgKeepPiInTr)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_img_keep_pi = %s\n", dummy);

  if (options->preKeepPiInTr)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_pre_keep_pi = %s\n", dummy);

  if (options->preCanonical)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "HYB: hybrid_pre_canonical = %s\n", dummy);

  switch (options->trMethod) {
  case Img_Iwls95_c :
    sprintf(dummy, "IWLS95");
    break;
  case Img_Mlp_c :
    sprintf(dummy, "MLP");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "HYB: hybrid_tr_method = %s\n", dummy);

  FREE(options);
}


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


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

  Synopsis    [Decides whether to split or to conjoin.]

  Description [Decides whether to split or to conjoin.]

  SideEffects []

******************************************************************************/
int
ImgDecideSplitOrConjoin(ImgTfmInfo_t *info, array_t *vector, mdd_t *from,
			int preFlag, array_t *relationArray,
			mdd_t *cofactorCube, mdd_t *abstractCube,
			int useBothFlag, int depth)
{
  int	conjoin = 0;
  float	lambda, improvedLambda;
  int	vectorBddSize, vectorSize;
  int	improved;
  int	minDepth;
  int	checkSpecialCases;
  int	checkImprovement;
  int	relationSize = 0;

  if (!preFlag) {
    if (vector && array_n(vector) <= 2)
      return(0); /* terminal case */
  }

  if (info->option->decideMode == 1 || info->option->decideMode == 3)
    checkSpecialCases = 1;
  else
    checkSpecialCases = 0;
  if (info->option->decideMode == 2 || info->option->decideMode == 3)
    checkImprovement = 1;
  else
    checkImprovement = 0;

  if (checkSpecialCases) {
    if (vector && array_n(vector) <= info->option->conjoinVectorSize) {
      if (preFlag)
	info->nConjoinsB++;
      else
	info->nConjoins++;
      if (info->option->printLambda) {
	fprintf(vis_stdout, "%d: conjoin - small vector size (%d)\n",
		depth, array_n(vector));
      }
      return(1);
    }
  }

  if (preFlag)
    minDepth = info->option->preSplitMinDepth;
  else
    minDepth = info->option->splitMinDepth;

  if (useBothFlag && relationArray && vector) {
    lambda = ComputeSupportLambda(info, relationArray, cofactorCube,
				  abstractCube, from, vector,
				  0, preFlag, &improvedLambda);
  } else if (relationArray) {
    if (checkSpecialCases) {
      if (array_n(relationArray) <= info->option->conjoinRelationSize ||
	  (relationSize = (int)bdd_size_multiple(relationArray)) <=
		info->option->conjoinRelationBddSize) {
	if (preFlag)
	  info->nConjoinsB++;
	else
	  info->nConjoins++;
	if (info->option->printLambda) {
	  fprintf(vis_stdout, "%d: conjoin - small relation array (%d, %ld)\n",
		  depth, array_n(relationArray),
		  bdd_size_multiple(relationArray));
	}
	return(1);
      }
    }

    lambda = ComputeSupportLambda(info, relationArray, cofactorCube,
				  abstractCube, from, NIL(array_t),
				  0, preFlag, &improvedLambda);
  } else {
    int		i;
    ImgComponent_t	*comp;

    relationArray = 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 *, relationArray, comp->func);
    }

    lambda = ComputeSupportLambda(info, relationArray, NIL(mdd_t),
				  NIL(mdd_t), from, NIL(array_t),
				  1, preFlag, &improvedLambda);

    array_free(relationArray);
  }

  if ((preFlag == 0 && lambda <= info->option->lambdaThreshold) ||
      (preFlag == 1 && lambda <= info->option->preLambdaThreshold)) {
    if (preFlag)
      info->nConjoinsB++;
    else
      info->nConjoins++;
    if (info->option->printLambda) {
      fprintf(vis_stdout, "%d: conjoin - small lambda (%.2f)\n",
	      depth, lambda);
    }
    conjoin = 1;
  } else {
    if (checkImprovement) {
      if (vector) {
	vectorBddSize = ImgVectorBddSize(vector);
	vectorSize = array_n(vector);
	if (depth == minDepth ||
	    improvedLambda >= info->option->improveLambda ||
	    ((float)vectorBddSize * 100.0 / (float)info->prevVectorBddSize) <=
		info->option->improveVectorBddSize ||
	    (info->prevVectorSize - vectorSize) >=
		info->option->improveVectorSize) {
	  improved = 1;
	} else
	  improved = 0;
	info->prevVectorBddSize = vectorBddSize;
	info->prevVectorSize = vectorSize;
      } else {
	if (relationSize)
	  vectorBddSize = relationSize;
	else
	  vectorBddSize = (int)bdd_size_multiple(relationArray);
	if (depth == minDepth ||
	    improvedLambda >= info->option->improveLambda ||
	    ((float)vectorBddSize * 100.0 / (float)info->prevVectorBddSize) <=
		info->option->improveVectorBddSize) {
	  improved = 1;
	} else
	  improved = 0;
	info->prevVectorBddSize = vectorBddSize;
      }
      if (improved) {
	if (preFlag)
	  info->nSplitsB++;
	else
	  info->nSplits++;
	if (info->option->printLambda) {
	  fprintf(vis_stdout, "%d: split - big lambda (%.2f) - improved\n",
		  depth, lambda);
	}
	conjoin = 0;
      } else {
	if (preFlag)
	  info->nConjoinsB++;
	else
	  info->nConjoins++;
	if (info->option->printLambda) {
	  fprintf(vis_stdout, "%d: conjon - big lambda (%.2f) - not improved\n",
		  depth, lambda);
	}
	conjoin = 1;
      }
    } else {
      if (preFlag)
	info->nSplitsB++;
      else
	info->nSplits++;
      if (info->option->printLambda) {
	fprintf(vis_stdout, "%d: split - big lambda (%.2f)\n",
	      depth, lambda);
      }
      conjoin = 0;
    }
  }

  return(conjoin); /* 0 : split, 1 : conjoin */
}


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

  Synopsis    [Computes an image by transition relation.]

  Description [Computes an image by transition relation.]

  SideEffects []

******************************************************************************/
mdd_t *
ImgImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from)
{
  int			i, j, nVars;
  array_t		*relationArray;
  mdd_t			*result, *domain, *relation, *var, *nextVar;
  ImgComponent_t	*comp;
  char			*support;
  array_t		*smoothVarsBddArray, *introducedVarsBddArray;
  array_t		*domainVarsBddArray;
  int			bddId;

  if (from && bdd_is_tautology(from, 0))
    return(mdd_zero(info->manager));

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

  relationArray = array_alloc(mdd_t *, 0);
  introducedVarsBddArray = array_alloc(mdd_t *, 0);

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (comp->intermediate) {
      relation = mdd_xnor(comp->var, comp->func);
      bddId = (int)bdd_top_var_id(comp->var);
      support[bddId] = 1;
    } else {
      nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
      relation = mdd_xnor(nextVar, comp->func);
      array_insert_last(mdd_t *, introducedVarsBddArray, nextVar);
    }
    array_insert_last(mdd_t *, relationArray, relation);
 
    for (j = 0; j < nVars; j++)
      support[j] = support[j] | comp->support[j];
  }

  if (from && (!bdd_is_tautology(from, 1))) {
    if (info->option->reorderWithFrom)
      array_insert_last(mdd_t *, relationArray, mdd_dup(from));

    comp = ImgComponentAlloc(info);
    comp->func = from;
    ImgComponentGetSupport(comp);
    for (i = 0; i < nVars; i++)
      support[i] = support[i] | comp->support[i];
    comp->func = NIL(mdd_t);
    ImgComponentFree(comp);
  }

  smoothVarsBddArray = array_alloc(mdd_t *, 0);
  if (!info->option->reorderWithFrom)
    domainVarsBddArray = array_alloc(mdd_t *, 0);
  else
    domainVarsBddArray = NIL(array_t);
  for (i = 0; i < nVars; i++) {
    if (support[i]) {
      var = bdd_var_with_index(info->manager, i);
      if ((!from) || info->option->reorderWithFrom)
	array_insert_last(mdd_t *, smoothVarsBddArray, var);
      else {
	if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)) ||
	    (info->intermediateVarsTable &&
	     st_lookup(info->intermediateVarsTable, (char *)(long)i,
			NIL(char *)))) {
	  array_insert_last(mdd_t *, smoothVarsBddArray, var);
	} else {
	  array_insert_last(mdd_t *, domainVarsBddArray, var);
	}
      }
    }
  }
  FREE(support);

  if ((!from) || info->option->reorderWithFrom) {
    result = ImgMultiwayLinearAndSmooth(info->manager,
					relationArray,
					smoothVarsBddArray,
					introducedVarsBddArray,
					info->option->trMethod,
					Img_Forward_c,
					info->trmOption);
  } else {
    result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
						relationArray, from,
						smoothVarsBddArray,
						domainVarsBddArray,
						introducedVarsBddArray,
						info->option->trMethod,
						Img_Forward_c,
						info->trmOption);
    mdd_array_free(domainVarsBddArray);
  }
  mdd_array_free(relationArray);
  mdd_array_free(smoothVarsBddArray);
  mdd_array_free(introducedVarsBddArray);
  domain = ImgSubstitute(result, info->functionData, Img_R2D_c);
  mdd_free(result);
  return(domain);
}


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

  Synopsis    [Computes an image by transition relation.]

  Description [Computes an image by transition relation.]

  SideEffects []

******************************************************************************/
mdd_t *
ImgImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector,
				mdd_t *from, array_t *relationArray,
				mdd_t *cofactorCube, mdd_t *abstractCube)
{
  int			i, j;
  array_t		*mergedRelationArray;
  mdd_t			*result, *domain, *relation, *var, *nextVar;
  ImgComponent_t	*comp, *supportComp;
  int			nVars;
  char			*support;
  array_t		*smoothVarsBddArray, *introducedVarsBddArray;
  array_t		*domainVarsBddArray;

  if (from && bdd_is_tautology(from, 0))
    return(mdd_zero(info->manager));

  if (cofactorCube && abstractCube) {
    if (!bdd_is_tautology(cofactorCube, 1) &&
	!bdd_is_tautology(abstractCube, 1)) {
      mergedRelationArray = ImgGetCofactoredAbstractedRelationArray(
					info->manager, relationArray,
					cofactorCube, abstractCube);
    } else if (!bdd_is_tautology(cofactorCube, 1)) {
      mergedRelationArray = ImgGetCofactoredRelationArray(relationArray,
							  cofactorCube);
    } else if (!bdd_is_tautology(abstractCube, 1)) {
      mergedRelationArray = ImgGetAbstractedRelationArray(info->manager,
							  relationArray,
							  abstractCube);
    } else
      mergedRelationArray = mdd_array_duplicate(relationArray);
  } else
    mergedRelationArray = mdd_array_duplicate(relationArray);

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

  supportComp = ImgComponentAlloc(info);
  for (i = 0; i < array_n(mergedRelationArray); i++) {
    supportComp->func = array_fetch(mdd_t *, mergedRelationArray, i);;
    ImgSupportClear(info, supportComp->support);
    ImgComponentGetSupport(supportComp);
    for (j = 0; j < nVars; j++)
      support[j] = support[j] | supportComp->support[j];
  }

  if (vector && array_n(vector) > 0) {
    for (i = 0; i < array_n(vector); i++) {
      comp = array_fetch(ImgComponent_t *, vector, i);
      if (comp->intermediate) {
	relation = mdd_xnor(comp->var, comp->func);
	support[(int)bdd_top_var_id(comp->var)] = 1;
      } else {
	nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	relation = mdd_xnor(nextVar, comp->func);
	support[(int)bdd_top_var_id(nextVar)] = 1;
	mdd_free(nextVar);
      }
      array_insert_last(mdd_t *, mergedRelationArray, relation);

      for (j = 0; j < nVars; j++)
	support[j] = support[j] | comp->support[j];
    }
  }

  if (from) {
    if ((!bdd_is_tautology(from, 1)) && info->option->reorderWithFrom)
      array_insert_last(mdd_t *, mergedRelationArray, mdd_dup(from));

    supportComp->func = from;
    ImgSupportClear(info, supportComp->support);
    ImgComponentGetSupport(supportComp);
    for (i = 0; i < nVars; i++)
      support[i] = support[i] | supportComp->support[i];
  }
  supportComp->func = NIL(mdd_t);
  ImgComponentFree(supportComp);

  smoothVarsBddArray = array_alloc(mdd_t *, 0);
  introducedVarsBddArray = array_alloc(mdd_t *, 0);
  if (!info->option->reorderWithFrom)
    domainVarsBddArray = array_alloc(mdd_t *, 0);
  else
    domainVarsBddArray = NIL(array_t);
  for (i = 0; i < nVars; i++) {
    if (support[i]) {
      var = bdd_var_with_index(info->manager, i);
      if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
	array_insert_last(mdd_t *, introducedVarsBddArray, var);
      else if ((!from) || info->option->reorderWithFrom)
	array_insert_last(mdd_t *, smoothVarsBddArray, var);
      else {
	if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)) ||
	    (info->intermediateVarsTable &&
	     st_lookup(info->intermediateVarsTable, (char *)(long)i,
			NIL(char *)))) {
	  array_insert_last(mdd_t *, smoothVarsBddArray, var);
	} else {
	  array_insert_last(mdd_t *, domainVarsBddArray, var);
	}
      }
    }
  }
  FREE(support);

  if ((!from) || info->option->reorderWithFrom) {
    result = ImgMultiwayLinearAndSmooth(info->manager,
					mergedRelationArray,
					smoothVarsBddArray,
					introducedVarsBddArray,
					info->option->trMethod,
					Img_Forward_c,
					info->trmOption);
  } else {
    result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
						mergedRelationArray, from,
						smoothVarsBddArray,
						domainVarsBddArray,
						introducedVarsBddArray,
						info->option->trMethod,
						Img_Forward_c,
						info->trmOption);
    mdd_array_free(domainVarsBddArray);
  }
  mdd_array_free(mergedRelationArray);
  mdd_array_free(smoothVarsBddArray);
  mdd_array_free(introducedVarsBddArray);

  domain = ImgSubstitute(result, info->functionData, Img_R2D_c);
  mdd_free(result);
  return(domain);
}


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

  Synopsis    [Computes a preimage by transition relation.]

  Description [Computes a preimage by transition relation.]

  SideEffects []

******************************************************************************/
mdd_t *
ImgPreImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from)
{
  int			i, j, nVars;
  array_t		*relationArray;
  mdd_t			*result, *relation, *var, *nextVar;
  ImgComponent_t	*comp;
  char			*support;
  array_t		*smoothVarsBddArray, *introducedVarsBddArray;
  array_t		*rangeVarsBddArray;
  mdd_t			*fromRange;

  if (bdd_is_tautology(from, 1))
    return(mdd_one(info->manager));
  else if (bdd_is_tautology(from, 0))
    return(mdd_zero(info->manager));

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

  relationArray = array_alloc(mdd_t *, 0);

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (comp->intermediate) {
      relation = mdd_xnor(comp->var, comp->func);
      support[(int)bdd_top_var_id(comp->var)] = 1;
    } else {
      nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
      relation = mdd_xnor(nextVar, comp->func);
      support[(int)bdd_top_var_id(nextVar)] = 1;
      mdd_free(nextVar);
    }
    array_insert_last(mdd_t *, relationArray, relation);
 
    for (j = 0; j < nVars; j++)
      support[j] = support[j] | comp->support[j];
  }

  fromRange = ImgSubstitute(from, info->functionData, Img_D2R_c);
  comp = ImgComponentAlloc(info);
  comp->func = fromRange;
  ImgComponentGetSupport(comp);
  for (i = 0; i < nVars; i++)
    support[i] = support[i] | comp->support[i];
  comp->func = NIL(mdd_t);
  ImgComponentFree(comp);

  smoothVarsBddArray = array_alloc(mdd_t *, 0);
  introducedVarsBddArray = array_alloc(mdd_t *, 0);
  if (!info->option->preReorderWithFrom)
    rangeVarsBddArray = array_alloc(mdd_t *, 0);
  else
    rangeVarsBddArray = NIL(array_t);
  for (i = 0; i < nVars; i++) {
    if (support[i]) {
      var = bdd_var_with_index(info->manager, i);
      if (info->intermediateVarsTable &&
	  st_lookup(info->intermediateVarsTable, (char *)(long)i,
		    NIL(char *))) {
	array_insert_last(mdd_t *, smoothVarsBddArray, var);
      } else if (st_lookup(info->rangeVarsTable, (char *)(long)i,
			   NIL(char *))) {
	if (info->option->preReorderWithFrom)
	  array_insert_last(mdd_t *, smoothVarsBddArray, var);
	else
	  array_insert_last(mdd_t *, rangeVarsBddArray, var);
      } else {
	if (info->preKeepPiInTr)
	  array_insert_last(mdd_t *, introducedVarsBddArray, var);
	else {
	  if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
			NIL(char *))) {
	    array_insert_last(mdd_t *, smoothVarsBddArray, var);
	  } else
	    array_insert_last(mdd_t *, introducedVarsBddArray, var);
	}
      }
    }
  }
  FREE(support);

  if (info->option->preReorderWithFrom) {
    array_insert_last(mdd_t *, relationArray, fromRange);
    result = ImgMultiwayLinearAndSmooth(info->manager,
					relationArray,
					smoothVarsBddArray,
					introducedVarsBddArray,
					info->option->trMethod,
					Img_Backward_c,
					info->trmOption);
  } else {
    result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
						relationArray, fromRange,
						smoothVarsBddArray,
						rangeVarsBddArray,
						introducedVarsBddArray,
						info->option->trMethod,
						Img_Backward_c,
						info->trmOption);
    mdd_free(fromRange);
    mdd_array_free(rangeVarsBddArray);
  }
  mdd_array_free(relationArray);
  mdd_array_free(smoothVarsBddArray);
  mdd_array_free(introducedVarsBddArray);
  return(result);
}


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

  Synopsis    [Computes a preimage by transition relation.]

  Description [Computes a preimage by transition relation.]

  SideEffects []

******************************************************************************/
mdd_t *
ImgPreImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector,
				   mdd_t *from, array_t *relationArray,
				   mdd_t *cofactorCube, mdd_t *abstractCube)
{
  int			i, j;
  array_t		*mergedRelationArray;
  mdd_t			*result, *relation, *var, *nextVar, *fromRange;
  ImgComponent_t	*comp, *supportComp;
  int			nVars;
  char			*support;
  array_t		*smoothVarsBddArray, *introducedVarsBddArray;
  array_t		*rangeVarsBddArray;

  if (bdd_is_tautology(from, 1))
    return(mdd_one(info->manager));
  if (bdd_is_tautology(from, 0))
    return(mdd_zero(info->manager));

  if (cofactorCube && abstractCube) {
    if (!bdd_is_tautology(cofactorCube, 1) &&
	!bdd_is_tautology(abstractCube, 1)) {
      mergedRelationArray = ImgGetCofactoredAbstractedRelationArray(
					info->manager, relationArray,
					cofactorCube, abstractCube);
    } else if (!bdd_is_tautology(cofactorCube, 1)) {
      mergedRelationArray = ImgGetCofactoredRelationArray(relationArray,
							  cofactorCube);
    } else if (!bdd_is_tautology(abstractCube, 1)) {
      mergedRelationArray = ImgGetAbstractedRelationArray(info->manager,
							  relationArray,
							  abstractCube);
    } else
      mergedRelationArray = mdd_array_duplicate(relationArray);
  } else
    mergedRelationArray = mdd_array_duplicate(relationArray);

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

  supportComp = ImgComponentAlloc(info);
  for (i = 0; i < array_n(mergedRelationArray); i++) {
    supportComp->func = array_fetch(mdd_t *, mergedRelationArray, i);;
    ImgSupportClear(info, supportComp->support);
    ImgComponentGetSupport(supportComp);
    for (j = 0; j < nVars; j++)
      support[j] = support[j] | supportComp->support[j];
  }

  if (vector && array_n(vector) > 0) {
    for (i = 0; i < array_n(vector); i++) {
      comp = array_fetch(ImgComponent_t *, vector, i);
      if (comp->intermediate) {
	relation = mdd_xnor(comp->var, comp->func);
	support[(int)bdd_top_var_id(comp->var)] = 1;
      } else {
	nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
	relation = mdd_xnor(nextVar, comp->func);
	support[(int)bdd_top_var_id(nextVar)] = 1;
	mdd_free(nextVar);
      }
      array_insert_last(mdd_t *, mergedRelationArray, relation);

      for (j = 0; j < nVars; j++)
	support[j] = support[j] | comp->support[j];
    }
  }

  fromRange = ImgSubstitute(from, info->functionData, Img_D2R_c);
  supportComp->func = fromRange;
  ImgSupportClear(info, supportComp->support);
  ImgComponentGetSupport(supportComp);
  for (i = 0; i < nVars; i++)
    support[i] = support[i] | supportComp->support[i];
  supportComp->func = NIL(mdd_t);
  ImgComponentFree(supportComp);

  smoothVarsBddArray = array_alloc(mdd_t *, 0);
  introducedVarsBddArray = array_alloc(mdd_t *, 0);
  if (!info->option->preReorderWithFrom)
    rangeVarsBddArray = array_alloc(mdd_t *, 0);
  else
    rangeVarsBddArray = NIL(array_t);
  for (i = 0; i < nVars; i++) {
    if (support[i]) {
      var = bdd_var_with_index(info->manager, i);
      if (info->intermediateVarsTable &&
	  st_lookup(info->intermediateVarsTable, (char *)(long)i,
		    NIL(char *))) {
	array_insert_last(mdd_t *, smoothVarsBddArray, var);
      } else if (st_lookup(info->rangeVarsTable, (char *)(long)i,
			   NIL(char *))) {
	if (info->option->preReorderWithFrom)
	  array_insert_last(mdd_t *, smoothVarsBddArray, var);
	else
	  array_insert_last(mdd_t *, rangeVarsBddArray, var);
      } else {
	if (info->preKeepPiInTr)
	  array_insert_last(mdd_t *, introducedVarsBddArray, var);
	else {
	  if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
			NIL(char *))) {
	    array_insert_last(mdd_t *, smoothVarsBddArray, var);
	  } else
	    array_insert_last(mdd_t *, introducedVarsBddArray, var);
	}
      }
    }
  }
  FREE(support);

  if (info->option->preReorderWithFrom) {
    array_insert_last(mdd_t *, mergedRelationArray, fromRange);
    result = ImgMultiwayLinearAndSmooth(info->manager,
					mergedRelationArray,
					smoothVarsBddArray,
					introducedVarsBddArray,
					info->option->trMethod,
					Img_Backward_c,
					info->trmOption);
  } else {
    result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
						mergedRelationArray, fromRange,
						smoothVarsBddArray,
						rangeVarsBddArray,
						introducedVarsBddArray,
						info->option->trMethod,
						Img_Backward_c,
						info->trmOption);
    mdd_free(fromRange);
    mdd_array_free(rangeVarsBddArray);
  }
  mdd_array_free(mergedRelationArray);
  mdd_array_free(smoothVarsBddArray);
  mdd_array_free(introducedVarsBddArray);

  return(result);
}


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

  Synopsis    [Checks whether a vector is equivalent to a relation array.]

  Description [Checks whether a vector is equivalent to a relation array.]

  SideEffects []

******************************************************************************/
int
ImgCheckEquivalence(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray,
		    mdd_t *cofactorCube, mdd_t *abstractCube, int preFlag)
{
  int			i, equal;
  mdd_t			*product1, *product2;
  mdd_t			*var, *tmp, *relation;
  ImgComponent_t	*comp;
  array_t		*newRelationArray, *tmpRelationArray;
  array_t		*domainVarBddArray, *quantifyVarBddArray;

  tmpRelationArray = array_alloc(mdd_t *, 0);
  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (comp->intermediate)
      relation = mdd_xnor(comp->var, comp->func);
    else {
      var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
      relation = mdd_xnor(var, comp->func);
      mdd_free(var);
    }
    array_insert_last(mdd_t *, tmpRelationArray, relation);
  }

  if (preFlag) {
    if (info->preKeepPiInTr) {
      quantifyVarBddArray = array_alloc(mdd_t *, 0);
      domainVarBddArray = array_join(info->domainVarBddArray,
				     info->quantifyVarBddArray);
    } else {
      quantifyVarBddArray = info->quantifyVarBddArray;
      domainVarBddArray = info->domainVarBddArray;
    }
    newRelationArray = ImgClusterRelationArray(info->manager,
	info->functionData, info->option->trMethod, Img_Backward_c,
	info->trmOption, tmpRelationArray, domainVarBddArray,
	quantifyVarBddArray, info->rangeVarBddArray,
	NIL(array_t *), NIL(array_t *), 0);
    if (info->preKeepPiInTr) {
      array_free(quantifyVarBddArray);
      array_free(domainVarBddArray);
    }
  } else {
    newRelationArray = ImgClusterRelationArray(info->manager,
	info->functionData, info->option->trMethod, Img_Forward_c,
	info->trmOption, tmpRelationArray, info->domainVarBddArray,
	info->quantifyVarBddArray, info->rangeVarBddArray,
	NIL(array_t *), NIL(array_t *), 0);
  }
  mdd_array_free(tmpRelationArray);

  product1 = mdd_one(info->manager);
  for (i = 0; i < array_n(newRelationArray); i++) {
    relation = array_fetch(mdd_t *, newRelationArray, i);
    tmp = product1;
    product1 = mdd_and(tmp, relation, 1, 1);
    mdd_free(tmp);
  }
  mdd_array_free(newRelationArray);

  if (cofactorCube && abstractCube) {
    newRelationArray = ImgGetCofactoredAbstractedRelationArray(info->manager,
				relationArray, cofactorCube, abstractCube);
  } else
    newRelationArray = relationArray;

  product2 = mdd_one(info->manager);
  for (i = 0; i < array_n(newRelationArray); i++) {
    relation = array_fetch(mdd_t *, newRelationArray, i);
    tmp = product2;
    product2 = mdd_and(tmp, relation, 1, 1);
    mdd_free(tmp);
  }

  if (newRelationArray != relationArray)
    mdd_array_free(newRelationArray);

  if (mdd_equal(product1, product2))
    equal = 1;
  else
    equal = 0;

  mdd_free(product1);
  mdd_free(product2);

  return(equal);
}


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

  Synopsis    [Checks whether a vector corresponds to its relation array.]

  Description [Checks whether a vector corresponds to its relation array.
  This function is used only for debugging with image_cluster_size = 1.
  Checks each function vector whether its relation exists in the transition
  relation.]

  SideEffects []

******************************************************************************/
int
ImgCheckMatching(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray)
{
  int			i, equal = 1;
  mdd_t			*var, *relation;
  ImgComponent_t	*comp;
  st_table		*relationTable;
  int			*ptr;

  relationTable = st_init_table(st_ptrcmp, st_ptrhash);

  for (i = 0; i < array_n(relationArray); i++) {
    relation = array_fetch(mdd_t *, relationArray, i);
    ptr = (int *)bdd_pointer(relation);
    st_insert(relationTable, (char *)ptr, NULL);
  }

  for (i = 0; i < array_n(vector); i++) {
    comp = array_fetch(ImgComponent_t *, vector, i);
    if (comp->intermediate)
      relation = mdd_xnor(comp->var, comp->func);
    else {
      var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
      relation = mdd_xnor(var, comp->func);
      mdd_free(var);
    }
    ptr = (int *)bdd_pointer(relation);
    if (!st_lookup(relationTable, (char *)ptr, NULL)) {
      if (comp->intermediate) {
	fprintf(vis_stderr,
		"Error : relation of varId[%d - intermediate] not found\n",
		(int)bdd_top_var_id(comp->var));
      } else {
	fprintf(vis_stderr, "Error : relation of varId[%d] not found\n",
		(int)bdd_top_var_id(comp->var));
      }
      equal = 0;
    }
    mdd_free(relation);
  }

  st_free_table(relationTable);
  return(equal);
}


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


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

  Synopsis    [Computes variable lifetime lambda.]

  Description [Computes variable lifetime lambda. newRelationFlag is 1 when
  relationArray is made from the function vector directly, in other words,
  relationArray is an array of next state functions in this case.]

  SideEffects []

******************************************************************************/
static float
ComputeSupportLambda(ImgTfmInfo_t *info, array_t *relationArray,
			mdd_t *cofactorCube, mdd_t *abstractCube,
			mdd_t *from, array_t *vector, int newRelationFlag,
			int preFlag, float *improvedLambda)
{
  array_t		*newRelationArray, *clusteredRelationArray;
  ImgComponent_t	*comp;
  int			i, j, nVars, nSupports;
  mdd_t			*newFrom, *var;
  char			*support;
  array_t		*smoothVarsBddArray, *introducedVarsBddArray;
  array_t		*domainVarsBddArray;
  array_t		*smoothSchedule, *smoothVars;
  float			lambda;
  int			size, total, lifetime;
  Img_DirectionType	direction;
  int			lambdaWithFrom, prevArea;
  array_t		*orderedRelationArray;
  int			nIntroducedVars;
  int			*highest, *lowest;
  mdd_t			*relation;
  int			asIs;

  if (cofactorCube && abstractCube) {
    newRelationArray = ImgGetCofactoredAbstractedRelationArray(info->manager,
			      relationArray, cofactorCube, abstractCube);
    if (from && info->option->lambdaWithFrom) {
      if (preFlag)
	newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
      else
	newFrom = mdd_dup(from);
      array_insert_last(mdd_t *, newRelationArray, newFrom);
      lambdaWithFrom = 1;
    } else {
      lambdaWithFrom = 0;
      newFrom = NIL(mdd_t);
    }
  } else {
    if (from && info->option->lambdaWithFrom) {
      if (newRelationFlag) {
	newRelationArray = relationArray;
	if (preFlag)
	  newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
	else
	  newFrom = from;
      } else {
	/* We don't want to modify the original relation array */
	newRelationArray = mdd_array_duplicate(relationArray);
	if (preFlag)
	  newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
	else
	  newFrom = mdd_dup(from);
      }
      array_insert_last(mdd_t *, newRelationArray, newFrom);
      lambdaWithFrom = 1;
    } else {
      newRelationArray = relationArray;
      newFrom = NIL(mdd_t);
      lambdaWithFrom = 0;
    }
  }

  if (vector) {
    for (i = 0; i < array_n(vector); i++) {
      comp = array_fetch(ImgComponent_t *, vector, i);
      array_insert_last(mdd_t *, newRelationArray, mdd_dup(comp->func));
    }
  }

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

  comp = ImgComponentAlloc(info);
  for (i = 0; i < array_n(newRelationArray); i++) {
    comp->func = array_fetch(mdd_t *, newRelationArray, i);;
    ImgSupportClear(info, comp->support);
    ImgComponentGetSupport(comp);
    for (j = 0; j < nVars; j++)
      support[j] = support[j] | comp->support[j];
  }
  comp->func = NIL(mdd_t);
  ImgComponentFree(comp);

  nSupports = 0;
  smoothVarsBddArray = array_alloc(mdd_t *, 0);
  domainVarsBddArray = array_alloc(mdd_t *, 0);
  introducedVarsBddArray = array_alloc(mdd_t *, 0);
  for (i = 0; i < nVars; i++) {
    if (support[i]) {
      var = bdd_var_with_index(info->manager, i);
      if (preFlag) {
	if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
	  if (lambdaWithFrom)
	    array_insert_last(mdd_t *, smoothVarsBddArray, var);
	  else
	    array_insert_last(mdd_t *, domainVarsBddArray, var);
	  if (info->option->preLambdaMode == 0 ||
	      info->option->preLambdaMode == 2)
	    nSupports++;
	} else {
	  if (info->preKeepPiInTr) {
	    if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
			NIL(char *))) {
	      array_insert_last(mdd_t *, introducedVarsBddArray, var);
	      nSupports++;
	    } else if (info->intermediateVarsTable &&
			st_lookup(info->intermediateVarsTable, (char *)(long)i,
				NIL(char *))) {
	      array_insert_last(mdd_t *, smoothVarsBddArray, var);
	      nSupports++;
	    } else { /* ps variables */
	      array_insert_last(mdd_t *, introducedVarsBddArray, var);
	      if (info->option->preLambdaMode != 0)
		nSupports++;
	    }
	  } else {
	    if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
			  NIL(char *)) ||
		(info->intermediateVarsTable &&
		 st_lookup(info->intermediateVarsTable, (char *)(long)i,
			   NIL(char *)))) {
	      array_insert_last(mdd_t *, smoothVarsBddArray, var);
	      nSupports++;
	    } else { /* ps variables */
	      array_insert_last(mdd_t *, introducedVarsBddArray, var);
	      if (info->option->preLambdaMode != 0)
		nSupports++;
	    }
	  }
	}
      } else { /* image computation */
	if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
	  array_insert_last(mdd_t *, introducedVarsBddArray, var);
	  if (info->option->lambdaMode == 2)
	    nSupports++;
	} else {
	  if (lambdaWithFrom)
	    array_insert_last(mdd_t *, smoothVarsBddArray, var);
	  else {
	    if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
			  NIL(char *)) ||
		(info->intermediateVarsTable &&
		 st_lookup(info->intermediateVarsTable, (char *)(long)i,
			   NIL(char *)))) {
	      array_insert_last(mdd_t *, smoothVarsBddArray, var);
	    } else
	      array_insert_last(mdd_t *, domainVarsBddArray, var);
	  }
	  nSupports++;
	}
      }
    }
  }

  if (preFlag)
    direction = Img_Backward_c;
  else
    direction = Img_Forward_c;

  if (info->option->lambdaFromMlp) {
    FREE(support);
    if (info->option->lambdaWithClustering) {
      ImgMlpClusterRelationArray(info->manager, info->functionData,
			newRelationArray, domainVarsBddArray,
			smoothVarsBddArray, introducedVarsBddArray,
			direction, &clusteredRelationArray, NIL(array_t *),
			info->trmOption);
      if (newRelationArray != relationArray)
	mdd_array_free(newRelationArray);
      newRelationArray = clusteredRelationArray;
    }
    prevArea = info->prevTotal;
    asIs = newRelationFlag ? 0 : 1; /* 0 when relationArray is an array of
				       functions, i.e. without next state
				       variables */
    lambda = ImgMlpComputeLambda(info->manager, newRelationArray,
			domainVarsBddArray, smoothVarsBddArray,
			introducedVarsBddArray, direction,
			info->option->lambdaMode, asIs, &prevArea,
			improvedLambda, info->trmOption);
    info->prevTotal = prevArea;
  } else {
    smoothSchedule = ImgGetQuantificationSchedule(info->manager,
			info->functionData, info->option->trMethod,
			direction, info->trmOption, newRelationArray,
			smoothVarsBddArray, domainVarsBddArray,
			introducedVarsBddArray,
			info->option->lambdaWithClustering,
			&orderedRelationArray);

    if (direction == Img_Forward_c) {
      size = array_n(smoothSchedule);
      lifetime = 0;
      if (info->option->lambdaMode == 0) { /* total lifetime (lambda) */
	for (i = 1; i < size; i++) {
	  smoothVars = array_fetch(array_t *, smoothSchedule, i);
	  lifetime += array_n(smoothVars) * i;
	}
	total = nSupports * (size - 1);
      } else if (info->option->lambdaMode == 1) { /* active lifetime (lambda) */
	lowest = ALLOC(int, sizeof(int) * nVars);
	for (i = 0; i < nVars; i++)
	  lowest[i] = nVars;
	highest = ALLOC(int, sizeof(int) * nVars);
	memset(highest, 0, sizeof(int) * nVars);

	comp = ImgComponentAlloc(info);
	for (i = 0; i < size - 1; i++) {
	  relation = array_fetch(mdd_t *, orderedRelationArray, i);
	  comp->func = relation;
	  ImgSupportClear(info, comp->support);
	  ImgComponentGetSupport(comp);
	  for (j = 0; j < nVars; j++) {
	    if (!comp->support[j])
	      continue;
	    if (st_lookup(info->rangeVarsTable, (char *)(long)j, NIL(char *)))
	      continue;
	    if (i < lowest[j])
	      lowest[j] = i;
	    if (i > highest[j])
	      highest[j] = i;
	  }
	}
	comp->func = NIL(mdd_t);
	ImgComponentFree(comp);

	for (i = 0; i < nVars; i++) {
	  if (lowest[i] == nVars)
	    continue;
	  if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
	    continue;
	  lifetime += highest[i] - lowest[i] + 1;
	}

	if (newRelationFlag)
	  lifetime += array_n(newRelationArray);
	total = nSupports * (size - 1);

	FREE(lowest);
	FREE(highest);
      } else { /* total lifetime (lambda) with introduced variables */
	for (i = 1; i < size; i++) {
	  smoothVars = array_fetch(array_t *, smoothSchedule, i);
	  lifetime += array_n(smoothVars) * i;
	}

	if (newRelationFlag) {
	  nIntroducedVars = array_n(newRelationArray);
	  lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
	} else {
	  comp = ImgComponentAlloc(info);
	  for (i = 0; i < size - 1; i++) {
	    relation = array_fetch(mdd_t *, orderedRelationArray, i);
	    comp->func = relation;
	    ImgSupportClear(info, comp->support);
	    ImgComponentGetSupport(comp);
	    nIntroducedVars = 0;
	    for (j = 0; j < nVars; j++) {
	      if (!comp->support[j])
		continue;
	      if (st_lookup(info->rangeVarsTable, (char *)(long)j, NIL(char *)))
		nIntroducedVars++;
	    }
	    lifetime += (size - i - 1) * nIntroducedVars;
	  }
	  comp->func = NIL(mdd_t);
	  ImgComponentFree(comp);
	}
	total = nSupports * (size - 1);
      }
      mdd_array_array_free(smoothSchedule);
    } else if (info->option->preLambdaMode == 0) { /* total lifetime (lambda) */
      /* direction == Img_Backward_c */
      size = array_n(smoothSchedule);
      lifetime = 0;
      for (i = 1; i < size; i++) {
	smoothVars = array_fetch(array_t *, smoothSchedule, i);
	lifetime += array_n(smoothVars) * i;
      }
      total = nSupports * (size - 1);
      mdd_array_array_free(smoothSchedule);
    } else { /* direction == Img_Backward_c */
      size = array_n(smoothSchedule);
      mdd_array_array_free(smoothSchedule);
      lifetime = 0;

      lowest = ALLOC(int, sizeof(int) * nVars);
      for (i = 0; i < nVars; i++)
	lowest[i] = nVars;
      highest = ALLOC(int, sizeof(int) * nVars);
      memset(highest, 0, sizeof(int) * nVars);

      comp = ImgComponentAlloc(info);
      for (i = 0; i < size - 1; i++) {
	relation = array_fetch(mdd_t *, orderedRelationArray, i);
	comp->func = relation;
	ImgSupportClear(info, comp->support);
	ImgComponentGetSupport(comp);
	for (j = 0; j < nVars; j++) {
	  if (!comp->support[j])
	    continue;
	  if (i < lowest[j])
	    lowest[j] = i;
	  if (i > highest[j])
	    highest[j] = i;
	}
      }
      comp->func = NIL(mdd_t);
      ImgComponentFree(comp);

      if (info->option->preLambdaMode == 1) { /* active lifetime (lambda) */
	for (i = 0; i < nVars; i++) {
	  if (lowest[i] == nVars)
	    continue;
	  if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)) ||
		st_lookup(info->quantifyVarsTable, (char *)(long)i,
			       NIL(char *)) ||
		(info->intermediateVarsTable &&
		 st_lookup(info->intermediateVarsTable, (char *)(long)i,
			       NIL(char *)))) {
	    lifetime += highest[i] - lowest[i] + 1;
	  }
	}
	if (newRelationFlag)
	  lifetime += array_n(newRelationArray);
	total = nSupports * (size - 1);
      } else if (info->option->preLambdaMode == 2) {
	/* total lifetime (lambda) with introduced variables */
	for (i = 0; i < nVars; i++) {
	  if (lowest[i] == nVars)
	    continue;
	  if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)) ||
	      st_lookup(info->quantifyVarsTable, (char *)(long)i,
			NIL(char *)) ||
	      (info->intermediateVarsTable &&
	       st_lookup(info->intermediateVarsTable, (char *)(long)i,
			NIL(char *)))) {
	    lifetime += highest[i] + 1;
	  } else {
	    lifetime += size - lowest[i] - 1;
	  }
	}
	if (newRelationFlag) {
	  nIntroducedVars = array_n(newRelationArray);
	  lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
	}
	total = nSupports * (size - 1);
      } else { /* total lifetime (lambda) with ps/pi variables */
	for (i = 0; i < nVars; i++) {
	  if (lowest[i] == nVars)
	    continue;
	  if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
	    continue;
	  if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
			NIL(char *)) ||
	      (info->intermediateVarsTable &&
	       st_lookup(info->intermediateVarsTable, (char *)(long)i,
			NIL(char *)))) {
	    lifetime += highest[i] + 1;
	  } else {
	    lifetime += size - lowest[i] - 1;
	  }
	}
	if (newRelationFlag) {
	  nIntroducedVars = array_n(newRelationArray);
	  lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
	}
	total = nSupports * (size - 1);
      }

      FREE(lowest);
      FREE(highest);
    }

    FREE(support);
    mdd_array_free(orderedRelationArray);

    if (total == 0.0) {
      lambda = 0.0;
      *improvedLambda = 0.0;
    } else {
      lambda = (float)lifetime / (float)total;
      if (info->prevTotal) {
	*improvedLambda = info->prevLambda -
			  (float)lifetime / (float)info->prevTotal;
      } else
	*improvedLambda = 0.0;
    }
    info->prevTotal = total;
  }

  mdd_array_free(smoothVarsBddArray);
  mdd_array_free(domainVarsBddArray);
  mdd_array_free(introducedVarsBddArray);
  if (newRelationArray != relationArray)
    mdd_array_free(newRelationArray);
  if (newRelationFlag && from && info->option->lambdaWithFrom &&
	newFrom != from) {
    mdd_free(newFrom);
  }

  if (info->option->verbosity >= 2) {
    if (preFlag)
      fprintf(vis_stdout, "** tfm info: lambda for preimage = %.2f\n", lambda);
    else
      fprintf(vis_stdout, "** tfm info: lambda for image = %.2f\n", lambda);
  }

  info->prevLambda = lambda;
  return(lambda);
}