#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] |
int nHookInfoList [static] |
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.]
