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

  FileName    [imgTfmCache.c]

  PackageName [img]

  Synopsis    [Routines for image cache in transition function method.]

  SeeAlso     [imgTfm.c imgTfmFwd.c imgTfmBwd.c imgTfmUtil.c]

  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: imgTfmCache.c,v 1.8 2005/04/23 14:30:54 jinh Exp $";

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

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

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

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

static	int		ComplementFlag; /* If set, returns the negation of the
					   result from cache */
static	array_t		*SubstituteVector; /* returns the result from cache by
					      substituting the variables */
static	ImgCacheTable_t	*ImgGlobalCache; /* global image cache */
static	ImgCacheTable_t	*PreGlobalCache; /* global preimage cache */
static	int		ImgGlobalCacheRef; /* the number of image-info
					      refering to the image cache */
static	int		PreGlobalCacheRef; /* the number of image-info
					      refering to the preimage cache */

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


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

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

static void CacheDestroyEntry(ImgCacheEntry_t *entry, boolean freeEntry);
static int VectorHash(ImgCacheTable_t *table, array_t *delta, bdd_t *constraint);
static int VectorStHash(char *key, int modulus);
static int KeyStHash(char *key, int modulus);
static int VectorCompare(array_t *vector1, array_t *vector2);
static int VectorSortCompare(array_t *vector1, array_t *vector2);
static int VectorSortCompareWithConstraint(array_t *vector1, array_t *vector2);
static int ImageKeyCompare(ImgCacheStKey_t *key1, ImgCacheStKey_t *key2);
static int ImageKeySortCompare(ImgCacheStKey_t *key1, ImgCacheStKey_t *key2);
static int PreImageKeyCompare(ImgCacheStKey_t *key1, ImgCacheStKey_t *key2);
static mdd_t * SubstituteCacheResult(ImgTfmInfo_t *info, array_t *keyVector, array_t *cacheVector, mdd_t *result);
static mdd_t * SubstituteCacheResultRecur(mdd_t *result, array_t *varArray, array_t *funcArray, int pos);

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


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


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

  Synopsis    [Gets the statistics of image cache of transition function
  method.]

  Description [Gets the statistics of image cache of transition function
  method]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Img_TfmGetCacheStatistics(Img_ImageInfo_t *imageInfo, int preFlag,
			  double *inserts, double *lookups, double *hits,
			  double *entries, int *nSlots, int *maxChainLength)
{
  ImgTfmInfo_t		*info;
  ImgCacheTable_t	*cache;

  if (imageInfo) {
    if (imageInfo->methodType != Img_Tfm_c &&
	imageInfo->methodType != Img_Hybrid_c) {
      return(0);
    }

    info = (ImgTfmInfo_t *)imageInfo->methodData;
    if (!info->option->useCache)
      return(0);

    if (preFlag)
      cache = info->preCache;
    else
      cache = info->imgCache;
    if (!cache)
      return(0);
  } else {
    if (preFlag)
      cache = PreGlobalCache;
    else
      cache = ImgGlobalCache;
    if (!cache)
      return(0);
  }

  *inserts = cache->inserts;
  *lookups = cache->lookups;
  *hits = cache->hits;
  *entries = cache->entries;
  if (cache->stTable) {
    *nSlots = 0;
    *maxChainLength = 0;
  } else {
    *nSlots = cache->nSlots;
    *maxChainLength = cache->maxChainLength;
  }
  return(1);
}


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

  Synopsis    [Checks whether a global cache is used for transition function
  method.]

  Description [Checks whether a global cache is used for transition function
  method. If it is, returns 1, otherwise returns 0.
  A global cache can be used when all image-info structs store the results
  into one image cache. A local cache is used for each image-info struct stores
  its results into its own image cache.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Img_TfmCheckGlobalCache(int preFlag)
{
  if (preFlag) {
    if (PreGlobalCache)
      return(1);
    else
      return(0);
  } else {
    if (ImgGlobalCache)
      return(1);
    else
      return(0);
  }
}


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

  Synopsis    [Prints the statistics of image cache of transition function
  method.]

  Description [Prints the statistics of image cache of transition function
  method.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Img_TfmPrintCacheStatistics(Img_ImageInfo_t *imageInfo, int preFlag)
{
  ImgTfmInfo_t		*info;
  ImgCacheTable_t	*cache;

  if (imageInfo) {
    if (imageInfo->methodType != Img_Tfm_c &&
	imageInfo->methodType != Img_Hybrid_c) {
      return;
    }

    info = (ImgTfmInfo_t *)imageInfo->methodData;
    if (!info->option->useCache)
      return;

    if (preFlag)
      cache = info->preCache;
    else
      cache = info->imgCache;
    if (!cache)
      return;
  } else {
    if (preFlag)
      cache = PreGlobalCache;
    else
      cache = ImgGlobalCache;
    if (!cache)
      return;
  }
  ImgPrintCacheStatistics(cache);
}


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

  Synopsis    [Frees all cache contents of image computation using transition
  function method.]

  Description [Frees all cache contents of image computation using transition
  function method. This function is to free the cache contents only when
  requested and when tfm_auto_flush_cache is off.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Img_TfmFlushCache(Img_ImageInfo_t *imageInfo, int preFlag)
{
  ImgTfmInfo_t	*info;

  if (imageInfo) {
    if (imageInfo->methodType != Img_Tfm_c &&
	imageInfo->methodType != Img_Hybrid_c) {
      return;
    }

    info = (ImgTfmInfo_t *)imageInfo->methodData;

    if (info->option->autoFlushCache == 0) {
      if (preFlag)
	ImgFlushCache(info->preCache);
      else
	ImgFlushCache(info->imgCache);
    }
  }
}


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


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

  Synopsis    [Initializes a cache table.]

  Description [Initializes a cache table.]

  SideEffects []

******************************************************************************/
void
ImgCacheInitTable(ImgTfmInfo_t *info, int num_slot, int globalCache,
		boolean preImgFlag)
{
  ImgCacheTable_t	*table;
  ImgTfmOption_t	*option = info->option;

  if (globalCache) {
    if (preImgFlag && PreGlobalCache) {
      info->preCache = PreGlobalCache;
      PreGlobalCacheRef++;
      return;
    } else if (!preImgFlag && ImgGlobalCache) {
      info->imgCache = ImgGlobalCache;
      ImgGlobalCacheRef++;
      return;
    }
  }

  table = ALLOC(ImgCacheTable_t, 1);
  memset(table, 0, sizeof(ImgCacheTable_t));
  table->nSlots = num_slot;
  if (option->useCache == 2) {
    if (preImgFlag)
      table->stTable = st_init_table((ST_PFICPCP)PreImageKeyCompare,
				     KeyStHash);
    else if (info->useConstraint && option->sortVectorFlag)
      table->stTable = st_init_table((ST_PFICPCP)ImageKeySortCompare,
				     KeyStHash);
    else if (info->useConstraint)
      table->stTable = st_init_table((ST_PFICPCP)ImageKeyCompare,
				     KeyStHash);
    else if (option->sortVectorFlag)
      table->stTable = st_init_table((ST_PFICPCP)VectorSortCompare,
				     VectorStHash);
    else
      table->stTable = st_init_table((ST_PFICPCP)VectorCompare,
				     VectorStHash);
  } else {
    table->slot = ALLOC(ImgCacheEntry_t *, num_slot);
    memset(table->slot, 0, sizeof(ImgCacheEntry_t *) * num_slot);
  }
  table->maxChainLength = option->maxChainLength;
  table->preImgFlag = preImgFlag;
  table->useConstraint = info->useConstraint;
  if (preImgFlag) {
    table->compareFunc = VectorCompare;
    info->preCache = table;
  } else {
    if (option->sortVectorFlag) {
      if (info->useConstraint)
	table->compareFunc = VectorSortCompareWithConstraint;
      else
	table->compareFunc = VectorSortCompare;
    } else
      table->compareFunc = VectorCompare;
    info->imgCache = table;
  }

  if (globalCache) {
    if (preImgFlag) {
      PreGlobalCache = table;
      PreGlobalCacheRef = 1;
    } else {
      ImgGlobalCache = table;
      ImgGlobalCacheRef = 1;
    }
  }
}


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

  Synopsis    [Destroys a cache table.]

  Description [Destroys a cache table.]

  SideEffects []

******************************************************************************/
void
ImgCacheDestroyTable(ImgCacheTable_t *table, int globalCache)
{
  unsigned int		i;
  ImgCacheEntry_t	*entry, *next;
  array_t		*vector;
  bdd_t			*result;
  st_generator		*stGen;
  ImgCacheStKey_t	*key;

  if (globalCache) {
    if (table->preImgFlag) {
      PreGlobalCacheRef--;
      if (PreGlobalCacheRef > 0)
	return;
    } else {
      ImgGlobalCacheRef--;
      if (ImgGlobalCacheRef > 0)
	return;
    }
  }

  if (table->stTable) {
    if (table->preImgFlag || table->useConstraint) {
      st_foreach_item(table->stTable, stGen, &key, &result) {
	ImgVectorFree(key->vector);
	if (key->constraint)
	  mdd_free(key->constraint);
	FREE(key);
	mdd_free(result);
      }
    } else {
      st_foreach_item(table->stTable, stGen, &vector, &result) {
	ImgVectorFree(vector);
	mdd_free(result);
      }
    }
    st_free_table(table->stTable);
  } else {
    for (i = 0; i < table->nSlots; i++) {
      entry = table->slot[i];
      while (entry != NIL(ImgCacheEntry_t)) {
	next = entry->next;
	CacheDestroyEntry(entry, TRUE);
	entry = next;
      }
    }
    FREE(table->slot);
  }

  if (globalCache) {
    if (table->preImgFlag)
      PreGlobalCache = NIL(ImgCacheTable_t);
    else
      ImgGlobalCache = NIL(ImgCacheTable_t);
  }

  FREE(table);
}


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

  Synopsis    [Lookups cache table.]

  Description [Lookups cache table.]

  SideEffects []

******************************************************************************/
bdd_t *
ImgCacheLookupTable(ImgTfmInfo_t *info, ImgCacheTable_t *table, array_t *delta,
		    bdd_t *constraint)
{
  int			slot;
  ImgCacheEntry_t	*entry;
  bdd_t			*result, *newResult;
  int			*ptr1, *ptr2;
  ImgCacheStKey_t	key;

  table->lookups += 1.0;

  /* lossless cache */
  if (table->stTable) {
    if (table->preImgFlag) {
      key.vector = delta;
      key.constraint = constraint;
      if (st_lookup(table->stTable, (char *)&key, &result)) {
	table->hits += 1.0;
	if (ComplementFlag)
	  return(mdd_not(result));
	else
	  return(mdd_dup(result));
      }
    } else if (table->useConstraint) {
      key.vector = delta;
      key.constraint = constraint;
      if (st_lookup(table->stTable, (char *)&key, &result)) {
	table->hits += 1.0;
	if (SubstituteVector) {
	  newResult = SubstituteCacheResult(info, delta, SubstituteVector,
					    result);
	  return(newResult);
	} else
	  return(mdd_dup(result));
      }
    } else {
      if (st_lookup(table->stTable, (char *)delta, &result)) {
	table->hits += 1.0;
	if (SubstituteVector) {
	  newResult = SubstituteCacheResult(info, delta, SubstituteVector,
					    result);
	  return(newResult);
	}
	return(mdd_dup(result));
      }
    }

    return(NIL(bdd_t));
  }

  slot = VectorHash(table, delta, constraint);

  entry = table->slot[slot];
  while (entry != NIL(ImgCacheEntry_t)) {
    if ((*table->compareFunc)(delta, entry->vector) == 0) {
      table->hits++;
      if (table->preImgFlag) { /* preimage computation */
	ptr1 = (int *)bdd_pointer(constraint);
	ptr2 = (int *)bdd_pointer(entry->constraint);
	if (((unsigned long)ptr1 ^ (unsigned long)ptr2) <= 01) {
	  table->hits++;
	  if (mdd_equal(constraint, entry->constraint))
	    return(mdd_dup(entry->result));
	  else
	    return(mdd_not(entry->result));
	}
      } else if (constraint) { /* image computation */
	if (mdd_equal(constraint, entry->constraint)) {
	  if (SubstituteVector) {
	    newResult = SubstituteCacheResult(info, delta, SubstituteVector,
						entry->result);
	    return(newResult);
	  }
	  return(mdd_dup(entry->result));
	}
      } else if (SubstituteVector) { /* range computation */
	newResult = SubstituteCacheResult(info, delta, SubstituteVector,
					  entry->result);
	return(newResult);
      } else {
	return(mdd_dup(entry->result));
      }
    }
    entry = entry->next;
  }
  return(NIL(bdd_t));
}


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

  Synopsis    [Inserts an entry into cache table.]

  Description [Inserts an entry into cache table.]

  SideEffects []

******************************************************************************/
void
ImgCacheInsertTable(ImgCacheTable_t *table, array_t *delta,
		    bdd_t *constraint, bdd_t *result)
{
  int			slot, num, minSize;
  ImgCacheEntry_t	*entry, *new_, *pos, *minDeltaEntry;

  table->inserts += 1.0;

  if (table->stTable) {
    table->entries += 1.0;
    if (table->preImgFlag || table->useConstraint) {
      ImgCacheStKey_t	*key;

      key = ALLOC(ImgCacheStKey_t, 1);
      key->vector = delta;
      key->constraint = constraint;
      st_insert(table->stTable, (char *)key, (char *)result);
    } else
      st_insert(table->stTable, (char *)delta, (char *)result);
    return;
  }

  slot = VectorHash(table, delta, constraint);

  minSize = 0x7fffffff;
  num = 0;
  pos = table->slot[slot];
  entry = minDeltaEntry = NIL(ImgCacheEntry_t);
  while (pos != NIL(ImgCacheEntry_t)) {
    if (array_n(pos->vector) < minSize) {
      minDeltaEntry = pos;
      minSize = array_n(pos->vector);
    }
    pos = pos->next;
    num++;
  }

  /* num = the number entries in the slot */
  if (num < table->maxChainLength) {
    new_ = ALLOC(ImgCacheEntry_t, 1);
    new_->vector = delta;
    new_->constraint = constraint;
    new_->result = result;
    new_->next = table->slot[slot];
    table->slot[slot] = new_;
    table->entries += 1.0;
  } else if (entry != NIL(ImgCacheEntry_t)) {
    CacheDestroyEntry(entry, FALSE);
    entry->vector = delta;
    entry->constraint = constraint;
    entry->result = result;
  } else { /* all entries are full of latest entries */
    if (0) { /* Rehash */
      unsigned int	i, new_num_slot, new_slot, old_num_slot;
      ImgCacheEntry_t	*next;
      ImgCacheEntry_t	**old_bin;

      old_num_slot = table->nSlots;
      old_bin = table->slot;
      new_num_slot = old_num_slot * 2;
      table->slot = ALLOC(ImgCacheEntry_t *, new_num_slot);
      if (!table->slot) {
	printf("VI_insert_table:new_slots");
	exit(-1);
      }
      memset(table->slot, 0, sizeof(ImgCacheEntry_t *) * new_num_slot);
      table->nSlots = new_num_slot;

      for (i = 0; i < old_num_slot; i++) {
	pos = old_bin[i];
	while (pos != NIL(ImgCacheEntry_t)) {
	  next = pos->next;
	  new_slot = VectorHash(table, pos->vector, pos->constraint);
	  pos->next = table->slot[new_slot];
	  table->slot[new_slot] = pos;
	  pos = next;
	}
      }

      new_slot = VectorHash(table, delta, constraint);
      new_ = ALLOC(ImgCacheEntry_t, 1);
      new_->vector = delta;
      new_->constraint = constraint;
      new_->result = result;
      new_->next = table->slot[slot];
      table->slot[slot] = new_;
      table->entries += 1.0;
    } else {
      CacheDestroyEntry(minDeltaEntry, FALSE);
      minDeltaEntry->vector = delta;
      minDeltaEntry->constraint = constraint;
      minDeltaEntry->result = result;
    }
  }
}


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

  Synopsis    [Flushes all cache entries.]

  Description [Flushes all cache entries.]

  SideEffects []

******************************************************************************/
void
ImgFlushCache(ImgCacheTable_t *table)
{
  unsigned int		i;
  ImgCacheEntry_t	*entry, *next;
  array_t		*vector;
  bdd_t			*result;
  st_generator		*stGen;
  ImgCacheStKey_t	*key;

  if (!table)
    return;

  if (table->stTable) {
    if (table->preImgFlag || table->useConstraint) {
      st_foreach_item(table->stTable, stGen, &key, &result) {
	st_delete(table->stTable, &key, NIL(char *));
	ImgVectorFree(key->vector);
	mdd_free(key->constraint);
	FREE(key);
	mdd_free(result);
      }
    } else {
      st_foreach_item(table->stTable, stGen, &vector, &result) {
	st_delete(table->stTable, &vector, NIL(char *));
	ImgVectorFree(vector);
	mdd_free(result);
      }
    }
  } else {
    for (i = 0; i < table->nSlots; i++) {
      entry = table->slot[i];
      while (entry != NIL(ImgCacheEntry_t)) {
	next = entry->next;
	CacheDestroyEntry(entry, TRUE);
	entry = next;
      }
      table->slot[i] = NIL(ImgCacheEntry_t);
    }
  }
  table->entries = 0.0;
}


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

  Synopsis    [Prints cache statistics for transition function method.]

  Description [Prints cache statistics for transition function method.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
ImgPrintCacheStatistics(ImgCacheTable_t *cache)
{
  if (cache->preImgFlag)
    fprintf(vis_stdout, "** cache statistics (preImg) **\n");
  else
    fprintf(vis_stdout, "** cache statistics (img) **\n");
  fprintf(vis_stdout, "# insertions = %g\n", cache->inserts);
  if (cache->inserts != 0.0) {
    fprintf(vis_stdout, "# lookups = %g\n", cache->lookups);
    fprintf(vis_stdout, "# hits = %g (%.2f%%)\n", cache->hits,
	cache->hits / cache->lookups * 100.0);
    fprintf(vis_stdout, "# misses = %g (%.2f%%)\n",
	cache->lookups - cache->hits,
	(cache->lookups - cache->hits) / cache->lookups * 100.0);
    fprintf(vis_stdout, "# entries = %g\n", cache->entries);
    if (!cache->stTable) {
      fprintf(vis_stdout, "# slots = %d\n", cache->nSlots);
      fprintf(vis_stdout, "maxChainLength = %d\n", cache->maxChainLength);
    }
  }
}


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


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

  Synopsis    [Destroys a cache entry.]

  Description [Destroys a cache entry.]

  SideEffects []

******************************************************************************/
static void
CacheDestroyEntry(ImgCacheEntry_t *entry, boolean freeEntry)
{
  ImgVectorFree(entry->vector);
  mdd_free(entry->result);
  if (entry->constraint)
    mdd_free(entry->constraint);
  if (freeEntry)
    FREE(entry);
}


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

  Synopsis    [Returns hash value of a vector.]

  Description [Returns hash value of a vector.]

  SideEffects []

******************************************************************************/
static int
VectorHash(ImgCacheTable_t *table, array_t *delta, bdd_t *constraint)
{
  unsigned long		value;
  ImgComponent_t	*comp;
  bdd_t			*func;
  int			i;

  value = array_n(delta);
  if (constraint)
    value += (unsigned long)bdd_pointer(constraint) & ~01;
  for (i = 0; i < array_n(delta); i++) {
    comp = array_fetch(ImgComponent_t *, delta, i);
    func = comp->func;
    value += (unsigned long)bdd_pointer(func) & ~01;
  }
  return((int)(value % table->nSlots));
}


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

  Synopsis    [Returns hash value of a vector for st_table.]

  Description [Returns hash value of a vector for st_table.]

  SideEffects []

******************************************************************************/
static int
VectorStHash(char *key, int modulus)
{
  unsigned long		value;
  array_t		*delta;
  ImgComponent_t	*comp;
  bdd_t			*func;
  int			i;

  delta = (array_t *)key;
  value = array_n(delta);

  for (i = 0; i < array_n(delta); i++) {
    comp = array_fetch(ImgComponent_t *, delta, i);
    func = comp->func;
    value += (unsigned long)bdd_pointer(func) & ~01;
  }
  return((int)(value % modulus));
}


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

  Synopsis    [Returns hash value of a key for st_table.]

  Description [Returns hash value of a key for st_table.]

  SideEffects []

******************************************************************************/
static int
KeyStHash(char *key, int modulus)
{
  ImgCacheStKey_t	*stKey;
  unsigned long		value;
  array_t		*delta;
  ImgComponent_t	*comp;
  bdd_t			*func;
  int			i;

  stKey = (ImgCacheStKey_t *)key;
  delta = stKey->vector;
  value = array_n(delta);
  if (stKey->constraint)
    value += (unsigned long)bdd_pointer(stKey->constraint) & ~01;

  for (i = 0; i < array_n(delta); i++) {
    comp = array_fetch(ImgComponent_t *, delta, i);
    func = comp->func;
    value += (unsigned long)bdd_pointer(func) & ~01;
  }
  return((int)(value % modulus));
}


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

  Synopsis    [Compares two vectors.]

  Description [Compares two vectors.]

  SideEffects []

******************************************************************************/
static int
VectorCompare(array_t *vector1, array_t *vector2)
{
  ImgComponent_t	*comp1, *comp2;
  int			i, index1, index2;

  if (array_n(vector1) != array_n(vector2))
    return(1);

  for (i = 0; i < array_n(vector1); i++) {
    comp1 = array_fetch(ImgComponent_t *, vector1, i);
    comp2 = array_fetch(ImgComponent_t *, vector2, i);
    index1 = (int)bdd_top_var_id(comp1->var);
    index2 = (int)bdd_top_var_id(comp2->var);
    if (index1 != index2)
      return(1);
    if (!mdd_equal(comp1->func, comp2->func))
      return(1);
  }
  SubstituteVector = NIL(array_t);
  return(0);
}


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

  Synopsis    [Compares two vectors considering substitution.]

  Description [Compares two vectors considering substitution.]

  SideEffects []

******************************************************************************/
static int
VectorSortCompare(array_t *vector1, array_t *vector2)
{
  ImgComponent_t	*comp1, *comp2;
  int			i, index1, index2;
  int			*ptr1, *ptr2, *regularPtr1, *regularPtr2;

  if (array_n(vector1) != array_n(vector2))
    return(1);

  SubstituteVector = NIL(array_t);
  for (i = 0; i < array_n(vector1); i++) {
    comp1 = array_fetch(ImgComponent_t *, vector1, i);
    comp2 = array_fetch(ImgComponent_t *, vector2, i);
    index1 = (int)bdd_top_var_id(comp1->var);
    index2 = (int)bdd_top_var_id(comp2->var);
    if (index1 != index2)
      SubstituteVector = vector2;
    ptr1 = (int *)bdd_pointer(comp1->func);
    ptr2 = (int *)bdd_pointer(comp2->func);
    regularPtr1 = (int *)((unsigned long)ptr1 & ~01);
    regularPtr2 = (int *)((unsigned long)ptr2 & ~01);
    if (regularPtr1 == regularPtr2) {
      if (ptr1 != ptr2) {
	if (comp1->intermediate || comp2->intermediate)
	  return(1);
	SubstituteVector = vector2;
      }
    } else
      return(1);
  }
  return(0);
}


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

  Synopsis    [Compares two vectors considering substitution.]

  Description [Compares two vectors considering substitution.]

  SideEffects []

******************************************************************************/
static int
VectorSortCompareWithConstraint(array_t *vector1, array_t *vector2)
{
  ImgComponent_t	*comp1, *comp2;
  int			i, index1, index2;

  if (array_n(vector1) != array_n(vector2))
    return(1);

  SubstituteVector = NIL(array_t);
  for (i = 0; i < array_n(vector1); i++) {
    comp1 = array_fetch(ImgComponent_t *, vector1, i);
    comp2 = array_fetch(ImgComponent_t *, vector2, i);
    index1 = (int)bdd_top_var_id(comp1->var);
    index2 = (int)bdd_top_var_id(comp2->var);
    if (index1 != index2)
      SubstituteVector = vector2;
    if (!mdd_equal(comp1->func, comp2->func))
      return(1);
  }
  return(0);
}


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

  Synopsis    [Compares two keys.]

  Description [Compares two keys.]

  SideEffects []

******************************************************************************/
static int
ImageKeyCompare(ImgCacheStKey_t *key1, ImgCacheStKey_t *key2)
{
  ComplementFlag = 0;
  if (mdd_equal(key1->constraint, key2->constraint)) {
    if (VectorCompare(key1->vector, key2->vector))
      return(1);
  } else
    return(1);
  return(0);
}


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

  Synopsis    [Compares two keys considering substitution.]

  Description [Compares two keys considering substitution.]

  SideEffects []

******************************************************************************/
static int
ImageKeySortCompare(ImgCacheStKey_t *key1, ImgCacheStKey_t *key2)
{
  ComplementFlag = 0;
  if (mdd_equal(key1->constraint, key2->constraint)) {
    if (VectorSortCompareWithConstraint(key1->vector, key2->vector))
      return(1);
  } else
    return(1);
  return(0);
}


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

  Synopsis    [Compares two keys for preimage.]

  Description [Compares two keys for preimage.]

  SideEffects []

******************************************************************************/
static int
PreImageKeyCompare(ImgCacheStKey_t *key1, ImgCacheStKey_t *key2)
{
  unsigned long	ptr1, ptr2;

  ptr1 = (unsigned long)bdd_pointer(key1->constraint);
  ptr2 = (unsigned long)bdd_pointer(key2->constraint);
  if ((ComplementFlag = (int) (ptr1 ^ ptr2)) <= 01) {
    if (VectorCompare(key1->vector, key2->vector))
      return(1);
  } else
    return(1);
  return(0);
}


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

  Synopsis    [Substitutes a cache result.]

  Description [Substitutes a cache result.]

  SideEffects []

******************************************************************************/
static mdd_t *
SubstituteCacheResult(ImgTfmInfo_t *info, array_t *keyVector,
		      array_t *cacheVector,
			mdd_t *result)
{
  mdd_t			*newResult;
  ImgComponent_t	*comp1, *comp2;
  int			*ptr1, *ptr2;
  int			i, id1, id2;
  mdd_t			*var, *func;
  array_t		*varArray, *funcArray;

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

  for (i = 0; i < array_n(keyVector); i++) {
    comp1 = array_fetch(ImgComponent_t *, keyVector, i);
    comp2 = array_fetch(ImgComponent_t *, cacheVector, i);
    ptr1 = (int *)bdd_pointer(comp1->func);
    ptr2 = (int *)bdd_pointer(comp2->func);
    id1 = (int)bdd_top_var_id(comp1->var);
    id2 = (int)bdd_top_var_id(comp2->var);
    if (id1 == id2) {
      if (ptr1 != ptr2) {
	array_insert_last(mdd_t *, varArray, comp2->var);
	func = mdd_not(comp1->var);
	array_insert_last(mdd_t *, funcArray, func);
      }
    } else {
      if (ptr1 == ptr2) {
	array_insert_last(mdd_t *, varArray, comp2->var);
	func = mdd_dup(comp1->var);
	array_insert_last(mdd_t *, funcArray, func);
      } else {
	array_insert_last(mdd_t *, varArray, comp2->var);
	func = mdd_not(comp1->var);
	array_insert_last(mdd_t *, funcArray, func);
      }
    }
  }
  if (array_n(varArray) == 1) {
    var = array_fetch(mdd_t *, varArray, 0);
    func = array_fetch(mdd_t *, funcArray, 0);
    newResult = bdd_compose(result, var, func);
  } else if (bdd_get_package_name() == CUDD)
    newResult = bdd_vector_compose(result, varArray, funcArray);
  else
    newResult = SubstituteCacheResultRecur(result, varArray, funcArray, 0);
  array_free(varArray);
  mdd_array_free(funcArray);
  return(newResult);
}


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

  Synopsis    [Recursive procedure of SubstituteCacheResult.]

  Description [Recursive procedure of SubstituteCacheResult.]

  SideEffects []

******************************************************************************/
static mdd_t *
SubstituteCacheResultRecur(mdd_t *result, array_t *varArray, array_t *funcArray,
			   int pos)
{
  mdd_t	*var, *varNot, *func;
  mdd_t	*resultT, *resultE, *newResultT, *newResultE, *newResult;

  if (pos > array_n(varArray))
    return(mdd_dup(result));

  var = array_fetch(mdd_t *, varArray, pos);
  func = array_fetch(mdd_t *, funcArray, pos);
  varNot = mdd_not(var);
  resultT = bdd_cofactor(result, var);
  resultE = bdd_cofactor(result, varNot);
  mdd_free(varNot);
  newResultT = SubstituteCacheResultRecur(resultT, varArray, funcArray,
					  pos + 1);
  mdd_free(resultT);
  newResultE = SubstituteCacheResultRecur(resultE, varArray, funcArray,
					  pos + 1);
  mdd_free(resultE);
  newResult = bdd_ite(func, newResultT, newResultE, 1, 1, 1);
  mdd_free(newResultT);
  mdd_free(newResultE);
  return(newResult);
}