src/img/imgTfmCache.c

Go to the documentation of this file.

#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                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* 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);

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


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);
}


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


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);
}


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                                          */
/*---------------------------------------------------------------------------*/


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;
    }
  }
}


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);
}


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));
}


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;
    }
  }
}


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;
}


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                                            */
/*---------------------------------------------------------------------------*/


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);
}


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));
}


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));
}


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));
}


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);
}


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);
}


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);
}


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);
}


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);
}


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);
}


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);
}


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);
}