VIS

src/img/imgTfm.c File Reference

#include "imgInt.h"
Include dependency graph for imgTfm.c:

Go to the source code of this file.

Functions

static ImgTfmInfo_t * TfmInfoStructAlloc (Img_MethodType method)
static int CompareIndex (const void *e1, const void *e2)
static int HookInfoFunction (bdd_manager *mgr, char *str, void *method)
static array_t * ChoosePartialVars (ImgTfmInfo_t *info, array_t *vector, int nPartialVars, int partialMethod)
static void PrintRecursionStatistics (ImgTfmInfo_t *info, int preFlag)
static void PrintFoundVariableStatistics (ImgTfmInfo_t *info, int preFlag)
static void GetRecursionStatistics (ImgTfmInfo_t *info, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp)
static int ReadSetIntValue (char *string, int l, int u, int defaultValue)
static boolean ReadSetBooleanValue (char *string, boolean defaultValue)
static void FindIntermediateVarsRecursively (ImgTfmInfo_t *info, mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *vector, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray)
static void GetIntermediateRelationsRecursively (mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *relationArray, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray)
static int CheckNondeterminism (Ntk_Network_t *network)
static array_t * TfmCreateBitVector (ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars)
static array_t * TfmCreateBitRelationArray (ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars)
static void TfmSetupPartialTransitionRelation (ImgTfmInfo_t *info, array_t **partialRelationArray)
static void TfmBuildRelationArray (ImgTfmInfo_t *info, ImgFunctionData_t *functionData, array_t *bitRelationArray, Img_DirectionType directionType, int writeMatrix)
static void RebuildTransitionRelation (ImgTfmInfo_t *info, Img_DirectionType directionType)
static void MinimizeTransitionFunction (array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus)
static void AddDontCareToTransitionFunction (array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus)
int Img_TfmGetRecursionStatistics (Img_ImageInfo_t *imageInfo, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp)
void Img_TfmPrintStatistics (Img_ImageInfo_t *imageInfo, Img_DirectionType dir)
void Img_TfmPrintRecursionStatistics (Img_ImageInfo_t *imageInfo, int preFlag)
void Img_PrintTfmOptions (void)
void * ImgImageInfoInitializeTfm (void *methodData, ImgFunctionData_t *functionData, Img_DirectionType directionType, Img_MethodType method)
mdd_t * ImgImageInfoComputeFwdTfm (ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray)
mdd_t * ImgImageInfoComputeFwdWithDomainVarsTfm (ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray)
mdd_t * ImgImageInfoComputeBwdTfm (ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray)
mdd_t * ImgImageInfoComputeBwdWithDomainVarsTfm (ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray)
void ImgImageInfoFreeTfm (void *methodData)
void ImgImageInfoPrintMethodParamsTfm (void *methodData, FILE *fp)
void ImgRestoreTransitionFunction (Img_ImageInfo_t *imageInfo, Img_DirectionType directionType)
void ImgDuplicateTransitionFunction (Img_ImageInfo_t *imageInfo, Img_DirectionType directionType)
void ImgMinimizeTransitionFunction (void *methodData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, int printStatus)
void ImgAddDontCareToTransitionFunction (void *methodData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, int printStatus)
void ImgAbstractTransitionFunction (Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType, int printStatus)
int ImgApproximateTransitionFunction (mdd_manager *mgr, void *methodData, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, Img_DirectionType directionType, mdd_t *bias)
array_t * ImgGetTransitionFunction (void *methodData, Img_DirectionType directionType)
void ImgUpdateTransitionFunction (void *methodData, array_t *vector, Img_DirectionType directionType)
void ImgReplaceIthTransitionFunction (void *methodData, int i, mdd_t *function, Img_DirectionType directionType)
ImgTfmOption_t * ImgTfmGetOptions (Img_MethodType method)
void ImgImageFreeClusteredTransitionRelationTfm (void *methodData, Img_DirectionType directionType)
void ImgImageConstrainAndClusterTransitionRelationTfm (Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus)
int ImgIsPartitionedTransitionRelationTfm (Img_ImageInfo_t *imageInfo)

Variables

static char rcsid[] UNUSED = "$Id: imgTfm.c,v 1.93 2005/04/23 14:30:54 jinh Exp $"
static st_table * HookInfoList
static int nHookInfoList

Function Documentation

static void AddDontCareToTransitionFunction ( array_t *  vector,
array_t *  relationArray,
mdd_t *  constrain,
Img_MinimizeType  minimizeMethod,
int  printStatus 
) [static]

Function********************************************************************

Synopsis [Adds dont cares to function vector or relation.]

Description [Adds dont cares to function vector or relation.]

SideEffects []

Definition at line 3684 of file imgTfm.c.

{
  int                   i;
  bdd_t                 *relation, *simplifiedRelation, *simplifiedFunc;
  long                  sizeConstrain = 0, size = 0;
  ImgComponent_t        *comp;

  if (bdd_is_tautology(constrain, 1))
    return;

  if (vector) {
    if (printStatus) {
      size = ImgVectorBddSize(vector);
      sizeConstrain = bdd_size(constrain);
    }

    arrayForEachItem(ImgComponent_t *, vector, i, comp) {
      simplifiedFunc = Img_AddDontCareToImage(comp->func, constrain,
                                              minimizeMethod);
      if (printStatus == 2) {
        (void)fprintf(vis_stdout,
            "IMG Info: minimized function %d | %ld => %d in component %d\n",
                      bdd_size(comp->func), sizeConstrain,
                      bdd_size(simplifiedFunc), i);
      }
      mdd_free(comp->func);
      comp->func = simplifiedFunc;
    }

    if (printStatus) {
      (void) fprintf(vis_stdout,
       "IMG Info: minimized function [%ld | %ld => %ld] with %d components\n",
                     size, sizeConstrain,
                     ImgVectorBddSize(vector), array_n(vector));
    }
  }

  if (relationArray) {
    if (printStatus) {
      size = bdd_size_multiple(relationArray);
      sizeConstrain = bdd_size(constrain);
    }

    arrayForEachItem(bdd_t*, relationArray, i, relation) {
      simplifiedRelation = Img_AddDontCareToImage(relation, constrain,
                                                  minimizeMethod);
      if (printStatus == 2) {
        (void)fprintf(vis_stdout,
                "IMG Info: minimized relation %d | %ld => %d in component %d\n",
                      bdd_size(relation), sizeConstrain,
                      bdd_size(simplifiedRelation), i);
      }
      mdd_free(relation);
      array_insert(bdd_t *, relationArray, i, simplifiedRelation);
    }

    if (printStatus) {
      (void) fprintf(vis_stdout,
       "IMG Info: minimized relation [%ld | %ld => %ld] with %d components\n",
                     size, sizeConstrain,
                     bdd_size_multiple(relationArray), array_n(relationArray));
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

static int CheckNondeterminism ( Ntk_Network_t *  network) [static]

Function********************************************************************

Synopsis [Checks whether the network is nondeterministic.]

Description [Checks whether the network is nondeterministic. However, current implementatin is just checking whether the network has multi-valued variables.]

SideEffects []

SeeAlso []

Definition at line 2845 of file imgTfm.c.

{
  Ntk_Node_t            *node;
  lsGen                 gen;
  Var_Variable_t        *var;
  int                   numValues;

  Ntk_NetworkForEachNode(network, gen, node) {
    var = Ntk_NodeReadVariable(node);
    numValues = Var_VariableReadNumValues(var);
    if (numValues > 2) {
      lsFinish(gen);
      return 1;
    }
  }
  return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

static array_t * ChoosePartialVars ( ImgTfmInfo_t *  info,
array_t *  vector,
int  nPartialVars,
int  partialMethod 
) [static]

Function********************************************************************

Synopsis [Chooses variables for static splitting.]

Description [Chooses variables for static splitting. partialMethod is set by hybrid_partial_method. Refer to print_hybrid_options command.]

SideEffects []

Definition at line 2410 of file imgTfm.c.

{
  int                   i, j, nVars;
  ImgComponent_t        *comp;
  char                  *support;
  int                   *varCost;
  int                   big, small, nChosen, insert, id;
  mdd_t                 *var;
  int                   *partialVars = ALLOC(int, nPartialVars);
  array_t               *partialBddVars = array_alloc(mdd_t *, 0);

  nVars = info->nVars;
  varCost = ALLOC(int, nVars);
  memset(varCost, 0, sizeof(int) * nVars);

  if (partialMethod == 0) {
    /* chooses the variable whose function has the largest bdd size */
    for (i = 0; i < array_n(vector); i++) {
      comp = array_fetch(ImgComponent_t *, vector, i);
      id = (int)bdd_top_var_id(comp->var);
      varCost[id] = bdd_size(comp->func);
    }
  } else {
    /* chooses the variable that appears the most frequently */
    for (i = 0; i < array_n(vector); i++) {
      comp = array_fetch(ImgComponent_t *, vector, i);
      support = comp->support;
      for (j = 0; j < nVars; j++) {
        if (support[j])
          varCost[j]++;
      }
    }
  }

  nChosen = 0;
  big = small = -1;
  for (i = 0; i < nVars; i++) {
    if (varCost[i] == 0)
      continue;
    if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
      continue;
    if (info->intermediateVarsTable &&
        st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) {
      continue;
    }
    if (nChosen == 0) {
      partialVars[0] = i;
      nChosen = 1;
      big = small = varCost[i];
    } else if (varCost[i] < small) {
      if (nChosen < nPartialVars) {
        partialVars[nChosen] = i;
        nChosen++;
        small = varCost[i];
      } else
        continue;
    } else if (varCost[i] > big) {
      if (nChosen < nPartialVars) {
        for (j = nChosen; j > 0; j--)
          partialVars[j] = partialVars[j - 1];
        partialVars[0] = i;
        nChosen++;
        big = varCost[i];
      } else {
        for (j = nPartialVars - 1; j > 0; j--)
          partialVars[j] = partialVars[j - 1];
        partialVars[0] = i;
        big = varCost[i];
        small = varCost[partialVars[nPartialVars - 1]];
      }
    } else {
      insert = nChosen;
      for (j = 0; j < nChosen; j++) {
        if (varCost[i] > varCost[partialVars[j]]) {
          insert = j;
          break;
        }
      }
      if (nChosen < nPartialVars) {
        for (j = nChosen; j > insert; j--)
          partialVars[j] = partialVars[j - 1];
        partialVars[insert] = i;
        nChosen++;
      } else if (insert < nChosen) {
        for (j = nPartialVars - 1; j > insert; j--)
          partialVars[j] = partialVars[j - 1];
        partialVars[insert] = i;
        small = varCost[partialVars[nPartialVars - 1]];
      }
    }
  }
  FREE(varCost);

  for (i = 0; i < nChosen; i++) {
    var = bdd_var_with_index(info->manager, partialVars[i]);
    array_insert_last(mdd_t *, partialBddVars, var);
  }

  FREE(partialVars);
  return(partialBddVars);
}

Here is the caller graph for this function:

static int CompareIndex ( const void *  e1,
const void *  e2 
) [static]

Function********************************************************************

Synopsis [Compares two variable indices of components.]

Description [Compares two variable indices of components.]

SideEffects []

Definition at line 2352 of file imgTfm.c.

{
  ImgComponent_t        *c1, *c2;
  int                   id1, id2;

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

  id1 = (int)bdd_top_var_id(c1->var);
  id2 = (int)bdd_top_var_id(c2->var);

  if (id1 > id2)
    return(1);
  else if (id1 < id2)
    return(-1);
  else
    return(0);
}

Here is the caller graph for this function:

static void FindIntermediateVarsRecursively ( ImgTfmInfo_t *  info,
mdd_manager *  mddManager,
vertex_t *  vertex,
int  mddId,
st_table *  vertexTable,
array_t *  vector,
st_table *  domainQuantifyVarMddIdTable,
array_t *  intermediateVarMddIdArray 
) [static]

Function********************************************************************

Synopsis [Traverses the partition recursively, creating the functions for the intermediate vertices.]

Description [Traverses the partition recursively, creating the functions for the intermediate vertices. This function is originated from PartitionTraverseRecursively in imgIwls95.c]

SideEffects []

Definition at line 2719 of file imgTfm.c.

{
  Mvf_Function_t        *mvf;
  lsList                faninEdges;
  lsGen                 gen;
  vertex_t              *faninVertex;
  edge_t                *faninEdge;
  array_t               *varBddFunctionArray, *bddArray;
  int                   i;
  mdd_t                 *var, *func;
  ImgComponent_t        *comp;

  if (st_is_member(vertexTable, (char *)vertex))
    return;
  st_insert(vertexTable, (char *)vertex, NIL(char));
  if (mddId != -1) { /* This is not the next state function node */
    /* There is an mdd variable associated with this vertex */
    array_insert_last(int, intermediateVarMddIdArray, mddId);
    mvf = Part_VertexReadFunction(vertex);
    varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager, mddId, mvf);
    bddArray = mdd_id_to_bdd_array(mddManager, mddId);
    assert(array_n(varBddFunctionArray) == array_n(bddArray));
    for (i = 0; i < array_n(bddArray); i++) {
      var = array_fetch(mdd_t *, bddArray, i);
      func = array_fetch(mdd_t *, varBddFunctionArray, i);
      comp = ImgComponentAlloc(info);
      comp->var = var;
      comp->func = func;
      comp->intermediate = 1;
      ImgComponentGetSupport(comp);
      array_insert_last(ImgComponent_t *, vector, comp);
    }
    array_free(varBddFunctionArray);
    array_free(bddArray);
  }
  faninEdges = g_get_in_edges(vertex);
  if (lsLength(faninEdges) == 0)
    return;
  lsForEachItem(faninEdges, gen, faninEdge) {
    faninVertex = g_e_source(faninEdge);
    mddId = Part_VertexReadMddId(faninVertex);
    if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) {
      /* This is either domain var or quantify var */
      continue;
    }
    FindIntermediateVarsRecursively(info, mddManager, faninVertex, mddId,
                                    vertexTable, vector,
                                    domainQuantifyVarMddIdTable,
                                    intermediateVarMddIdArray);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void GetIntermediateRelationsRecursively ( mdd_manager *  mddManager,
vertex_t *  vertex,
int  mddId,
st_table *  vertexTable,
array_t *  relationArray,
st_table *  domainQuantifyVarMddIdTable,
array_t *  intermediateVarMddIdArray 
) [static]

Function********************************************************************

Synopsis [Traverses the partition recursively, creating the relations for the intermediate vertices.]

Description [Traverses the partition recursively, creating the relations for the intermediate vertices. This function is a copy of PartitionTraverseRecursively from imgIwls95.c.]

SideEffects []

Definition at line 2789 of file imgTfm.c.

{
  Mvf_Function_t        *mvf;
  lsList                faninEdges;
  lsGen                 gen;
  vertex_t              *faninVertex;
  edge_t                *faninEdge;
  array_t               *varBddRelationArray;

  if (st_is_member(vertexTable, (char *)vertex))
    return;
  st_insert(vertexTable, (char *)vertex, NIL(char));
  if (mddId != -1) { /* This is not the next state function node */
    /* There is an mdd variable associated with this vertex */
    array_insert_last(int, intermediateVarMddIdArray, mddId);
    mvf = Part_VertexReadFunction(vertex);
    varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf);
    array_append(relationArray, varBddRelationArray);
    array_free(varBddRelationArray);
  }
  faninEdges = g_get_in_edges(vertex);
  if (lsLength(faninEdges) == 0)
    return;
  lsForEachItem(faninEdges, gen, faninEdge) {
    faninVertex = g_e_source(faninEdge);
    mddId = Part_VertexReadMddId(faninVertex);
    if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) {
      /* This is either domain var or quantify var */
      continue;
    }
    GetIntermediateRelationsRecursively(mddManager, faninVertex, mddId,
                                        vertexTable, relationArray,
                                        domainQuantifyVarMddIdTable,
                                        intermediateVarMddIdArray);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void GetRecursionStatistics ( ImgTfmInfo_t *  info,
int  preFlag,
int *  nRecurs,
int *  nLeaves,
int *  nTurns,
float *  averageDepth,
int *  maxDepth,
int *  nDecomps,
int *  topDecomp,
int *  maxDecomp,
float *  averageDecomp 
) [static]

Function********************************************************************

Synopsis [Returns the statistics of recursions of transition function method.]

Description [Returns the statistics of recursions of transition function method.]

SideEffects []

SeeAlso []

Definition at line 2609 of file imgTfm.c.

{
  if (preFlag) {
    *nRecurs = info->nRecursionB;
    *nLeaves = info->nLeavesB;
    *nTurns = info->nTurnsB;
    *averageDepth = info->averageDepthB;
    *maxDepth = info->maxDepthB;
    *nDecomps = 0;
    *topDecomp = 0;
    *maxDecomp = 0;
    *averageDecomp = 0.0;
  } else {
    *nRecurs = info->nRecursion;
    *nLeaves = info->nLeaves;
    *nTurns = info->nTurns;
    *averageDepth = info->averageDepth;
    *maxDepth = info->maxDepth;
    *nDecomps = info->nDecomps;
    *topDecomp = info->topDecomp;
    *maxDecomp = info->maxDecomp;
    *averageDecomp = info->averageDecomp;
  }
}

Here is the caller graph for this function:

static int HookInfoFunction ( bdd_manager *  mgr,
char *  str,
void *  method 
) [static]

Function********************************************************************

Synopsis [Flushes cache entries in a list.]

Description [Flushes cache entries in a list.]

SideEffects []

Definition at line 2382 of file imgTfm.c.

{
  ImgTfmInfo_t  *info;
  st_generator  *stGen;

  if (HookInfoList) {
    st_foreach_item(HookInfoList, stGen, &info, NULL) {
      if (info->imgCache)
        ImgFlushCache(info->imgCache);
      if (info->preCache)
        ImgFlushCache(info->preCache);
    }
  }
  return(0);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Img_PrintTfmOptions ( void  )

Function********************************************************************

Synopsis [Prints the options for image computation using transition function method.]

Description [Prints the options for image computation using transition function method.]

SideEffects []

SeeAlso []

Definition at line 272 of file imgTfm.c.

{
  ImgTfmOption_t        *options;
  Img_MethodType        method;
  char                  *flagValue, dummy[40];

  flagValue = Cmd_FlagReadByName("image_method");
  if (flagValue) {
    if (strcmp(flagValue, "hybrid") == 0)
      method = Img_Hybrid_c;
    else
      method = Img_Tfm_c;
  } else
    method = Img_Tfm_c;

  options = ImgTfmGetOptions(method);

  switch (options->splitMethod) {
  case 0 :
    sprintf(dummy, "input split");
    break;
  case 1 :
    sprintf(dummy, "output split");
    break;
  case 2 :
    sprintf(dummy, "mixed");
    break;
  case 3 :
    sprintf(dummy, "hybrid");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_split_method = %d (%s)\n",
          options->splitMethod, dummy);

  switch (options->inputSplit) {
  case 0 :
    sprintf(dummy, "support before splitting");
    break;
  case 1 :
    sprintf(dummy, "support after splitting");
    break;
  case 2 :
    sprintf(dummy, "estimate BDD size after splitting");
    break;
  case 3 :
    sprintf(dummy, "top variable");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_input_split = %d (%s)\n",
          options->inputSplit, dummy);

  if (options->piSplitFlag)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_pi_split_flag = %s\n", dummy);

  /* whether to convert image computation to range computation */
  switch (options->rangeComp) {
  case 0 :
    sprintf(dummy, "do not convert");
    break;
  case 1 :
    sprintf(dummy, "convert to range computation");
    break;
  case 2 :
    sprintf(dummy, "convert with threshold");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_range_comp = %d (%s)\n",
          options->rangeComp, dummy);

  fprintf(vis_stdout, "TFM: tfm_range_threshold = %d\n",
          options->rangeThreshold);

  fprintf(vis_stdout, "TFM: tfm_range_try_threshold = %d\n",
          options->rangeTryThreshold);

  if (options->rangeCheckReorder)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_range_check_reorder = %s\n", dummy);

  switch (options->tieBreakMode) {
  case 0 :
    sprintf(dummy, "closest variable to top");
    break;
  case 1 :
    sprintf(dummy, "smallest BDD size after splitting");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_tie_break_mode = %d (%s)\n",
          options->tieBreakMode, dummy);

  switch (options->outputSplit) {
  case 0 :
    sprintf(dummy, "smallest BDD size");
    break;
  case 1 :
    sprintf(dummy, "largest BDD size");
    break;
  case 2 :
    sprintf(dummy, "top variable");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_output_split = %d (%s)\n",
          options->outputSplit, dummy);

  fprintf(vis_stdout, "TFM: tfm_turn_depth = %d\n",
          options->turnDepth);

  if (options->findDecompVar)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_find_decomp_var = %s\n", dummy);

  if (options->sortVectorFlag)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_sort_vector_flag = %s\n", dummy);

  if (options->printStatistics)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_print_stats = %s\n", dummy);

  if (options->printBddSize)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_print_bdd_size = %s\n", dummy);

  if (options->splitCubeFunc)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_split_cube_func = %s\n", dummy);

  switch (options->findEssential) {
  case 0 :
    sprintf(dummy, "off");
    break;
  case 1 :
    sprintf(dummy, "on");
    break;
  case 2 :
    sprintf(dummy, "dynamic");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_find_essential = %d (%s)\n",
          options->findEssential, dummy);

  switch (options->printEssential) {
  case 0 :
    sprintf(dummy, "off");
    break;
  case 1 :
    sprintf(dummy, "at the end");
    break;
  case 2 :
    sprintf(dummy, "at every image computation");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_print_essential = %d (%s)\n",
          options->printEssential, dummy);

  switch (options->useCache) {
  case 0 :
    sprintf(dummy, "off");
    break;
  case 1 :
    sprintf(dummy, "on");
    break;
  case 2 :
    sprintf(dummy, "store all intermediate");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_use_cache = %d (%s)\n",
          options->useCache, dummy);

  if (options->globalCache)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_global_cache = %s\n", dummy);

  fprintf(vis_stdout, "TFM: tfm_max_chain_length = %d\n",
          options->maxChainLength);

  fprintf(vis_stdout, "TFM: tfm_init_cache_size = %d\n",
          options->initCacheSize);

  switch (options->autoFlushCache) {
  case 0 :
    sprintf(dummy, "when requested");
    break;
  case 1 :
    sprintf(dummy, "at the end of image computation");
    break;
  case 2 :
    sprintf(dummy, "before reordering");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_auto_flush_cache = %d (%s)\n",
          options->autoFlushCache, dummy);

  if (options->composeIntermediateVars)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_compose_intermediate_vars = %s\n", dummy);

  switch (options->preSplitMethod) {
  case 0 :
    sprintf(dummy, "input split");
    break;
  case 1 :
    sprintf(dummy, "output split");
    break;
  case 2 :
    sprintf(dummy, "mixed");
    break;
  case 3 :
    sprintf(dummy, "substitution");
    break;
  case 4 :
    sprintf(dummy, "hybrid");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_pre_split_method = %d (%s)\n",
          options->preSplitMethod, dummy);

  switch (options->preInputSplit) {
  case 0 :
    sprintf(dummy, "support before splitting");
    break;
  case 1 :
    sprintf(dummy, "support after splitting");
    break;
  case 2 :
    sprintf(dummy, "estimate BDD size after splitting");
    break;
  case 3 :
    sprintf(dummy, "top variable");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_pre_input_split = %d (%s)\n",
          options->preInputSplit, dummy);

  switch (options->preOutputSplit) {
  case 0 :
    sprintf(dummy, "smallest BDD size");
    break;
  case 1 :
    sprintf(dummy, "largest BDD size");
    break;
  case 2 :
    sprintf(dummy, "top variable");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_pre_output_split = %d (%s)\n",
          options->preOutputSplit, dummy);

  switch (options->preDcLeafMethod) {
  case 0 :
    sprintf(dummy, "substitution");
    break;
  case 1 :
    sprintf(dummy, "constraint cofactoring");
    break;
  case 2 :
    sprintf(dummy, "hybrid");
    break;
  default :
    sprintf(dummy, "invalid");
    break;
  }
  fprintf(vis_stdout, "TFM: tfm_pre_dc_leaf_method = %d (%s)\n",
          options->preDcLeafMethod, dummy);

  if (options->preMinimize)
    sprintf(dummy, "yes");
  else
    sprintf(dummy, "no");
  fprintf(vis_stdout, "TFM: tfm_pre_minimize = %s\n", dummy);

  fprintf(vis_stdout, "TFM: tfm_verbosity = %d\n",
          options->verbosity);

  FREE(options);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int Img_TfmGetRecursionStatistics ( Img_ImageInfo_t *  imageInfo,
int  preFlag,
int *  nRecurs,
int *  nLeaves,
int *  nTurns,
float *  averageDepth,
int *  maxDepth,
int *  nDecomps,
int *  topDecomp,
int *  maxDecomp,
float *  averageDecomp 
)

AutomaticEnd Function********************************************************************

Synopsis [Gets the statistics of recursions of transition function method.]

Description [Gets the statistics of recursions of transition function method.]

SideEffects []

SeeAlso []

Definition at line 152 of file imgTfm.c.

{
  ImgTfmInfo_t  *info;

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

  info = (ImgTfmInfo_t *)imageInfo->methodData;
  if (preFlag) {
    *nRecurs = info->nRecursionB;
    *nLeaves = info->nLeavesB;
    *nTurns = info->nTurnsB;
    *averageDepth = info->averageDepthB;
    *maxDepth = info->maxDepthB;
    *nDecomps = 0;
    *topDecomp = 0;
    *maxDecomp = 0;
    *averageDecomp = 0.0;
  } else {
    *nRecurs = info->nRecursion;
    *nLeaves = info->nLeaves;
    *nTurns = info->nTurns;
    *averageDepth = info->averageDepth;
    *maxDepth = info->maxDepth;
    *nDecomps = info->nDecomps;
    *topDecomp = info->topDecomp;
    *maxDecomp = info->maxDecomp;
    *averageDecomp = info->averageDecomp;
  }
  return(1);
}

Here is the caller graph for this function:

void Img_TfmPrintRecursionStatistics ( Img_ImageInfo_t *  imageInfo,
int  preFlag 
)

Function********************************************************************

Synopsis [Prints the statistics of recursions for transition function method.]

Description [Prints the statistics of recursions for transition function method.]

SideEffects []

SeeAlso []

Definition at line 232 of file imgTfm.c.

{
  float avgDepth, avgDecomp;
  int   nRecurs, nLeaves, nTurns, nDecomps, topDecomp, maxDecomp;
  int   maxDepth;

  (void) Img_TfmGetRecursionStatistics(imageInfo, preFlag, &nRecurs, &nLeaves,
                                &nTurns, &avgDepth, &maxDepth, &nDecomps,
                                &topDecomp, &maxDecomp, &avgDecomp);
  if (preFlag)
    fprintf(vis_stdout, "** recursion statistics of splitting (preImg) **\n");
  else
    fprintf(vis_stdout, "** recursion statistics of splitting (img) **\n");
  fprintf(vis_stdout, "# recursions = %d\n", nRecurs);
  fprintf(vis_stdout, "# leaves = %d\n", nLeaves);
  fprintf(vis_stdout, "# turns = %d\n", nTurns);
  fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n",
          avgDepth, maxDepth);
  if (!preFlag) {
    fprintf(vis_stdout,
            "# decompositions = %d (top = %d, max = %d, average = %g)\n",
            nDecomps, topDecomp, maxDecomp, avgDecomp);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Img_TfmPrintStatistics ( Img_ImageInfo_t *  imageInfo,
Img_DirectionType  dir 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 205 of file imgTfm.c.

{
  if (dir == Img_Forward_c || dir == Img_Both_c) {
    Img_TfmPrintCacheStatistics(imageInfo, 0);
    Img_TfmPrintRecursionStatistics(imageInfo, 0);
  }
  if (dir == Img_Backward_c || dir == Img_Both_c) {
    Img_TfmPrintCacheStatistics(imageInfo, 1);
    Img_TfmPrintRecursionStatistics(imageInfo, 1);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgAbstractTransitionFunction ( Img_ImageInfo_t *  imageInfo,
array_t *  abstractVars,
mdd_t *  abstractCube,
Img_DirectionType  directionType,
int  printStatus 
)

Function********************************************************************

Synopsis [Abstracts out given variables from transition function.]

Description [Abstracts out given variables from transition function. abstractVars should be an array of bdd variables.]

SideEffects []

Definition at line 1508 of file imgTfm.c.

{
  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)imageInfo->methodData;
  int                   i, size = 0;
  bdd_t                 *abstractedFunction;
  ImgComponent_t        *comp;
  array_t               *vector;
  int                   flag = 0;
  int                   fwd_size = 0, bwd_size = 0;
  bdd_t                 *relation, *abstractedRelation;

  if (!abstractVars || array_n(abstractVars) == 0)
    return;

  if (info->vector) {
    if (printStatus)
      size = ImgVectorBddSize(info->vector);

    arrayForEachItem(ImgComponent_t *, info->vector, i, comp) {
      if (bdd_is_tautology(comp->func, 1))
        continue;
      if (abstractCube)
        abstractedFunction = bdd_smooth_with_cube(comp->func, abstractCube);
      else
        abstractedFunction = bdd_smooth(comp->func, abstractVars);
      if (bdd_is_tautology(abstractedFunction, 1)) {
        comp->flag = 1;
        flag = 1;
        continue;
      }
      if (mdd_equal(abstractedFunction, comp->func))
        mdd_free(abstractedFunction);
      else {
        if (printStatus == 2) {
          (void) fprintf(vis_stdout,
              "IMG Info: abstracted function %d => %d in component %d\n",
                         bdd_size(comp->func), bdd_size(abstractedFunction), i);
        }
        mdd_free(comp->func);
        comp->func = abstractedFunction;
        ImgSupportClear(info, comp->support);
        ImgComponentGetSupport(comp);
      }
    }

    if (flag) {
      vector = info->vector;
      info->vector = array_alloc(ImgComponent_t *, 0);
      arrayForEachItem(ImgComponent_t *, vector, i, comp) {
        if (comp->flag) {
          ImgComponentFree(comp);
          continue;
        }
        array_insert_last(ImgComponent_t *, info->vector, comp);
      }
      array_free(vector);
    }

    if (printStatus) {
      (void) fprintf(vis_stdout,
       "IMG Info: abstracted function [%d => %ld] with %d components\n",
                     size, ImgVectorBddSize(info->vector),
                     array_n(info->vector));
    }
  }

  if (info->buildTR == 0)
    return;
  else if (info->buildTR == 1 && info->option->synchronizeTr) {
    if (info->fwdClusteredRelationArray &&
        (directionType == Img_Forward_c || directionType == Img_Both_c)) {
      RebuildTransitionRelation(info, Img_Forward_c);
    }
    if (info->bwdClusteredRelationArray &&
        (directionType == Img_Backward_c || directionType == Img_Both_c)) {
      RebuildTransitionRelation(info, Img_Backward_c);
    }
    return;
  }

  if (printStatus) {
    if (directionType == Img_Forward_c || directionType == Img_Both_c)
      fwd_size = bdd_size_multiple(info->fwdClusteredRelationArray);
    if (directionType == Img_Backward_c || directionType == Img_Both_c)
      bwd_size = bdd_size_multiple(info->bwdClusteredRelationArray);
  }
  if (info->fwdClusteredRelationArray &&
      (directionType == Img_Forward_c || directionType == Img_Both_c)) {
    arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) {
      if (abstractCube)
        abstractedRelation = bdd_smooth_with_cube(relation, abstractCube);
      else
        abstractedRelation = bdd_smooth(relation, abstractVars);
      if (printStatus == 2) {
        (void) fprintf(vis_stdout,
          "IMG Info: abstracted fwd relation %d => %d in component %d\n",
                         bdd_size(relation), bdd_size(abstractedRelation), i);
      }
      mdd_free(relation);
      array_insert(bdd_t*, info->fwdClusteredRelationArray, i,
                   abstractedRelation);
    }
  }
  if (info->bwdClusteredRelationArray &&
      (directionType == Img_Backward_c || directionType == Img_Both_c)) {
    arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) {
      if (abstractCube)
        abstractedRelation = bdd_smooth_with_cube(relation, abstractCube);
      else
        abstractedRelation = bdd_smooth(relation, abstractVars);
      if (printStatus == 2) {
        (void) fprintf(vis_stdout,
          "IMG Info: abstracted bwd relation %d => %d in component %d\n",
                         bdd_size(relation), bdd_size(abstractedRelation), i);
      }
      mdd_free(relation);
      array_insert(bdd_t*, info->bwdClusteredRelationArray, i,
                   abstractedRelation);
    }
  }
  if (printStatus) {
    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
      (void) fprintf(vis_stdout,
     "IMG Info: abstracted fwd relation [%d => %ld] with %d components\n",
                     fwd_size,
                     bdd_size_multiple(info->fwdClusteredRelationArray),
                     array_n(info->fwdClusteredRelationArray));
    }
    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
      (void) fprintf(vis_stdout,
     "IMG Info: abstracted bwd relation [%d => %ld] with %d components\n",
                     bwd_size,
                     bdd_size_multiple(info->bwdClusteredRelationArray),
                     array_n(info->bwdClusteredRelationArray));
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgAddDontCareToTransitionFunction ( void *  methodData,
array_t *  constrainArray,
Img_MinimizeType  minimizeMethod,
Img_DirectionType  directionType,
int  printStatus 
)

Function********************************************************************

Synopsis [Adds a dont care set to the transition function and relation.]

Description [Adds a dont care set to the transition function and relation. This function is called during guided search.]

SideEffects []

Definition at line 1362 of file imgTfm.c.

{
  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
  int                   i, j;
  bdd_t                 *function, *simplifiedFunction;
  bdd_t                 *constrain;
  bdd_t                 *relation, *simplifiedRelation;
  int                   size = 0;
  long                  sizeConstrain;
  ImgComponent_t        *comp;

  if (printStatus)
    sizeConstrain = bdd_size_multiple(constrainArray);
  else
    sizeConstrain = 0;

  if (info->vector) {
    if (printStatus)
      size = ImgVectorBddSize(info->vector);

    arrayForEachItem(ImgComponent_t *, info->vector, i, comp) {
      function = mdd_dup(comp->func);
      arrayForEachItem(bdd_t *, constrainArray, j, constrain) {
        if (bdd_is_tautology(constrain, 1))
          continue;
        simplifiedFunction = Img_AddDontCareToImage(function, constrain,
                                                    minimizeMethod);
        if (printStatus == 2) {
          (void) fprintf(vis_stdout,
              "IMG Info: minimized function %d | %d => %d in component %d\n",
                          bdd_size(function), bdd_size(constrain),
                          bdd_size(simplifiedFunction), i);
        }
        mdd_free(function);
        function = simplifiedFunction;
      }
      if (mdd_equal(function, comp->func))
        mdd_free(function);
      else {
        mdd_free(comp->func);
        comp->func = function;
        ImgSupportClear(info, comp->support);
        ImgComponentGetSupport(comp);
      }
    }

    if (printStatus) {
      (void) fprintf(vis_stdout,
        "IMG Info: minimized function [%d | %ld => %ld] with %d components\n",
                   size, sizeConstrain,
                   ImgVectorBddSize(info->vector), array_n(info->vector));
    }
  }

  if (info->buildTR == 0)
    return;
  else if (info->buildTR == 1 && info->option->synchronizeTr) {
    if (info->fwdClusteredRelationArray &&
        (directionType == Img_Forward_c || directionType == Img_Both_c)) {
      RebuildTransitionRelation(info, Img_Forward_c);
    }
    if (info->bwdClusteredRelationArray &&
        (directionType == Img_Backward_c || directionType == Img_Both_c)) {
      RebuildTransitionRelation(info, Img_Backward_c);
    }
    return;
  }

  if (info->fwdClusteredRelationArray &&
      (directionType == Img_Forward_c || directionType == Img_Both_c)) {
    if (printStatus)
      size = bdd_size_multiple(info->fwdClusteredRelationArray);
    arrayForEachItem(bdd_t *, constrainArray, i, constrain) {
      if (bdd_is_tautology(constrain, 1))
        continue;

      arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, j, relation) {
        simplifiedRelation = Img_AddDontCareToImage(relation, constrain,
                                                    minimizeMethod);
        if (printStatus == 2) {
          (void) fprintf(vis_stdout,
            "IMG Info: minimized fwd relation %d | %d => %d in component %d\n",
                         bdd_size(relation), bdd_size(constrain),
                         bdd_size(simplifiedRelation), j);
        }
        mdd_free(relation);
        array_insert(bdd_t*, info->fwdClusteredRelationArray, j,
                     simplifiedRelation);
      }
    }
    if (printStatus) {
      (void) fprintf(vis_stdout,
     "IMG Info: minimized fwd relation [%d | %ld => %ld] with %d components\n",
                     size, sizeConstrain,
                     bdd_size_multiple(info->fwdClusteredRelationArray),
                     array_n(info->fwdClusteredRelationArray));
    }
  }
  if (info->bwdClusteredRelationArray &&
      (directionType == Img_Backward_c || directionType == Img_Both_c)) {
    if (printStatus)
      size = bdd_size_multiple(info->bwdClusteredRelationArray);
    arrayForEachItem(bdd_t *, constrainArray, i, constrain) {
      if (bdd_is_tautology(constrain, 1))
        continue;

      arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, j, relation) {
        simplifiedRelation = Img_AddDontCareToImage(relation, constrain,
                                                    minimizeMethod);
        if (printStatus == 2) {
          (void) fprintf(vis_stdout,
            "IMG Info: minimized bwd relation %d | %d => %d in component %d\n",
                         bdd_size(relation), bdd_size(constrain),
                         bdd_size(simplifiedRelation), j);
        }
        mdd_free(relation);
        array_insert(bdd_t*, info->bwdClusteredRelationArray, j,
                     simplifiedRelation);
      }
    }
    if (printStatus) {
      (void) fprintf(vis_stdout,
     "IMG Info: minimized bwd relation [%d | %ld => %ld] with %d components\n",
                     size, sizeConstrain,
                     bdd_size_multiple(info->bwdClusteredRelationArray),
                     array_n(info->bwdClusteredRelationArray));
    }
  }
}

Here is the call graph for this function:

int ImgApproximateTransitionFunction ( mdd_manager *  mgr,
void *  methodData,
bdd_approx_dir_t  approxDir,
bdd_approx_type_t  approxMethod,
int  approxThreshold,
double  approxQuality,
double  approxQualityBias,
Img_DirectionType  directionType,
mdd_t *  bias 
)

Function********************************************************************

Synopsis [Approximate transition function.]

Description [Approximate transition function.]

SideEffects []

Definition at line 1659 of file imgTfm.c.

{
  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
  int                   i;
  bdd_t                 *approxFunction;
  int                   unchanged = 0;
  ImgComponent_t        *comp;
  bdd_t                 *relation, *approxRelation;

  if (info->vector) {
    arrayForEachItem(ImgComponent_t *, info->vector, i, comp) {
      approxFunction = Img_ApproximateImage(mgr, comp->func,
                                            approxDir, approxMethod,
                                            approxThreshold, approxQuality,
                                            approxQualityBias, bias);
      if (bdd_is_tautology(approxFunction, 1)) {
        fprintf(vis_stdout,
                  "** img warning : bdd_one from subsetting in [%d].\n", i);
        mdd_free(approxFunction);
        unchanged++;
      } else if (bdd_is_tautology(approxFunction, 0)) {
        fprintf(vis_stdout,
                  "** img warning : bdd_zero from subsetting in [%d].\n", i);
        mdd_free(approxFunction);
        unchanged++;
      } else if (mdd_equal(approxFunction, comp->func)) {
        mdd_free(approxFunction);
        unchanged++;
      } else {
        mdd_free(comp->func);
        comp->func = approxFunction;
        ImgSupportClear(info, comp->support);
        ImgComponentGetSupport(comp);
      }
    }
  }

  if (info->buildTR == 0)
    return(unchanged);
  else if (info->buildTR == 1 && info->option->synchronizeTr) {
    if (info->fwdClusteredRelationArray &&
        (directionType == Img_Forward_c || directionType == Img_Both_c)) {
      RebuildTransitionRelation(info, Img_Forward_c);
    }
    if (info->bwdClusteredRelationArray &&
        (directionType == Img_Backward_c || directionType == Img_Both_c)) {
      RebuildTransitionRelation(info, Img_Backward_c);
    }
    return(unchanged);
  }

  if (info->fwdClusteredRelationArray &&
      (directionType == Img_Forward_c || directionType == Img_Both_c)) {
    arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) {
      approxRelation = Img_ApproximateImage(mgr, relation,
                                            approxDir, approxMethod,
                                            approxThreshold, approxQuality,
                                            approxQualityBias, bias);
      if (bdd_is_tautology(approxRelation, 1)) {
        fprintf(vis_stdout,
                "** img warning : bdd_one from subsetting in fwd[%d].\n", i);
        mdd_free(approxRelation);
        unchanged++;
      } else if (bdd_is_tautology(approxRelation, 0)) {
        fprintf(vis_stdout,
                "** img warning : bdd_zero from subsetting in fwd[%d].\n", i);
        mdd_free(approxRelation);
        unchanged++;
      } else if (mdd_equal(approxRelation, relation)) {
        mdd_free(approxRelation);
        unchanged++;
      } else {
        mdd_free(relation);
        array_insert(bdd_t*, info->fwdClusteredRelationArray, i,
                     approxRelation);
      }
    }
  }
  if (info->bwdClusteredRelationArray &&
      (directionType == Img_Backward_c || directionType == Img_Both_c)) {
    arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) {
      approxRelation = Img_ApproximateImage(mgr, relation,
                                            approxDir, approxMethod,
                                            approxThreshold, approxQuality,
                                            approxQualityBias, bias);
      if (bdd_is_tautology(approxRelation, 1)) {
        fprintf(vis_stdout,
                "** img warning : bdd_one from subsetting in bwd[%d].\n", i);
        mdd_free(approxRelation);
        unchanged++;
      } else if (bdd_is_tautology(approxRelation, 0)) {
        fprintf(vis_stdout,
                "** img warning : bdd_zero from subsetting in bwd[%d].\n", i);
        mdd_free(approxRelation);
        unchanged++;
      } else if (mdd_equal(approxRelation, relation)) {
        mdd_free(approxRelation);
        unchanged++;
      } else {
        mdd_free(relation);
        array_insert(bdd_t*, info->bwdClusteredRelationArray, i,
                     approxRelation);
      }
    }
  }
  return(unchanged);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgDuplicateTransitionFunction ( Img_ImageInfo_t *  imageInfo,
Img_DirectionType  directionType 
)

Function********************************************************************

Synopsis [Duplicates transition function.]

Description [Duplicates transition function.]

SideEffects []

Definition at line 1178 of file imgTfm.c.

{
  array_t       *copiedVector;
  array_t       *copiedRelation;
  ImgTfmInfo_t  *tfmInfo = (ImgTfmInfo_t *)imageInfo->methodData;

  if (tfmInfo->vector) {
    copiedVector = ImgVectorCopy(tfmInfo, tfmInfo->vector);
    assert(!imageInfo->savedRelation);
    imageInfo->savedRelation = (void *)tfmInfo->vector;
    tfmInfo->vector = copiedVector;
  }
  if (tfmInfo->fwdClusteredRelationArray) {
    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
      copiedRelation = mdd_array_duplicate(tfmInfo->fwdClusteredRelationArray);
      tfmInfo->fwdSavedRelation = tfmInfo->fwdClusteredRelationArray;
      tfmInfo->fwdClusteredRelationArray = copiedRelation;
    }
  }
  if (tfmInfo->bwdClusteredRelationArray) {
    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
      copiedRelation = mdd_array_duplicate(tfmInfo->bwdClusteredRelationArray);
      tfmInfo->bwdSavedRelation = tfmInfo->bwdClusteredRelationArray;
      tfmInfo->bwdClusteredRelationArray = copiedRelation;
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* ImgGetTransitionFunction ( void *  methodData,
Img_DirectionType  directionType 
)

Function********************************************************************

Synopsis [Returns current transition function.]

Description [Returns current transition function.]

SideEffects []

Definition at line 1782 of file imgTfm.c.

{
  ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)methodData;
  if (tfmInfo->vector)
    return(tfmInfo->vector);
  if (directionType == Img_Forward_c)
    return(tfmInfo->fwdClusteredRelationArray);
  return(tfmInfo->bwdClusteredRelationArray);
}

Here is the caller graph for this function:

void ImgImageConstrainAndClusterTransitionRelationTfm ( Img_ImageInfo_t *  imageInfo,
Img_DirectionType  direction,
mdd_t *  constrain,
Img_MinimizeType  minimizeMethod,
boolean  underApprox,
boolean  cleanUp,
boolean  forceReorder,
int  printStatus 
)

Function********************************************************************

Synopsis [Constrains the bit function and relation and creates a new transition function vector and relation.]

Description [Constrains the bit function and relation and creates a new transition function vector and relation. First, the existing transition function vector and relation is freed. The bit relation is created if it isnt stored already. The bit relation is then copied into the Clustered relation of the given direction and constrained by the given constraint. The bit relation is clustered. In the case of the backward relation, the clustered relation is minimized with respect to the care set.]

SideEffects [Frees current transition relation]

Definition at line 2172 of file imgTfm.c.

{
  ImgFunctionData_t     *functionData = &(imageInfo->functionData);
  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)imageInfo->methodData;
  graph_t               *mddNetwork;
  mdd_manager           *mddManager = Part_PartitionReadMddManager(
                                        functionData->mddNetwork);
  int                   composeIntermediateVars, findIntermediateVars;
  array_t               *relationArray;

  /* free existing function vector and/or relation */
  ImgImageFreeClusteredTransitionRelationTfm(imageInfo->methodData, direction);
  if (forceReorder)
    bdd_reorder(mddManager);

  mddNetwork = functionData->mddNetwork;

  /* create function vector or bit relation */
  if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c &&
      info->nVars != info->nRealVars) {
    if (info->option->composeIntermediateVars) {
      composeIntermediateVars = 1;
      findIntermediateVars = 0;
    } else {
      composeIntermediateVars = 0;
      findIntermediateVars = 1;
    }
  } else {
    composeIntermediateVars = 0;
    findIntermediateVars = 0;
  }

  if (info->buildTR == 2) { /* non-deterministic */
    if (info->buildPartialTR) {
      info->fullVector = TfmCreateBitVector(info, composeIntermediateVars,
                                            findIntermediateVars);
      TfmSetupPartialTransitionRelation(info, &relationArray);
    } else {
      info->vector = NIL(array_t);
      relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars,
                                                findIntermediateVars);
    }
  } else {
    info->vector = TfmCreateBitVector(info, composeIntermediateVars,
                                        findIntermediateVars);
    if (info->buildTR == 0 || info->option->synchronizeTr)
      relationArray = NIL(array_t);
    else {
      relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars,
                                                findIntermediateVars);
    }
  }

  /* apply the constrain to the bit relation */
  if (constrain) {
    if (underApprox) {
      MinimizeTransitionFunction(info->vector, relationArray,
                                 constrain, minimizeMethod, printStatus);
    } else {
      AddDontCareToTransitionFunction(info->vector, relationArray,
                                      constrain, minimizeMethod, printStatus);
    }
  }

  if (info->vector && info->option->sortVectorFlag && info->option->useCache)
    array_sort(info->vector, CompareIndex);
  if (info->buildTR) {
    TfmBuildRelationArray(info, functionData, relationArray, direction, 0);
    if (relationArray)
      mdd_array_free(relationArray);
  }

  /* Print information */
  if (info->option->verbosity > 0){
    if (info->method == Img_Tfm_c)
      fprintf(vis_stdout,"Computing Image Using tfm technique.\n");
    else
      fprintf(vis_stdout,"Computing Image Using hybrid technique.\n");
    fprintf(vis_stdout,"Total # of domain binary variables = %3d\n",
            array_n(functionData->domainBddVars));
    fprintf(vis_stdout,"Total # of range binary variables = %3d\n",
            array_n(functionData->rangeBddVars));
    fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n",
            array_n(functionData->quantifyBddVars));
    if (info->vector) {
      (void) fprintf(vis_stdout,
                     "Shared size of transition function vector for image ");
      (void) fprintf(vis_stdout,
                     "computation is %10ld BDD nodes (%-4d components)\n",
                     ImgVectorBddSize(info->vector), array_n(info->vector));
    }
    if (((direction == Img_Forward_c) || (direction == Img_Both_c)) &&
        (info->fwdClusteredRelationArray != NIL(array_t))) {
      (void) fprintf(vis_stdout,
                     "Shared size of transition relation for forward image ");
      (void) fprintf(vis_stdout,
                     "computation is %10ld BDD nodes (%-4d components)\n",
                     bdd_size_multiple(info->fwdClusteredRelationArray),
                     array_n(info->fwdClusteredRelationArray));
    }
    if (((direction == Img_Backward_c) || (direction == Img_Both_c)) &&
      (info->bwdClusteredRelationArray != NIL(array_t))) {
      (void) fprintf(vis_stdout,
                     "Shared size of transition relation for backward image ");
      (void) fprintf(vis_stdout,
                     "computation is %10ld BDD nodes (%-4d components)\n",
                     bdd_size_multiple(info->bwdClusteredRelationArray),
                     array_n(info->bwdClusteredRelationArray));
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgImageFreeClusteredTransitionRelationTfm ( void *  methodData,
Img_DirectionType  directionType 
)

Function********************************************************************

Synopsis [Frees current transition function vector and relation for the given direction.]

Description [Frees current transition function vector and relation for the given direction.]

SideEffects []

Definition at line 2126 of file imgTfm.c.

{
  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)methodData;

  if (info->vector) {
    ImgVectorFree(info->vector);
    info->vector = NIL(array_t);
  }
  if (info->fullVector) {
    ImgVectorFree(info->fullVector);
    info->fullVector = NIL(array_t);
  }
  if (info->partialBddVars)
    mdd_array_free(info->partialBddVars);
  if (info->partialVarFlag)
    FREE(info->partialVarFlag);
  if (info->fwdClusteredRelationArray != NIL(array_t)) {
    mdd_array_free(info->fwdClusteredRelationArray);
    info->fwdClusteredRelationArray = NIL(array_t);
  }
  if (info->bwdClusteredRelationArray != NIL(array_t)) {
    mdd_array_free(info->bwdClusteredRelationArray);
    info->bwdClusteredRelationArray = NIL(array_t);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* ImgImageInfoComputeBwdTfm ( ImgFunctionData_t *  functionData,
Img_ImageInfo_t *  imageInfo,
mdd_t *  fromLowerBound,
mdd_t *  fromUpperBound,
array_t *  toCareSetArray 
)

Function********************************************************************

Synopsis [Computes the backward image of domainSubset.]

Description [Computes the backward image of domainSubset.]

SideEffects []

SeeAlso [ImgImageInfoComputeBwdWithDomainVarsTfm]

Definition at line 925 of file imgTfm.c.

{
  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)imageInfo->methodData;
  mdd_t         *image, *domainSubset, *simplifiedImage;
  array_t       *replace;

  if (info->vector == NIL(array_t) &&
      !(info->buildTR == 2 && info->bwdClusteredRelationArray)) {
    fprintf(vis_stderr, "** img error: The data structure has not been ");
    fprintf(vis_stderr, "initialized for backward image computation\n");
    return(NIL(mdd_t));
  }

  info->updatedFlag = FALSE;
  domainSubset = bdd_between(fromLowerBound, fromUpperBound);

  if (info->toCareSetArray)
    replace = info->toCareSetArray;
  else {
    replace = NIL(array_t);
    info->toCareSetArray = toCareSetArray;
  }
  image = ImgTfmPreImage(info, domainSubset);
  info->toCareSetArray = replace;

  mdd_free(domainSubset);
  simplifiedImage = bdd_minimize_array(image, toCareSetArray);
  bdd_free(image);
  return(simplifiedImage);
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* ImgImageInfoComputeBwdWithDomainVarsTfm ( ImgFunctionData_t *  functionData,
Img_ImageInfo_t *  imageInfo,
mdd_t *  fromLowerBound,
mdd_t *  fromUpperBound,
array_t *  toCareSetArray 
)

Function********************************************************************

Synopsis [Computes the backward image of a set of states.]

Description [Identical to ImgImageInfoComputeBwdTfm.]

SideEffects []

SeeAlso [ImgImageInfoComputeBwdTfm]

Definition at line 973 of file imgTfm.c.

{
  mdd_t *image;

  image = ImgImageInfoComputeBwdTfm(functionData,
                imageInfo, fromLowerBound, fromUpperBound, toCareSetArray);
  return(image);
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* ImgImageInfoComputeFwdTfm ( ImgFunctionData_t *  functionData,
Img_ImageInfo_t *  imageInfo,
mdd_t *  fromLowerBound,
mdd_t *  fromUpperBound,
array_t *  toCareSetArray 
)

Function********************************************************************

Synopsis [Computes the forward image of a set of states.]

Description [Computes the forward image of a set of states.]

SideEffects []

SeeAlso [ImgImageInfoComputeFwdWithDomainVarsTfm]

Definition at line 860 of file imgTfm.c.

{
  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)imageInfo->methodData;
  mdd_t         *image, *domainSubset;

  if (info->vector == NIL(array_t) &&
      !(info->buildTR == 2 && info->fwdClusteredRelationArray)) {
    fprintf(vis_stderr, "** img error: The data structure has not been ");
    fprintf(vis_stderr, "initialized for image computation\n");
    return(NIL(mdd_t));
  }

  info->updatedFlag = FALSE;
  domainSubset = bdd_between(fromLowerBound, fromUpperBound);

  image = ImgTfmImage(info, domainSubset);

  mdd_free(domainSubset);
  return(image);
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* ImgImageInfoComputeFwdWithDomainVarsTfm ( ImgFunctionData_t *  functionData,
Img_ImageInfo_t *  imageInfo,
mdd_t *  fromLowerBound,
mdd_t *  fromUpperBound,
array_t *  toCareSetArray 
)

Function********************************************************************

Synopsis [Computes the forward image of a set of states in terms of domain variables.]

Description [Identical to ImgImageInfoComputeFwdTfm.]

SideEffects []

SeeAlso [ImgImageInfoComputeFwdTfm]

Definition at line 899 of file imgTfm.c.

{
  mdd_t *image;

  image = ImgImageInfoComputeFwdTfm(functionData,
                imageInfo , fromLowerBound, fromUpperBound, toCareSetArray);
  return(image);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgImageInfoFreeTfm ( void *  methodData)

Function********************************************************************

Synopsis [Frees the memory associated with imageInfo.]

Description [Frees the memory associated with imageInfo.]

SideEffects []

Definition at line 997 of file imgTfm.c.

{
  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)methodData;

  if (info == NIL(ImgTfmInfo_t)) {
    fprintf(vis_stderr, "** img error: Trying to free the NULL image info\n");
    return;
  }
  if (info->option->printStatistics) {
    if (info->nRecursion) {
      if (info->imgCache)
        ImgPrintCacheStatistics(info->imgCache);
      PrintRecursionStatistics(info, 0);
      PrintFoundVariableStatistics(info, 0);
    }
    if (info->nRecursionB) {
      if (info->preCache)
        ImgPrintCacheStatistics(info->preCache);
      PrintRecursionStatistics(info, 1);
      PrintFoundVariableStatistics(info, 1);
    }
  }
  if (info->vector != NIL(array_t))
    ImgVectorFree(info->vector);
  if (info->toCareSetArray != NIL(array_t))
    mdd_array_free(info->toCareSetArray);
  if (info->imgCache)
    ImgCacheDestroyTable(info->imgCache, info->option->globalCache);
  if (info->preCache)
    ImgCacheDestroyTable(info->preCache, info->option->globalCache);
  st_free_table(info->quantifyVarsTable);
  st_free_table(info->rangeVarsTable);
  if (info->intermediateVarsTable) {
    st_free_table(info->intermediateVarsTable);
    info->intermediateVarsTable = NIL(st_table);
  }
  if (info->intermediateBddVars) {
    mdd_array_free(info->intermediateBddVars);
    info->intermediateBddVars= NIL(array_t);
  }
  if (info->newQuantifyBddVars) {
    mdd_array_free(info->newQuantifyBddVars);
    info->newQuantifyBddVars = NIL(array_t);
  }

  if (info->option->useCache) {
    if (info->option->autoFlushCache == 2) {
      nHookInfoList--;
      st_delete(HookInfoList, &info, NULL);
      if (nHookInfoList == 0) {
        st_free_table(HookInfoList);
        bdd_remove_hook(info->manager, HookInfoFunction,
                        BDD_PRE_REORDERING_HOOK);
      }
    }
  }
  if (info->option != NULL)
    FREE(info->option);

  if (info->fwdClusteredRelationArray)
    mdd_array_free(info->fwdClusteredRelationArray);
  if (info->bwdClusteredRelationArray)
    mdd_array_free(info->bwdClusteredRelationArray);
  if (info->fwdArraySmoothVarBddArray)
    mdd_array_array_free(info->fwdArraySmoothVarBddArray);
  if (info->bwdArraySmoothVarBddArray)
    mdd_array_array_free(info->bwdArraySmoothVarBddArray);
  if (info->fwdSmoothVarCubeArray)
    mdd_array_free(info->fwdSmoothVarCubeArray);
  if (info->bwdSmoothVarCubeArray)
    mdd_array_free(info->bwdSmoothVarCubeArray);
  if (info->trmOption)
    ImgFreeTrmOptions(info->trmOption);
  if (info->partialBddVars)
    mdd_array_free(info->partialBddVars);
  if (info->partialVarFlag)
    FREE(info->partialVarFlag);
  if (info->fullVector != NIL(array_t))
    ImgVectorFree(info->fullVector);

  if (info->foundEssentials)
    FREE(info->foundEssentials);
  if (info->debugCareSet)
    mdd_free(info->debugCareSet);

  if (info->savedArraySmoothVarBddArray != NIL(array_t))
    mdd_array_array_free(info->savedArraySmoothVarBddArray);
  if (info->savedSmoothVarCubeArray != NIL(array_t))
    mdd_array_free(info->savedSmoothVarCubeArray);
  FREE(info);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void* ImgImageInfoInitializeTfm ( void *  methodData,
ImgFunctionData_t *  functionData,
Img_DirectionType  directionType,
Img_MethodType  method 
)

Function********************************************************************

Synopsis [Initializes an image data structure for image computation using transition function method.]

Description [Initialized an image data structure for image computation using transition function method.]

SideEffects []

Definition at line 622 of file imgTfm.c.

{
  int                   i;
  int                   latches;
  int                   variables, nVars;
  array_t               *vector;
  graph_t               *mddNetwork;
  mdd_manager           *mddManager;
  array_t               *rangeVarMddIdArray;
  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
  int                   index;
  mdd_t                 *var;
  char                  *flagValue;
  char                  filename[20];
  int                   composeIntermediateVars, findIntermediateVars;
  int                   nonDeterministic;

  if (info) {
    if (info->option->useCache) {
      if (directionType == Img_Forward_c || directionType == Img_Both_c) {
        if (!info->imgCache)
          ImgCacheInitTable(info, info->option->initCacheSize,
                            info->option->globalCache, FALSE);
      }
      if (directionType == Img_Backward_c || directionType == Img_Both_c) {
        if (!info->preCache)
          ImgCacheInitTable(info, info->option->initCacheSize,
                            info->option->globalCache, TRUE);
      }
    }
    if (info->buildTR &&
        (((directionType == Img_Forward_c || directionType == Img_Both_c) &&
          !info->fwdClusteredRelationArray) ||
         ((directionType == Img_Backward_c || directionType == Img_Both_c) &&
          !info->bwdClusteredRelationArray))) {
      TfmBuildRelationArray(info, functionData, NIL(array_t), directionType, 0);
    }
    return((void *)info);
  }

  mddNetwork = functionData->mddNetwork;
  mddManager = Part_PartitionReadMddManager(mddNetwork);
  rangeVarMddIdArray = functionData->rangeVars;

  nonDeterministic = CheckNondeterminism(functionData->network);
  if (nonDeterministic)
    info = TfmInfoStructAlloc(Img_Hybrid_c);
  else
    info = TfmInfoStructAlloc(method);
  info->nonDeterministic = nonDeterministic;
  info->functionData = functionData;
  info->quantifyVarsTable = st_init_table(st_numcmp, st_numhash);
  for (i = 0; i < array_n(functionData->quantifyBddVars); i++) {
    var = array_fetch(mdd_t *, functionData->quantifyBddVars, i);
    index = (int)bdd_top_var_id(var);
    st_insert(info->quantifyVarsTable, (char *)(long)index, NIL(char));
  }
  info->rangeVarsTable = st_init_table(st_numcmp, st_numhash);
  for (i = 0; i < array_n(functionData->rangeBddVars); i++) {
    var = array_fetch(mdd_t *, functionData->rangeBddVars, i);
    index = (int)bdd_top_var_id(var);
    st_insert(info->rangeVarsTable, (char *)(long)index, NIL(char));
  }

  latches = 2 * mdd_get_number_of_bdd_vars(mddManager, rangeVarMddIdArray);
  nVars = latches + mdd_get_number_of_bdd_vars(mddManager,
                                                functionData->quantifyVars);
  variables = bdd_num_vars(mddManager); /* real number of variables */
  info->nRealVars = nVars;
  info->nVars = variables;

  if (info->nonDeterministic) {
    if (method == Img_Tfm_c) {
      fprintf(vis_stdout,
        "** tfm warning: The circuit may have nondeterminism.\n");
      fprintf(vis_stdout, "\tautomatically switched to hybrid mode = 2.\n");
      info->method = Img_Hybrid_c;
    } else {
      if (info->option->hybridMode == 2) {
        if (info->option->buildPartialTR) {
          fprintf(vis_stdout,
                "** hyb warning: The circuit may have nondeterminism.\n");
          fprintf(vis_stdout,
                "\tdid not use partial transition relation.\n");
        } else {
          fprintf(vis_stdout,
                "** hyb info: The circuit may have nondeterminism.\n");
        }
      } else {
        fprintf(vis_stdout,
                "** hyb warning: The circuit may have nondeterminism.\n");
        fprintf(vis_stdout, "\tautomatically switched to hybrid mode = 2.\n");
      }
    }
  }
  if (info->nonDeterministic ||
      (info->option->hybridMode > 0 &&
       (info->option->splitMethod == 3 || info->option->preSplitMethod == 4))) {
    if (info->option->hybridMode == 2 || info->nonDeterministic)
      info->buildTR = 2;
    else
      info->buildTR = 1;
  }
  if (info->buildTR == 2 &&
      info->option->buildPartialTR &&
      info->nonDeterministic == 0 &&
      info->option->useCache == 0) {
    info->buildPartialTR = TRUE;
  }

  info->imgKeepPiInTr = info->option->imgKeepPiInTr;
  if (info->option->useCache)
    info->preKeepPiInTr = TRUE;
  else
    info->preKeepPiInTr = info->option->preKeepPiInTr;

  if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c &&
      nVars != variables) {
    if (info->option->composeIntermediateVars) {
      composeIntermediateVars = 1;
      findIntermediateVars = 0;
    } else {
      composeIntermediateVars = 0;
      findIntermediateVars = 1;
    }
  } else {
    composeIntermediateVars = 0;
    findIntermediateVars = 0;
  }

  if (info->buildTR != 2 || info->buildPartialTR) { /* deterministic */
    vector = TfmCreateBitVector(info, composeIntermediateVars,
                                findIntermediateVars);
  } else
    vector = NIL(array_t);

  info->manager = mddManager;
  if (info->buildPartialTR)
    info->fullVector = vector;
  else
    info->vector = vector;
  if (info->buildTR == 2)
    info->useConstraint = 1;
  else if (info->option->splitMethod == 1)
    info->useConstraint = 0;
  else {
    if (info->option->rangeComp == 2)
      info->useConstraint = 2;
    else if (info->option->rangeComp == 0)
      info->useConstraint = 1;
    else
      info->useConstraint = 0;
  }
  if (info->option->useCache) {
    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
      ImgCacheInitTable(info, info->option->initCacheSize,
                        info->option->globalCache, FALSE);
    }
    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
      ImgCacheInitTable(info, info->option->initCacheSize,
                        info->option->globalCache, TRUE);
    }
    if (info->option->autoFlushCache == 2) {
      if (nHookInfoList == 0) {
        HookInfoList = st_init_table(st_ptrcmp, st_ptrhash);
        bdd_add_hook(info->manager, HookInfoFunction, BDD_PRE_REORDERING_HOOK);
        st_insert(HookInfoList, (char *)info, NIL(char));
      } else {
        if (info->option->globalCache == 0)
          st_insert(HookInfoList, (char *)info, NIL(char));
      }
      nHookInfoList++;
    }
  }

  info->trmOption = ImgGetTrmOptions();
  info->domainVarBddArray = functionData->domainBddVars;
  info->quantifyVarBddArray = functionData->quantifyBddVars;
  info->rangeVarBddArray = functionData->rangeBddVars;

  if (info->vector && info->option->sortVectorFlag && info->option->useCache)
    array_sort(info->vector, CompareIndex);
  if (info->buildPartialTR)
    TfmSetupPartialTransitionRelation(info, NIL(array_t *));
  if (info->buildTR)
    TfmBuildRelationArray(info, functionData, NIL(array_t), directionType, 1);
  if (info->buildTR == 1) {
    ImgPrintVectorDependency(info, info->vector, info->option->verbosity);
    if (info->option->writeSupportMatrix == 1) {
      sprintf(filename, "support%d.mat", info->option->supportFileCount++);
      ImgWriteSupportMatrix(info, info->vector, NIL(array_t), filename);
    }
  }
  if (info->option->writeSupportMatrixAndStop)
    exit(0);

  flagValue = Cmd_FlagReadByName("image_eliminate_depend_vars");
  if (flagValue == NIL(char))
    info->eliminateDepend = 0; /* the default value */
  else
    info->eliminateDepend = atoi(flagValue);
  if (info->eliminateDepend && bdd_get_package_name() != CUDD) {
    fprintf(vis_stderr,
    "** tfm error : image_eliminate_depend_vars is available for only CUDD.\n");
    info->eliminateDepend = 0;
  }
  info->nPrevEliminatedFwd = -1;

  flagValue = Cmd_FlagReadByName("image_verbosity");
  if (flagValue)
    info->imageVerbosity = atoi(flagValue);

  if (info->option->printEssential) {
    info->foundEssentials = ALLOC(int, IMG_TF_MAX_PRINT_DEPTH);
    memset(info->foundEssentials, 0, sizeof(int) * IMG_TF_MAX_PRINT_DEPTH);
  }
  if (info->option->debug)
    info->debugCareSet = bdd_one(mddManager);
  else
    info->debugCareSet = NIL(mdd_t);
  return((void *)info);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgImageInfoPrintMethodParamsTfm ( void *  methodData,
FILE *  fp 
)

Function********************************************************************

Synopsis [Prints information about the transition function method.]

Description [This function is used to obtain the information about the parameters used to initialize the imageInfo.]

SideEffects []

Definition at line 1101 of file imgTfm.c.

{
  ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData;

  if (fp == NULL)
    return;
  if (info->vector)
    ImgPrintVectorDependency(info, info->vector, 1);
  if (info->method == Img_Tfm_c) {
    fprintf(vis_stdout,
            "For the options in tfm method, try print_tfm_options.\n");
    return;
  }
  if (info->fwdClusteredRelationArray != NIL(array_t)) {
    fprintf(fp, "Shared size of transition relation for forward image");
    fprintf(fp, " computation is %10ld BDD nodes (%-4d components)\n",
            bdd_size_multiple(info->fwdClusteredRelationArray),
            array_n(info->fwdClusteredRelationArray));
  }
  if (info->bwdClusteredRelationArray != NIL(array_t)) {
    fprintf(fp, "Shared size of transition relation for backward image");
    fprintf(fp, " computation is %10ld BDD nodes (%-4d components)\n",
            bdd_size_multiple(info->bwdClusteredRelationArray),
            array_n(info->bwdClusteredRelationArray));
  }
  fprintf(vis_stdout, "For the options in hybrid method,");
  fprintf(vis_stdout, " try print_hybrid_options and print_tfm_options.\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ImgIsPartitionedTransitionRelationTfm ( Img_ImageInfo_t *  imageInfo)

Function********************************************************************

Synopsis [Check whether transition relation is built in hybrid.]

Description [Check whether transition relation is built in hybrid.]

SideEffects []

Definition at line 2302 of file imgTfm.c.

{
  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)imageInfo->methodData;

  if (info->buildTR)
    return(1);
  else
    return(0);
}

Here is the caller graph for this function:

void ImgMinimizeTransitionFunction ( void *  methodData,
array_t *  constrainArray,
Img_MinimizeType  minimizeMethod,
Img_DirectionType  directionType,
int  printStatus 
)

Function********************************************************************

Synopsis [Minimizes transition function with given set of constraints.]

Description [Minimizes transition function with given set of constraints.]

SideEffects []

Definition at line 1218 of file imgTfm.c.

{
  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
  int                   i, j;
  bdd_t                 *function, *simplifiedFunction;
  bdd_t                 *constrain;
  bdd_t                 *relation, *simplifiedRelation;
  int                   size = 0;
  long                  sizeConstrain;
  ImgComponent_t        *comp;

  if (printStatus)
    sizeConstrain = bdd_size_multiple(constrainArray);
  else
    sizeConstrain = 0;

  if (info->vector) {
    if (printStatus)
      size = ImgVectorBddSize(info->vector);

    arrayForEachItem(ImgComponent_t *, info->vector, i, comp) {
      function = mdd_dup(comp->func);
      arrayForEachItem(bdd_t *, constrainArray, j, constrain) {
        if (bdd_is_tautology(constrain, 1))
          continue;
        simplifiedFunction = Img_MinimizeImage(function, constrain,
                                               minimizeMethod, TRUE);
        if (printStatus == 2) {
          (void) fprintf(vis_stdout,
              "IMG Info: minimized function %d | %d => %d in component %d\n",
                          bdd_size(function), bdd_size(constrain),
                          bdd_size(simplifiedFunction), i);
        }
        mdd_free(function);
        function = simplifiedFunction;
      }
      if (mdd_equal(function, comp->func))
        mdd_free(function);
      else {
        mdd_free(comp->func);
        comp->func = function;
        ImgSupportClear(info, comp->support);
        ImgComponentGetSupport(comp);
      }
    }

    if (printStatus) {
      (void) fprintf(vis_stdout,
        "IMG Info: minimized function [%d | %ld => %ld] with %d components\n",
                   size, sizeConstrain,
                   ImgVectorBddSize(info->vector), array_n(info->vector));
    }
  }

  if (info->buildTR == 0)
    return;
  else if (info->buildTR == 1 && info->option->synchronizeTr) {
    if (info->fwdClusteredRelationArray &&
        (directionType == Img_Forward_c || directionType == Img_Both_c)) {
      RebuildTransitionRelation(info, Img_Forward_c);
    }
    if (info->bwdClusteredRelationArray &&
        (directionType == Img_Backward_c || directionType == Img_Both_c)) {
      RebuildTransitionRelation(info, Img_Backward_c);
    }
    return;
  }

  if (info->fwdClusteredRelationArray &&
      (directionType == Img_Forward_c || directionType == Img_Both_c)) {
    if (printStatus)
      size = bdd_size_multiple(info->fwdClusteredRelationArray);
    arrayForEachItem(bdd_t *, constrainArray, i, constrain) {
      if (bdd_is_tautology(constrain, 1))
        continue;

      arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, j, relation) {
        simplifiedRelation = Img_MinimizeImage(relation, constrain,
                                                 minimizeMethod, TRUE);
        if (printStatus == 2) {
          (void) fprintf(vis_stdout,
            "IMG Info: minimized fwd relation %d | %d => %d in component %d\n",
                         bdd_size(relation), bdd_size(constrain),
                         bdd_size(simplifiedRelation), j);
        }
        mdd_free(relation);
        array_insert(bdd_t*, info->fwdClusteredRelationArray, j,
                     simplifiedRelation);
      }
    }
    if (printStatus) {
      (void) fprintf(vis_stdout,
     "IMG Info: minimized fwd relation [%d | %ld => %ld] with %d components\n",
                     size, sizeConstrain,
                     bdd_size_multiple(info->fwdClusteredRelationArray),
                     array_n(info->fwdClusteredRelationArray));
    }
  }
  if (info->bwdClusteredRelationArray &&
      (directionType == Img_Backward_c || directionType == Img_Both_c)) {
    if (printStatus)
      size = bdd_size_multiple(info->bwdClusteredRelationArray);
    arrayForEachItem(bdd_t *, constrainArray, i, constrain) {
      if (bdd_is_tautology(constrain, 1))
        continue;

      arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, j, relation) {
        simplifiedRelation = Img_MinimizeImage(relation, constrain,
                                                 minimizeMethod, TRUE);
        if (printStatus == 2) {
          (void) fprintf(vis_stdout,
            "IMG Info: minimized bwd relation %d | %d => %d in component %d\n",
                         bdd_size(relation), bdd_size(constrain),
                         bdd_size(simplifiedRelation), j);
        }
        mdd_free(relation);
        array_insert(bdd_t*, info->bwdClusteredRelationArray, j,
                     simplifiedRelation);
      }
    }
    if (printStatus) {
      (void) fprintf(vis_stdout,
     "IMG Info: minimized bwd relation [%d | %ld => %ld] with %d components\n",
                     size, sizeConstrain,
                     bdd_size_multiple(info->bwdClusteredRelationArray),
                     array_n(info->bwdClusteredRelationArray));
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgReplaceIthTransitionFunction ( void *  methodData,
int  i,
mdd_t *  function,
Img_DirectionType  directionType 
)

Function********************************************************************

Synopsis [Replace ith transition function.]

Description [Replace ith transition function.]

SideEffects []

Definition at line 1826 of file imgTfm.c.

{
  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
  array_t               *relationArray;
  ImgComponent_t        *comp;
  mdd_t                 *old;

  if (info->vector) {
    comp = array_fetch(ImgComponent_t *, info->vector, i);
    mdd_free(comp->func);
    comp->func = function;
    ImgSupportClear(info, comp->support);
    ImgComponentGetSupport(comp);
    return;
  }

  if (directionType == Img_Forward_c)
    relationArray = info->fwdClusteredRelationArray;
  else
    relationArray = info->bwdClusteredRelationArray;

  old = array_fetch(mdd_t *, relationArray, i);
  mdd_free(old);
  array_insert(mdd_t *, relationArray, i, function);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgRestoreTransitionFunction ( Img_ImageInfo_t *  imageInfo,
Img_DirectionType  directionType 
)

Function********************************************************************

Synopsis [Restores original transition function from saved.]

Description [Restores original transition function from saved.]

SideEffects []

Definition at line 1141 of file imgTfm.c.

{
  ImgTfmInfo_t  *tfmInfo = (ImgTfmInfo_t *)imageInfo->methodData;

  if (tfmInfo->vector) {
    ImgVectorFree(tfmInfo->vector);
    tfmInfo->vector = (array_t *)imageInfo->savedRelation;
    imageInfo->savedRelation = NIL(void);
  }
  if (tfmInfo->fwdClusteredRelationArray) {
    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
      mdd_array_free(tfmInfo->fwdClusteredRelationArray);
      tfmInfo->fwdClusteredRelationArray = tfmInfo->fwdSavedRelation;
      tfmInfo->fwdSavedRelation = NIL(array_t);
    }
  }
  if (tfmInfo->bwdClusteredRelationArray) {
    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
      mdd_array_free(tfmInfo->bwdClusteredRelationArray);
      tfmInfo->bwdClusteredRelationArray = tfmInfo->bwdSavedRelation;
      tfmInfo->bwdSavedRelation = NIL(array_t);
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

ImgTfmOption_t* ImgTfmGetOptions ( Img_MethodType  method)

Function********************************************************************

Synopsis [Gets the necessary options for computing the image and returns in the option structure.]

Description [Gets the necessary options for computing the image and returns in the option structure.]

SideEffects []

Definition at line 1866 of file imgTfm.c.

{
  char                  *flagValue;
  ImgTfmOption_t        *option;

  option = ALLOC(ImgTfmOption_t, 1);
  memset(option, 0, sizeof(ImgTfmOption_t));

  option->debug = ReadSetBooleanValue("tfm_debug", FALSE);
  option->checkEquivalence = ReadSetBooleanValue("tfm_check_equivalence",
                                                 FALSE);
  option->writeSupportMatrix = ReadSetIntValue("tfm_write_support_matrix",
                                                0, 2, 0);
  option->writeSupportMatrixWithYvars =
    ReadSetBooleanValue("tfm_write_support_matrix_with_y", FALSE);
  option->writeSupportMatrixAndStop =
    ReadSetBooleanValue("tfm_write_support_matrix_and_stop", FALSE);
  option->writeSupportMatrixReverseRow =
    ReadSetBooleanValue("tfm_write_support_matrix_reverse_row", TRUE);
  option->writeSupportMatrixReverseCol =
    ReadSetBooleanValue("tfm_write_support_matrix_reverse_col", TRUE);

  option->verbosity = ReadSetIntValue("tfm_verbosity", 0, 2, 0);
  if (method == Img_Tfm_c)
    option->splitMethod = ReadSetIntValue("tfm_split_method", 0, 3, 0);
  else
    option->splitMethod = 3; /* the default value */
  option->inputSplit = ReadSetIntValue("tfm_input_split", 0, 3, 0);
  option->piSplitFlag = ReadSetBooleanValue("tfm_pi_split_flag", TRUE);
  if (method == Img_Tfm_c)
    option->rangeComp = ReadSetIntValue("tfm_range_comp", 0, 2, 1);
  else
    option->rangeComp = ReadSetIntValue("tfm_range_comp", 0, 2, 2);

  flagValue = Cmd_FlagReadByName("tfm_range_threshold");
  if (flagValue == NIL(char))
    option->rangeThreshold = 10; /* the default value */
  else
    option->rangeThreshold = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("tfm_range_try_threshold");
  if (flagValue == NIL(char))
    option->rangeTryThreshold = 2; /* the default value */
  else
    option->rangeTryThreshold = atoi(flagValue);

  option->rangeCheckReorder =
    ReadSetBooleanValue("tfm_range_check_reorder", FALSE);
  option->tieBreakMode = ReadSetIntValue("tfm_tie_break", 0, 1, 0);

  option->outputSplit = ReadSetIntValue("tfm_output_split", 0, 2, 0);

  flagValue = Cmd_FlagReadByName("tfm_turn_depth");
  if (flagValue == NIL(char)) {
    if (method == Img_Tfm_c)
      option->turnDepth = 5; /* the default for tfm */
    else
      option->turnDepth = -1; /* the default for hybrid */
  } else
    option->turnDepth = atoi(flagValue);

  option->findDecompVar = ReadSetBooleanValue("tfm_find_decomp_var", FALSE);
  option->globalCache = ReadSetBooleanValue("tfm_global_cache", TRUE);

  flagValue = Cmd_FlagReadByName("tfm_use_cache");
  if (flagValue == NIL(char)) {
    if (method == Img_Tfm_c)
      option->useCache = 1;
    else
      option->useCache = 0;
  } else
    option->useCache = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("tfm_max_chain_length");
  if (flagValue == NIL(char))
    option->maxChainLength = 2; /* the default value */
  else
    option->maxChainLength = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("tfm_init_cache_size");
  if (flagValue == NIL(char))
    option->initCacheSize = 1001; /* the default value */
  else
    option->initCacheSize = atoi(flagValue);

  option->autoFlushCache = ReadSetIntValue("tfm_auto_flush_cache", 0, 2, 1);
  if (method == Img_Tfm_c)
    option->sortVectorFlag = ReadSetBooleanValue("tfm_sort_vector", TRUE);
  else
    option->sortVectorFlag = ReadSetBooleanValue("tfm_sort_vector", FALSE);
  option->printStatistics = ReadSetBooleanValue("tfm_print_stats", FALSE);
  option->printBddSize = ReadSetBooleanValue("tfm_print_bdd_size", FALSE);

  flagValue = Cmd_FlagReadByName("tfm_max_essential_depth");
  if (flagValue == NIL(char))
    option->maxEssentialDepth = 5; /* the default value */
  else
    option->maxEssentialDepth = atoi(flagValue);

  option->findEssential = ReadSetIntValue("tfm_find_essential", 0, 2, 0);
  if (option->findEssential && bdd_get_package_name() != CUDD) {
    fprintf(vis_stderr,
            "** tfm error: tfm_find_essential is available for only CUDD.\n");
    option->findEssential = 0; 
  }
  option->printEssential = ReadSetIntValue("tfm_print_essential", 0, 2, 0);
  option->splitCubeFunc = ReadSetBooleanValue("tfm_split_cube_func", FALSE);
  option->composeIntermediateVars =
        ReadSetBooleanValue("tfm_compose_intermediate_vars", FALSE);

  if (method == Img_Tfm_c)
    option->preSplitMethod = ReadSetIntValue("tfm_pre_split_method", 0, 4, 0);
  else
    option->preSplitMethod = 4;
  option->preInputSplit = ReadSetIntValue("tfm_pre_input_split", 0, 3, 0);
  option->preOutputSplit = ReadSetIntValue("tfm_pre_output_split", 0, 2, 0);
  option->preDcLeafMethod = ReadSetIntValue("tfm_pre_dc_leaf_method", 0, 2, 0);
  option->preMinimize = ReadSetBooleanValue("tfm_pre_minimize", FALSE);

  option->trSplitMethod = ReadSetIntValue("hybrid_tr_split_method", 0, 1, 0);

  option->hybridMode = ReadSetIntValue("hybrid_mode", 0, 2, 1);
  option->buildPartialTR =
    ReadSetBooleanValue("hybrid_build_partial_tr", FALSE);

  flagValue = Cmd_FlagReadByName("hybrid_partial_num_vars");
  if (flagValue == NIL(char))
    option->nPartialVars = 8; /* the default value */
  else
    option->nPartialVars = atoi(flagValue);

  option->partialMethod = ReadSetIntValue("hybrid_partial_method", 0, 1, 0);

  option->delayedSplit = ReadSetBooleanValue("hybrid_delayed_split", FALSE);

  flagValue = Cmd_FlagReadByName("hybrid_split_min_depth");
  if (flagValue == NIL(char))
    option->splitMinDepth = 1; /* the default value */
  else
    option->splitMinDepth = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("hybrid_split_max_depth");
  if (flagValue == NIL(char))
    option->splitMaxDepth = 5; /* the default value */
  else
    option->splitMaxDepth = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("hybrid_pre_split_min_depth");
  if (flagValue == NIL(char))
    option->preSplitMinDepth = 0; /* the default value */
  else
    option->preSplitMinDepth = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("hybrid_pre_split_max_depth");
  if (flagValue == NIL(char))
    option->preSplitMaxDepth = 4; /* the default value */
  else
    option->preSplitMaxDepth = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("hybrid_lambda_threshold");
  if (flagValue == NIL(char))
    option->lambdaThreshold = 0.6; /* the default value */
  else
    sscanf(flagValue, "%f", &option->lambdaThreshold);

  flagValue = Cmd_FlagReadByName("hybrid_pre_lambda_threshold");
  if (flagValue == NIL(char))
    option->preLambdaThreshold = 0.65; /* the default value */
  else
    sscanf(flagValue, "%f", &option->preLambdaThreshold);

  flagValue = Cmd_FlagReadByName("hybrid_conjoin_vector_size");
  if (flagValue == NIL(char))
    option->conjoinVectorSize = 10; /* the default value */
  else
    option->conjoinVectorSize = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("hybrid_conjoin_relation_size");
  if (flagValue == NIL(char))
    option->conjoinRelationSize = 1; /* the default value */
  else
    option->conjoinRelationSize = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("hybrid_conjoin_relation_bdd_size");
  if (flagValue == NIL(char))
    option->conjoinRelationBddSize = 200; /* the default value */
  else
    option->conjoinRelationBddSize = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("hybrid_improve_lambda");
  if (flagValue == NIL(char))
    option->improveLambda = 0.1; /* the default value */
  else
    sscanf(flagValue, "%f", &option->improveLambda);

  flagValue = Cmd_FlagReadByName("hybrid_improve_vector_size");
  if (flagValue == NIL(char))
    option->improveVectorSize = 3; /* the default value */
  else
    option->improveVectorSize = atoi(flagValue);

  flagValue = Cmd_FlagReadByName("hybrid_improve_vector_bdd_size");
  if (flagValue == NIL(char))
    option->improveVectorBddSize = 30.0; /* the default value */
  else
    sscanf(flagValue, "%f", &option->improveVectorBddSize);

  option->decideMode = ReadSetIntValue("hybrid_decide_mode", 0, 3, 3);

  option->reorderWithFrom =
    ReadSetBooleanValue("hybrid_reorder_with_from", TRUE);
  option->preReorderWithFrom =
    ReadSetBooleanValue("hybrid_pre_reorder_with_from", FALSE);

  option->lambdaMode = ReadSetIntValue("hybrid_lambda_mode", 0, 2, 0);
  option->preLambdaMode = ReadSetIntValue("hybrid_pre_lambda_mode", 0, 3, 2);
  option->lambdaWithFrom = ReadSetBooleanValue("hybrid_lambda_with_from", TRUE);
  option->lambdaWithTr = ReadSetBooleanValue("hybrid_lambda_with_tr", TRUE);
  option->lambdaWithClustering =
    ReadSetBooleanValue("hybrid_lambda_with_clustering", FALSE);

  option->synchronizeTr = ReadSetBooleanValue("hybrid_synchronize_tr", FALSE);
  option->imgKeepPiInTr = ReadSetBooleanValue("hybrid_img_keep_pi", FALSE);
  option->preKeepPiInTr = ReadSetBooleanValue("hybrid_pre_keep_pi", FALSE);

  flagValue = Cmd_FlagReadByName("hybrid_tr_method");
  if (flagValue == NIL(char))
    option->trMethod = Img_Iwls95_c; /* the default value */
  else {
    if (strcmp(flagValue, "iwls95") == 0)
      option->trMethod = Img_Iwls95_c;
    else if (strcmp(flagValue, "mlp") == 0)
      option->trMethod = Img_Mlp_c;
    else {
      fprintf(vis_stderr,
                "** tfm error : invalid value %s for hybrid_tr_method\n",
                flagValue);
      option->trMethod = Img_Iwls95_c;
    }
  }
  option->preCanonical = ReadSetBooleanValue("hybrid_pre_canonical", FALSE);

  option->printLambda = ReadSetBooleanValue("hybrid_print_lambda", FALSE);

  return(option);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImgUpdateTransitionFunction ( void *  methodData,
array_t *  vector,
Img_DirectionType  directionType 
)

Function********************************************************************

Synopsis [Overwrites transition function with given.]

Description [Overwrites transition function with given.]

SideEffects []

Definition at line 1803 of file imgTfm.c.

{
  ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)methodData;
  if (tfmInfo->vector)
    tfmInfo->vector = vector;
  else if (directionType == Img_Forward_c)
    tfmInfo->fwdClusteredRelationArray = vector;
  else
    tfmInfo->bwdClusteredRelationArray = vector;
}

Here is the caller graph for this function:

static void MinimizeTransitionFunction ( array_t *  vector,
array_t *  relationArray,
mdd_t *  constrain,
Img_MinimizeType  minimizeMethod,
int  printStatus 
) [static]

Function********************************************************************

Synopsis [Minimizes function vector or relation with given constraint.]

Description [Minimizes function vector or relation with given constraint.]

SideEffects []

Definition at line 3606 of file imgTfm.c.

{
  int           i;
  bdd_t         *relation, *simplifiedRelation, *simplifiedFunc;
  long          sizeConstrain = 0, size = 0;
  ImgComponent_t *comp;

  if (bdd_is_tautology(constrain, 1))
    return;

  if (vector) {
    if (printStatus) {
      size = ImgVectorBddSize(vector);
      sizeConstrain = bdd_size(constrain);
    }

    arrayForEachItem(ImgComponent_t *, vector, i, comp) {
      simplifiedFunc = Img_MinimizeImage(comp->func, constrain, minimizeMethod,
                                         TRUE);
      if (printStatus == 2) {
        (void)fprintf(vis_stdout,
            "IMG Info: minimized function %d | %ld => %d in component %d\n",
                      bdd_size(comp->func), sizeConstrain,
                      bdd_size(simplifiedFunc), i);
      }
      mdd_free(comp->func);
      comp->func = simplifiedFunc;
    }

    if (printStatus) {
      (void) fprintf(vis_stdout,
       "IMG Info: minimized function [%ld | %ld => %ld] with %d components\n",
                     size, sizeConstrain,
                     ImgVectorBddSize(vector), array_n(vector));
    }
  }

  if (relationArray) {
    if (printStatus) {
      size = bdd_size_multiple(relationArray);
      sizeConstrain = bdd_size(constrain);
    }

    arrayForEachItem(bdd_t*, relationArray, i, relation) {
      simplifiedRelation = Img_MinimizeImage(relation, constrain,
                                             minimizeMethod, TRUE);
      if (printStatus == 2) {
        (void)fprintf(vis_stdout,
                "IMG Info: minimized relation %d | %ld => %d in component %d\n",
                      bdd_size(relation), sizeConstrain,
                      bdd_size(simplifiedRelation), i);
      }
      mdd_free(relation);
      array_insert(bdd_t *, relationArray, i, simplifiedRelation);
    }

    if (printStatus) {
      (void) fprintf(vis_stdout,
       "IMG Info: minimized relation [%ld | %ld => %ld] with %d components\n",
                     size, sizeConstrain,
                     bdd_size_multiple(relationArray), array_n(relationArray));
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void PrintFoundVariableStatistics ( ImgTfmInfo_t *  info,
int  preFlag 
) [static]

Function********************************************************************

Synopsis [Prints statistics of finding essential and dependent variables.]

Description [Prints statistics of finding essential and dependent variables.]

SideEffects []

SeeAlso []

Definition at line 2562 of file imgTfm.c.

{
  int   i, maxDepth;

  if (preFlag) {
    fprintf(vis_stdout, "# split = %d, conjoin = %d\n",
            info->nSplitsB, info->nConjoinsB);
    return;
  }

  fprintf(vis_stdout,
    "# found essential vars = %d (top = %d, average = %g, averageDepth = %g)\n",
          info->nFoundEssentials, info->topFoundEssentialDepth,
          info->averageFoundEssential, info->averageFoundEssentialDepth);
  if (info->option->printEssential == 1) {
    maxDepth = info->maxDepth < IMG_TF_MAX_PRINT_DEPTH ?
                info->maxDepth : IMG_TF_MAX_PRINT_DEPTH;
    fprintf(vis_stdout, "foundEssential:");
    for (i = 0; i < maxDepth; i++)
      fprintf(vis_stdout, " [%d]%d", i, info->foundEssentials[i]);
    fprintf(vis_stdout, "\n");
  }
  if (info->useConstraint == 2)
    fprintf(vis_stdout, "# range computations = %d\n", info->nRangeComps);
  fprintf(vis_stdout,
          "# found dependent vars = %d (average = %g)\n",
          info->nFoundDependVars, info->averageFoundDependVars);
  fprintf(vis_stdout, "# tautologous subimage = %d\n", info->nEmptySubImage);
  fprintf(vis_stdout, "# split = %d, conjoin = %d, cubeSplit = %d\n",
          info->nSplits, info->nConjoins, info->nCubeSplits);
}

Here is the caller graph for this function:

static void PrintRecursionStatistics ( ImgTfmInfo_t *  info,
int  preFlag 
) [static]

Function********************************************************************

Synopsis [Prints statistics of recursions for transition function method.]

Description [Prints statistics of recursions for transition function method.]

SideEffects []

SeeAlso []

Definition at line 2526 of file imgTfm.c.

{
  float avgDepth, avgDecomp;
  int   nRecurs, nLeaves, nTurns, nDecomps, topDecomp, maxDecomp, maxDepth;

  GetRecursionStatistics(info, preFlag, &nRecurs, &nLeaves, &nTurns, &avgDepth,
                 &maxDepth, &nDecomps, &topDecomp, &maxDecomp, &avgDecomp);
  if (preFlag)
    fprintf(vis_stdout, "** recursion statistics of splitting (preImg) **\n");
  else
    fprintf(vis_stdout, "** recursion statistics of splitting (img) **\n");
  fprintf(vis_stdout, "# recursions = %d\n", nRecurs);
  fprintf(vis_stdout, "# leaves = %d\n", nLeaves);
  fprintf(vis_stdout, "# turns = %d\n", nTurns);
  fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n",
          avgDepth, maxDepth);
  if (!preFlag) {
    fprintf(vis_stdout,
            "# decompositions = %d (top = %d, max = %d, average = %g)\n",
            nDecomps, topDecomp, maxDecomp, avgDecomp);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

static boolean ReadSetBooleanValue ( char *  string,
boolean  defaultValue 
) [static]

Function********************************************************************

Synopsis [Reads a set Boolean value.]

Description [Reads a set Boolean value.]

SideEffects []

SeeAlso []

Definition at line 2684 of file imgTfm.c.

{
  char          *flagValue;
  boolean       value = defaultValue;

  flagValue = Cmd_FlagReadByName(string);
  if (flagValue != NIL(char)) {
    if (strcmp(flagValue, "yes") == 0)
      value = TRUE;
    else if (strcmp(flagValue, "no") == 0)
      value = FALSE;
    else {
      fprintf(vis_stderr,
              "** tfm error: invalid value %s for %s[yes/no]. **\n",
              flagValue, string);
    }
  }

  return(value);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static int ReadSetIntValue ( char *  string,
int  l,
int  u,
int  defaultValue 
) [static]

Function********************************************************************

Synopsis [Reads a set integer value.]

Description [Reads a set integer value.]

SideEffects []

SeeAlso []

Definition at line 2650 of file imgTfm.c.

{
  char  *flagValue;
  int   tmp;
  int   value = defaultValue;

  flagValue = Cmd_FlagReadByName(string);
  if (flagValue != NIL(char)) {
    sscanf(flagValue, "%d", &tmp);
    if (tmp >= l && (tmp <= u || u == 0))
      value = tmp;
    else {
      fprintf(vis_stderr,
        "** tfm error: invalid value %d for %s[%d-%d]. **\n", tmp, string,
              l, u);
    }
  }

  return(value);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void RebuildTransitionRelation ( ImgTfmInfo_t *  info,
Img_DirectionType  directionType 
) [static]

Function********************************************************************

Synopsis [Rebuilds transition relation from function vector.]

Description [Rebuilds transition relation from function vector.]

SideEffects []

SeeAlso []

Definition at line 3517 of file imgTfm.c.

{
  int                   i;
  mdd_t                 *var, *relation;
  ImgComponent_t        *comp;
  array_t               *relationArray;
  array_t               *quantifyVarBddArray, *domainVarBddArray;

  relationArray = array_alloc(mdd_t *, 0);

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

  if (directionType == Img_Forward_c || directionType == Img_Both_c) {
    mdd_array_free(info->fwdClusteredRelationArray);
    if (info->imgKeepPiInTr) {
      if (info->intermediateBddVars)
        quantifyVarBddArray = info->intermediateBddVars;
      else
        quantifyVarBddArray = array_alloc(mdd_t *, 0);
      domainVarBddArray = array_join(info->domainVarBddArray,
                                     info->quantifyVarBddArray);
    } else {
      if (info->newQuantifyBddVars)
        quantifyVarBddArray = info->newQuantifyBddVars;
      else
        quantifyVarBddArray = info->quantifyVarBddArray;
      domainVarBddArray = info->domainVarBddArray;
    }
    info->fwdClusteredRelationArray = ImgClusterRelationArray(
        info->manager, info->functionData, info->option->trMethod,
        Img_Forward_c, info->trmOption, relationArray,
        domainVarBddArray, quantifyVarBddArray,
        info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray,
        &info->fwdSmoothVarCubeArray, 0);
    if (info->imgKeepPiInTr) {
      if (!info->intermediateBddVars)
        array_free(quantifyVarBddArray);
      array_free(domainVarBddArray);
    }
  }
  if (directionType == Img_Backward_c || directionType == Img_Both_c) {
    mdd_array_free(info->bwdClusteredRelationArray);
    if (info->preKeepPiInTr) {
      if (info->intermediateBddVars)
        quantifyVarBddArray = info->intermediateBddVars;
      else
        quantifyVarBddArray = array_alloc(mdd_t *, 0);
      domainVarBddArray = array_join(info->domainVarBddArray,
                                     info->quantifyVarBddArray);
    } else {
      if (info->newQuantifyBddVars)
        quantifyVarBddArray = info->newQuantifyBddVars;
      else
        quantifyVarBddArray = info->quantifyVarBddArray;
      domainVarBddArray = info->domainVarBddArray;
    }
    info->bwdClusteredRelationArray = ImgClusterRelationArray(
            info->manager, info->functionData,
            info->option->trMethod, Img_Backward_c, info->trmOption,
            relationArray, domainVarBddArray, quantifyVarBddArray,
            info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray,
            &info->fwdSmoothVarCubeArray, 0);
    if (info->preKeepPiInTr) {
      if (!info->intermediateBddVars)
        array_free(quantifyVarBddArray);
      array_free(domainVarBddArray);
    }
  }

  mdd_array_free(relationArray);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void TfmBuildRelationArray ( ImgTfmInfo_t *  info,
ImgFunctionData_t *  functionData,
array_t *  bitRelationArray,
Img_DirectionType  directionType,
int  writeMatrix 
) [static]

Function********************************************************************

Synopsis [Builds relation array from function vector or bit relation.]

Description [Builds relation array from function vector or bit relation.]

SideEffects []

SeeAlso [ImgImageInfoInitializeTfm]

Definition at line 3244 of file imgTfm.c.

{
  int                   i;
  mdd_t                 *var, *relation;
  array_t               *relationArray;
  ImgComponent_t        *comp;
  int                   id;
  array_t               *domainVarBddArray, *quantifyVarBddArray;
  mdd_t                 *one, *res1, *res2;
  char                  filename[20];
  int                   composeIntermediateVars, findIntermediateVars;

  if ((info->buildTR == 1 && info->option->synchronizeTr) ||
        info->buildPartialTR) {
    relationArray = array_alloc(mdd_t *, 0);
    if (info->fullVector) {
      for (i = 0; i < array_n(info->fullVector); i++) {
        comp = array_fetch(ImgComponent_t *, info->fullVector, i);
        id = (int)bdd_top_var_id(comp->var);
        if (!info->partialVarFlag[id]) {
          if (comp->intermediate)
            relation = mdd_xnor(comp->var, comp->func);
          else {
            var = ImgSubstitute(comp->var, functionData, Img_D2R_c);
            relation = mdd_xnor(var, comp->func);
            mdd_free(var);
          }
          array_insert_last(mdd_t *, relationArray, relation);
        }
      }
    } else {
      for (i = 0; i < array_n(info->vector); i++) {
        comp = array_fetch(ImgComponent_t *, info->vector, i);
        if (comp->intermediate)
          relation = mdd_xnor(comp->var, comp->func);
        else {
          var = ImgSubstitute(comp->var, functionData, Img_D2R_c);
          relation = mdd_xnor(var, comp->func);
          mdd_free(var);
        }
        array_insert_last(mdd_t *, relationArray, relation);
      }
    }

    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
      if (info->imgKeepPiInTr) {
        if (info->intermediateBddVars)
          quantifyVarBddArray = info->intermediateBddVars;
        else
          quantifyVarBddArray = array_alloc(mdd_t *, 0);
        domainVarBddArray = array_join(info->domainVarBddArray,
                                        info->quantifyVarBddArray);
      } else {
        if (info->newQuantifyBddVars)
          quantifyVarBddArray = info->newQuantifyBddVars;
        else
          quantifyVarBddArray = info->quantifyVarBddArray;
        domainVarBddArray = info->domainVarBddArray;
      }
      info->fwdClusteredRelationArray = ImgClusterRelationArray(
        info->manager, info->functionData,
        info->option->trMethod, Img_Forward_c, info->trmOption,
        relationArray, domainVarBddArray, quantifyVarBddArray,
        info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray,
        &info->fwdSmoothVarCubeArray, 0);
      if (writeMatrix && info->option->writeSupportMatrix == 3) {
        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
        ImgWriteSupportMatrix(info, info->vector,
                                info->fwdClusteredRelationArray, filename);
      } else if (writeMatrix && info->option->writeSupportMatrix == 2) {
        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
        ImgWriteSupportMatrix(info, NIL(array_t),
                                info->fwdClusteredRelationArray, filename);
      }
      if (info->imgKeepPiInTr) {
        if (!info->intermediateBddVars)
          array_free(quantifyVarBddArray);
        array_free(domainVarBddArray);
      }
      if (info->option->checkEquivalence && (!info->fullVector)) {
        assert(ImgCheckEquivalence(info, info->vector,
                                   info->fwdClusteredRelationArray,
                                   NIL(mdd_t), NIL(mdd_t), 0));
      }
      if (info->option->debug) {
        one = mdd_one(info->manager);
        if (info->fullVector) {
          res1 = ImgImageByHybrid(info, info->fullVector, one);
          res2 = ImgImageByHybridWithStaticSplit(info, info->vector, one,
                                        info->fwdClusteredRelationArray,
                                        NIL(mdd_t), NIL(mdd_t));
        } else {
          res1 = ImgImageByHybrid(info, info->vector, one);
          res2 = ImgImageByHybridWithStaticSplit(info, NIL(array_t), one,
                                        info->fwdClusteredRelationArray,
                                        NIL(mdd_t), NIL(mdd_t));
        }
        assert(mdd_equal(res1, res2));
        mdd_free(one);
        mdd_free(res1);
        mdd_free(res2);
      }
    }
    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
      if (info->preKeepPiInTr) {
        if (info->intermediateBddVars)
          quantifyVarBddArray = info->intermediateBddVars;
        else
          quantifyVarBddArray = array_alloc(mdd_t *, 0);
        domainVarBddArray = array_join(info->domainVarBddArray,
                                        info->quantifyVarBddArray);
      } else {
        if (info->newQuantifyBddVars)
          quantifyVarBddArray = info->newQuantifyBddVars;
        else
          quantifyVarBddArray = info->quantifyVarBddArray;
        domainVarBddArray = info->domainVarBddArray;
      }
      info->bwdClusteredRelationArray = ImgClusterRelationArray(
        info->manager, info->functionData,
        info->option->trMethod, Img_Backward_c, info->trmOption,
        relationArray, domainVarBddArray, quantifyVarBddArray,
        info->rangeVarBddArray, &info->bwdArraySmoothVarBddArray,
        &info->bwdSmoothVarCubeArray, 0);
      if (writeMatrix && info->option->writeSupportMatrix == 3) {
        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
        ImgWriteSupportMatrix(info, info->vector,
                                info->bwdClusteredRelationArray, filename);
      } else if (writeMatrix && info->option->writeSupportMatrix == 2) {
        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
        ImgWriteSupportMatrix(info, NIL(array_t),
                                info->bwdClusteredRelationArray, filename);
      }
      if (info->preKeepPiInTr) {
        if (!info->intermediateBddVars)
          array_free(quantifyVarBddArray);
        array_free(domainVarBddArray);
      }
      if (info->option->checkEquivalence && (!info->fullVector)) {
        assert(ImgCheckEquivalence(info, info->vector,
                                   info->bwdClusteredRelationArray,
                                   NIL(mdd_t), NIL(mdd_t), 1));
      }
      if (info->option->debug) {
        one = mdd_one(info->manager);
        if (info->fullVector) {
          res1 = ImgImageByHybrid(info, info->fullVector, one);
          res2 = ImgImageByHybridWithStaticSplit(info, info->vector, one,
                                        info->bwdClusteredRelationArray,
                                        NIL(mdd_t), NIL(mdd_t));
        } else {
          res1 = ImgImageByHybrid(info, info->vector, one);
          res2 = ImgImageByHybridWithStaticSplit(info, NIL(array_t), one,
                                        info->bwdClusteredRelationArray,
                                        NIL(mdd_t), NIL(mdd_t));
        }
        assert(mdd_equal(res1, res2));
        mdd_free(one);
        mdd_free(res1);
        mdd_free(res2);
      }
    }

    mdd_array_free(relationArray);
  } else {
    graph_t     *mddNetwork = functionData->mddNetwork;

    if (bitRelationArray)
      relationArray = bitRelationArray;
    else {
      if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c &&
          info->nVars != info->nRealVars) {
        if (info->option->composeIntermediateVars) {
          composeIntermediateVars = 1;
          findIntermediateVars = 0;
        } else {
          composeIntermediateVars = 0;
          findIntermediateVars = 1;
        }
      } else {
        composeIntermediateVars = 0;
        findIntermediateVars = 0;
      }

      relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars,
                                                findIntermediateVars);
    }

    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
      if (info->imgKeepPiInTr) {
        if (info->intermediateBddVars)
          quantifyVarBddArray = info->intermediateBddVars;
        else
          quantifyVarBddArray = array_alloc(mdd_t *, 0);
        domainVarBddArray = array_join(info->domainVarBddArray,
                                        info->quantifyVarBddArray);
      } else {
        if (info->newQuantifyBddVars)
          quantifyVarBddArray = info->newQuantifyBddVars;
        else
          quantifyVarBddArray = info->quantifyVarBddArray;
        domainVarBddArray = info->domainVarBddArray;
      }
      info->fwdClusteredRelationArray = ImgClusterRelationArray(
                info->manager, info->functionData, info->option->trMethod,
                Img_Forward_c, info->trmOption, relationArray,
                domainVarBddArray, quantifyVarBddArray,
                info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray,
                &info->fwdSmoothVarCubeArray, 0);
      if (writeMatrix && info->option->writeSupportMatrix >= 2) {
        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
        ImgWriteSupportMatrix(info, NIL(array_t),
                                info->fwdClusteredRelationArray, filename);
      }
      if (info->imgKeepPiInTr) {
        if (!info->intermediateBddVars)
          array_free(quantifyVarBddArray);
        array_free(domainVarBddArray);
      }
    }
    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
      if (info->preKeepPiInTr) {
        if (info->intermediateBddVars)
          quantifyVarBddArray = info->intermediateBddVars;
        else
          quantifyVarBddArray = array_alloc(mdd_t *, 0);
        domainVarBddArray = array_join(info->domainVarBddArray,
                                        info->quantifyVarBddArray);
      } else {
        if (info->newQuantifyBddVars)
          quantifyVarBddArray = info->newQuantifyBddVars;
        else
          quantifyVarBddArray = info->quantifyVarBddArray;
        domainVarBddArray = info->domainVarBddArray;
      }
      info->bwdClusteredRelationArray = ImgClusterRelationArray(
        info->manager, info->functionData,
        info->option->trMethod, Img_Backward_c, info->trmOption,
        relationArray, domainVarBddArray, quantifyVarBddArray,
        info->rangeVarBddArray, &info->bwdArraySmoothVarBddArray,
        &info->bwdSmoothVarCubeArray, 0);
      if (writeMatrix && info->option->writeSupportMatrix >= 2) {
        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
        ImgWriteSupportMatrix(info, NIL(array_t),
                                info->bwdClusteredRelationArray, filename);
      }
      if (info->preKeepPiInTr) {
        if (!info->intermediateBddVars)
          array_free(quantifyVarBddArray);
        array_free(domainVarBddArray);
      }
    }

    if (!bitRelationArray)
      mdd_array_free(relationArray);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

static array_t * TfmCreateBitRelationArray ( ImgTfmInfo_t *  info,
int  composeIntermediateVars,
int  findIntermediateVars 
) [static]

Function********************************************************************

Synopsis [Creates the bit relations.]

Description [Creates the bit relations.]

SideEffects []

SeeAlso [ImgImageInfoInitializeTfm]

Definition at line 3054 of file imgTfm.c.

{
  array_t               *bddRelationArray = array_alloc(mdd_t*, 0);
  ImgFunctionData_t     *functionData = info->functionData;
  array_t               *domainVarMddIdArray = functionData->domainVars;
  array_t               *rangeVarMddIdArray = functionData->rangeVars;
  array_t               *quantifyVarMddIdArray = functionData->quantifyVars;
  graph_t               *mddNetwork = functionData->mddNetwork;
  array_t               *roots = functionData->roots;
  int                   i, j, n1, n2, mddId, nIntermediateVars = 0;
  mdd_manager           *mddManager = Part_PartitionReadMddManager(mddNetwork);
  st_table              *vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table              *domainQuantifyVarMddIdTable =
                                st_init_table(st_numcmp, st_numhash);
  char                  *nodeName;
  mdd_t                 *relation, *composedRelation;
  array_t               *intermediateVarMddIdArray, *intermediateBddVars;
  int                   index;
  mdd_t                 *var;

  if (findIntermediateVars)
    intermediateVarMddIdArray = array_alloc(int, 0);
  else
    intermediateVarMddIdArray = NIL(array_t);

  arrayForEachItem(int, domainVarMddIdArray, i, mddId) {
    st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
  }
  arrayForEachItem(int, quantifyVarMddIdArray, i, mddId) {
    st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
  }
  
  arrayForEachItem(char *, roots, i, nodeName) {
    vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName);
    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
    int mddId = array_fetch(int, rangeVarMddIdArray, i);
    
    array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager,
                                                                 mddId, mvf);
    if (composeIntermediateVars) {
      for (j = 0; j < array_n(varBddRelationArray); j++) {
        relation = array_fetch(mdd_t *, varBddRelationArray, j);
        composedRelation = Img_ComposeIntermediateNodes(
                functionData->mddNetwork, relation, functionData->domainVars,
                functionData->rangeVars, functionData->quantifyVars);
        mdd_free(relation);
        array_insert(mdd_t *, varBddRelationArray, j, composedRelation);
      }

      array_append(bddRelationArray, varBddRelationArray);
      array_free(varBddRelationArray);
    } else {
      array_append(bddRelationArray, varBddRelationArray);
      array_free(varBddRelationArray);

      if (findIntermediateVars) {
        if (info->option->verbosity)
          n1 = array_n(bddRelationArray);
        GetIntermediateRelationsRecursively(mddManager, vertex, -1, vertexTable,
                                            bddRelationArray,
                                            domainQuantifyVarMddIdTable,
                                            intermediateVarMddIdArray);
        if (info->option->verbosity) {
          n2 = array_n(bddRelationArray);
          nIntermediateVars += n2 - n1;
        }
      }
    }
  }

  st_free_table(vertexTable);
  st_free_table(domainQuantifyVarMddIdTable);
  if (findIntermediateVars) {
    int nonExistFlag;

    /* checks whether intermediate variables are already found */
    if (info->intermediateVarsTable && info->intermediateBddVars &&
        info->newQuantifyBddVars) {
      nonExistFlag = 0;
    } else {
      assert(!info->intermediateVarsTable);
      assert(!info->intermediateBddVars);
      assert(!info->newQuantifyBddVars);
      nonExistFlag = 1;
    }

    if (info->option->verbosity) {
      (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n",
              info->nIntermediateVars);
    }
    if (nonExistFlag) {
      intermediateBddVars = mdd_id_array_to_bdd_array(mddManager,
                                                intermediateVarMddIdArray);
    } else
      intermediateBddVars = NIL(array_t);
    array_free(intermediateVarMddIdArray);
    if (nonExistFlag) {
      info->intermediateVarsTable = st_init_table(st_numcmp, st_numhash);
      for (i = 0; i < array_n(intermediateBddVars); i++) {
        var = array_fetch(mdd_t *, intermediateBddVars, i);
        index = (int)bdd_top_var_id(var);
        st_insert(info->intermediateVarsTable, (char *)(long)index, NIL(char));
      }
      info->newQuantifyBddVars = mdd_array_duplicate(
                                        functionData->quantifyBddVars);
      for (i = 0; i < array_n(intermediateBddVars); i++) {
        var = array_fetch(mdd_t *, intermediateBddVars, i);
        array_insert_last(mdd_t *, info->newQuantifyBddVars, mdd_dup(var));
      }
      info->intermediateBddVars = intermediateBddVars;
    }
  }
  return(bddRelationArray);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static array_t * TfmCreateBitVector ( ImgTfmInfo_t *  info,
int  composeIntermediateVars,
int  findIntermediateVars 
) [static]

Function********************************************************************

Synopsis [Creates function vector.]

Description [Creates function vector.]

SideEffects []

SeeAlso [ImgImageInfoInitializeTfm]

Definition at line 2876 of file imgTfm.c.

{
  int                   i, j;
  array_t               *vector;
  graph_t               *mddNetwork;
  mdd_manager           *mddManager;
  array_t               *roots;
  array_t               *rangeVarMddIdArray;
  int                   index;
  mdd_t                 *var;
  ImgComponent_t        *comp;
  st_table              *vertexTable;
  st_table              *domainQuantifyVarMddIdTable;
  array_t               *intermediateVarMddIdArray, *intermediateBddVars;
  int                   mddId;
  ImgFunctionData_t     *functionData = info->functionData;

  mddNetwork = functionData->mddNetwork;
  mddManager = Part_PartitionReadMddManager(mddNetwork);
  roots = functionData->roots;
  rangeVarMddIdArray = functionData->rangeVars;

  if (findIntermediateVars) {
    vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
    domainQuantifyVarMddIdTable = st_init_table(st_numcmp, st_numhash);
    intermediateVarMddIdArray = array_alloc(int, 0);
    arrayForEachItem(int, functionData->domainVars, i, mddId) {
      st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
    }
    arrayForEachItem(int, functionData->quantifyVars, i, mddId) {
      st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
    }
  } else {
    vertexTable = NIL(st_table);
    domainQuantifyVarMddIdTable = NIL(st_table);
    intermediateVarMddIdArray = NIL(array_t);
  }

  vector = array_alloc(ImgComponent_t *, 0);
  /*
   * Iterate over the function of all the root nodes.
   */
  for (i = 0; i < array_n(roots); i++) {
    mdd_t *func;
    char *nodeName = array_fetch(char*, roots, i);
    vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName);
    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
    int mddId = array_fetch(int, rangeVarMddIdArray, i);
    array_t *varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager,
                                                                mddId, mvf);
    array_t *bddArray = mdd_id_to_bdd_array(mddManager, mddId);

    assert(array_n(varBddFunctionArray) == array_n(bddArray));
    if (info->option->debug) {
      mdd_t *rel1, *rel2;
      array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager,
                                                                   mddId,
                                                                   mvf);
      for (j = 0; j < array_n(bddArray); j++) {
        var = array_fetch(mdd_t *, bddArray, j);
        func = array_fetch(mdd_t *, varBddFunctionArray, j);
        rel1 = array_fetch(mdd_t *, varBddRelationArray, j);
        rel2 = mdd_xnor(var, func);
        if (!mdd_equal(rel1, rel2)) {
          if (mdd_lequal(rel1, rel2, 1, 1))
            fprintf(vis_stdout, "** %d(%d): rel < funcRel\n", i, j);
          else if (mdd_lequal(rel2, rel1, 1, 1))
            fprintf(vis_stdout, "** %d(%d): rel > funcRel\n", i, j);
          else
            fprintf(vis_stdout, "** %d(%d): rel != funcRel\n", i, j);
        }
        mdd_free(rel1);
        mdd_free(rel2);
      }

      array_free(varBddRelationArray);
    }
    for (j = 0; j < array_n(bddArray); j++) {
      var = array_fetch(mdd_t *, bddArray, j);
      func = array_fetch(mdd_t *, varBddFunctionArray, j);
      if (array_n(bddArray) == 1 && bdd_is_tautology(func, 1)) {
        array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager,
                                                                mddId, mvf);
        mdd_t *relation = array_fetch(mdd_t *, varBddRelationArray, 0);
        /* non-deterministic constant */
        if (bdd_is_tautology(relation, 1)) {
          mdd_array_free(varBddRelationArray);
          mdd_free(func);
          break;
        }
        mdd_array_free(varBddRelationArray);
      }
      comp = ImgComponentAlloc(info);
      comp->var = ImgSubstitute(var, functionData, Img_R2D_c);
      if (composeIntermediateVars) {
        comp->func = Img_ComposeIntermediateNodes(functionData->mddNetwork,
                  func, functionData->domainVars, functionData->rangeVars,
                  functionData->quantifyVars);
        mdd_free(func);
      } else
        comp->func = func;
      ImgComponentGetSupport(comp);
      array_insert_last(ImgComponent_t *, vector, comp);
    }
    if (findIntermediateVars) {
      int       n1, n2;

      n1 = array_n(vector);
      FindIntermediateVarsRecursively(info, mddManager, vertex, -1,
                                        vertexTable, vector,
                                        domainQuantifyVarMddIdTable,
                                        intermediateVarMddIdArray);
      n2 = array_n(vector);
      info->nIntermediateVars += n2 - n1;
    }
    array_free(varBddFunctionArray);
    mdd_array_free(bddArray);
  }
  if (findIntermediateVars) {
    int nonExistFlag;

    /* checks whether intermediate variables are already found */
    if (info->intermediateVarsTable && info->intermediateBddVars &&
        info->newQuantifyBddVars) {
      nonExistFlag = 0;
    } else {
      assert(!info->intermediateVarsTable);
      assert(!info->intermediateBddVars);
      assert(!info->newQuantifyBddVars);
      nonExistFlag = 1;
    }

    if (info->option->verbosity) {
      (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n",
              info->nIntermediateVars);
    }
    st_free_table(vertexTable);
    st_free_table(domainQuantifyVarMddIdTable);
    if (nonExistFlag) {
      intermediateBddVars = mdd_id_array_to_bdd_array(mddManager,
                                                intermediateVarMddIdArray);
    } else
      intermediateBddVars = NIL(array_t);
    array_free(intermediateVarMddIdArray);
    if (nonExistFlag) {
      info->intermediateVarsTable = st_init_table(st_numcmp, st_numhash);
      for (i = 0; i < array_n(intermediateBddVars); i++) {
        var = array_fetch(mdd_t *, intermediateBddVars, i);
        index = (int)bdd_top_var_id(var);
        st_insert(info->intermediateVarsTable, (char *)(long)index, NIL(char));
      }
      info->newQuantifyBddVars = mdd_array_duplicate(
                                        functionData->quantifyBddVars);
      for (i = 0; i < array_n(intermediateBddVars); i++) {
        var = array_fetch(mdd_t *, intermediateBddVars, i);
        array_insert_last(mdd_t *, info->newQuantifyBddVars, mdd_dup(var));
      }
      info->intermediateBddVars = intermediateBddVars;
    }
  }

  return(vector);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static ImgTfmInfo_t * TfmInfoStructAlloc ( Img_MethodType  method) [static]

AutomaticStart

Function********************************************************************

Synopsis [Allocates and initializes the info structure for transition function method.]

Description [Allocates and initializes the info structure for transition function method.]

SideEffects []

Definition at line 2330 of file imgTfm.c.

{
  ImgTfmInfo_t  *info;

  info = ALLOC(ImgTfmInfo_t, 1);
  memset(info, 0, sizeof(ImgTfmInfo_t));
  info->method = method;
  info->option = ImgTfmGetOptions(method);
  return(info);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void TfmSetupPartialTransitionRelation ( ImgTfmInfo_t *  info,
array_t **  partialRelationArray 
) [static]

Function********************************************************************

Synopsis [Builds partial vector and relation array.]

Description [Builds partial vector and relation array.]

SideEffects []

SeeAlso [ImgImageInfoInitializeTfm]

Definition at line 3183 of file imgTfm.c.

{
  int                   i, id;
  mdd_t                 *var, *relation;
  ImgComponent_t        *comp, *newComp;
  array_t               *partialVector;
  ImgFunctionData_t     *functionData = info->functionData;

  if (!info->buildPartialTR)
    return;

  info->partialBddVars = ChoosePartialVars(info, info->fullVector,
                                           info->option->nPartialVars,
                                           info->option->partialMethod);
  info->partialVarFlag = ALLOC(char, info->nVars);
  memset(info->partialVarFlag, 0, sizeof(char) * info->nVars);
  for (i = 0; i < array_n(info->partialBddVars); i++) {
    var = array_fetch(mdd_t *, info->partialBddVars, i);
    id = (int)bdd_top_var_id(var);
    info->partialVarFlag[id] = 1;
  }

  partialVector = array_alloc(ImgComponent_t *, 0);
  if (partialRelationArray)
    *partialRelationArray = array_alloc(mdd_t *, 0);

  for (i = 0; i < array_n(info->fullVector); i++) {
    comp = array_fetch(ImgComponent_t *, info->fullVector, i);
    id = (int)bdd_top_var_id(comp->var);
    if (info->partialVarFlag[id]) {
      newComp = ImgComponentCopy(info, comp);
      array_insert_last(ImgComponent_t *, partialVector, newComp);

      if (newComp->intermediate)
        relation = mdd_xnor(newComp->var, newComp->func);
      else {
        var = ImgSubstitute(newComp->var, functionData, Img_D2R_c);
        relation = mdd_xnor(var, newComp->func);
        mdd_free(var);
      }
      array_insert_last(mdd_t *, *partialRelationArray, relation);
    }
  }

  info->vector = partialVector;
}

Here is the call graph for this function:

Here is the caller graph for this function:


Variable Documentation

st_table* HookInfoList [static]

Definition at line 95 of file imgTfm.c.

int nHookInfoList [static]

Definition at line 97 of file imgTfm.c.

char rcsid [] UNUSED = "$Id: imgTfm.c,v 1.93 2005/04/23 14:30:54 jinh Exp $" [static]

CFile***********************************************************************

FileName [imgTfm.c]

PackageName [img]

Synopsis [Routines for image and preimage computations using transition function method.]

Description [Transition function method is implemented as a part of the hybrid image computation (refer to "To Split or to Conjoin: The Question in Image Computation", In-Ho Moon et. al. in the proceedings of DAC00.) The hybrid method starts with transition function method based on splitting, then switches to transition relation method based on conjunctions. The decision is based on computing variable lifetimes from dependence matrix dynamically at every recursion.

The transition function method itself also can be used as an image_method, however we do not recommend to use this method for general purpose. This method can be used for experimental purpose. However, this method performs quite well for most approximate reachability and some examples on exact reachability.

There are two image computation methods in transition function method; input splitting (default) and output splitting. Also three preimage computation methods in transition function method are implemented; domain cofactoring (default), sequential substitution, and simultaneous substitution.

The performance of transition function method is significantly depending on both the choice of splitting variable and the use of image cache. However, the hybrid method does not use image cache by default. Since the recursion depths are bounded (not so deep) in the hybrid method, the cache hit ratio is usually very low.

The implementation of the transition function method and the hybrid method is very complicate since there are so many options. For details, try print_tfm_options and print_hybrid_options commands in vis, also more detailed descriptions for all options can be read by using help in vis for the two commands.

The hybrid method can start with either only function vector or only transition relation, as well as with both function vector and transition relation. In case of starting with only the function vector, when we switch to conjoin, transition relation is built on demand. This method may consume less memory than the others, but it may take more time since it is a big overhead to build transition relation at every conjunction. To reduce this overhead, the hybrid method can start with both function vector and transition relation (default). In the presense of non-determinism, the hybrid mehtod also can start with only transition relation without the function vector.]

SeeAlso [imgTfmFwd.c imgTfmBwd.c imgTfmUtil.c imgTfmCache.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.]

Definition at line 77 of file imgTfm.c.