src/img/imgTfmUtil.c

Go to the documentation of this file.

#include "imgInt.h"

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

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

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

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

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

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

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

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

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

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


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


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

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

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

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

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

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

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

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

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

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

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

  *newVector = vector1;
  *cube = old;
}


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

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

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

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

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

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

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

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

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

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

  return(newFrom);
}


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

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


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

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

  return(size);
}


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

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

  return(size);
}


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

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


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

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


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

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


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


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

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


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


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


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

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


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

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


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

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

  constrainedRelationArray = ImgGetCofactoredRelationArray(relationArray,
                                                           constraint);

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

  return(constrainedRelationArray);
}


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

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

  cofactoredRelationArray = array_alloc(mdd_t *, 0);

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

  return(cofactoredRelationArray);
}


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

  if (bdd_is_tautology(func, 1))
    return;

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


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

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

  abstractedRelationArray = array_alloc(mdd_t *, 0);

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

  return(abstractedRelationArray);
}


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

  if (bdd_is_tautology(cube, 1))
    return;

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


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

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

  return(newRelationArray);
}


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

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

  return(newRelationArray);
}


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

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

  constrainedVector = ImgGetCofactoredVector(info, vector, constraint);

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

  return(constrainedVector);
}


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

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

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

  return(cofactoredVector);
}


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

  if (bdd_is_tautology(func, 1))
    return;

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


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

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

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

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

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

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

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

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


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

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


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

  assert(ImgVectorFunctionSize(vector) == 1);

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

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

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

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


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

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


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

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

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

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

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

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

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

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

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

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

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

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

  return(cofactoredVector);
}


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

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


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


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


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

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

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

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

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

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

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


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

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

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

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

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


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

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

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

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

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

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


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


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


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

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

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

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