#include "imgInt.h"
Include dependency graph for imgHybrid.c:
Go to the source code of this file.
Functions | |
| static float | ComputeSupportLambda (ImgTfmInfo_t *info, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, mdd_t *from, array_t *vector, int newRelationFlag, int preFlag, float *improvedLambda) |
| void | Img_PrintHybridOptions (void) |
| int | ImgDecideSplitOrConjoin (ImgTfmInfo_t *info, array_t *vector, mdd_t *from, int preFlag, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int useBothFlag, int depth) |
| mdd_t * | ImgImageByHybrid (ImgTfmInfo_t *info, array_t *vector, mdd_t *from) |
| mdd_t * | ImgImageByHybridWithStaticSplit (ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube) |
| mdd_t * | ImgPreImageByHybrid (ImgTfmInfo_t *info, array_t *vector, mdd_t *from) |
| mdd_t * | ImgPreImageByHybridWithStaticSplit (ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube) |
| int | ImgCheckEquivalence (ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int preFlag) |
| int | ImgCheckMatching (ImgTfmInfo_t *info, array_t *vector, array_t *relationArray) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: imgHybrid.c,v 1.27 2008/11/27 02:19:53 fabio Exp $" |
Function Documentation
| static float ComputeSupportLambda | ( | ImgTfmInfo_t * | info, |
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube, | ||
| mdd_t * | from, | ||
| array_t * | vector, | ||
| int | newRelationFlag, | ||
| int | preFlag, | ||
| float * | improvedLambda | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Computes variable lifetime lambda.]
Description [Computes variable lifetime lambda. newRelationFlag is 1 when relationArray is made from the function vector directly, in other words, relationArray is an array of next state functions in this case.]
SideEffects []
Definition at line 1194 of file imgHybrid.c.
{
array_t *newRelationArray, *clusteredRelationArray;
ImgComponent_t *comp;
int i, j, nVars, nSupports;
mdd_t *newFrom, *var;
char *support;
array_t *smoothVarsBddArray, *introducedVarsBddArray;
array_t *domainVarsBddArray;
array_t *smoothSchedule, *smoothVars;
float lambda;
int size, total, lifetime;
Img_DirectionType direction;
int lambdaWithFrom, prevArea;
array_t *orderedRelationArray;
int nIntroducedVars;
int *highest, *lowest;
mdd_t *relation;
int asIs;
if (cofactorCube && abstractCube) {
newRelationArray = ImgGetCofactoredAbstractedRelationArray(info->manager,
relationArray, cofactorCube, abstractCube);
if (from && info->option->lambdaWithFrom) {
if (preFlag)
newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
else
newFrom = mdd_dup(from);
array_insert_last(mdd_t *, newRelationArray, newFrom);
lambdaWithFrom = 1;
} else {
lambdaWithFrom = 0;
newFrom = NIL(mdd_t);
}
} else {
if (from && info->option->lambdaWithFrom) {
if (newRelationFlag) {
newRelationArray = relationArray;
if (preFlag)
newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
else
newFrom = from;
} else {
/* We don't want to modify the original relation array */
newRelationArray = mdd_array_duplicate(relationArray);
if (preFlag)
newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
else
newFrom = mdd_dup(from);
}
array_insert_last(mdd_t *, newRelationArray, newFrom);
lambdaWithFrom = 1;
} else {
newRelationArray = relationArray;
newFrom = NIL(mdd_t);
lambdaWithFrom = 0;
}
}
if (vector) {
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
array_insert_last(mdd_t *, newRelationArray, mdd_dup(comp->func));
}
}
nVars = info->nVars;
support = ALLOC(char, sizeof(char) * nVars);
memset(support, 0, sizeof(char) * nVars);
comp = ImgComponentAlloc(info);
for (i = 0; i < array_n(newRelationArray); i++) {
comp->func = array_fetch(mdd_t *, newRelationArray, i);;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
for (j = 0; j < nVars; j++)
support[j] = support[j] | comp->support[j];
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
nSupports = 0;
smoothVarsBddArray = array_alloc(mdd_t *, 0);
domainVarsBddArray = array_alloc(mdd_t *, 0);
introducedVarsBddArray = array_alloc(mdd_t *, 0);
for (i = 0; i < nVars; i++) {
if (support[i]) {
var = bdd_var_with_index(info->manager, i);
if (preFlag) {
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
if (lambdaWithFrom)
array_insert_last(mdd_t *, smoothVarsBddArray, var);
else
array_insert_last(mdd_t *, domainVarsBddArray, var);
if (info->option->preLambdaMode == 0 ||
info->option->preLambdaMode == 2)
nSupports++;
} else {
if (info->preKeepPiInTr) {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *))) {
array_insert_last(mdd_t *, introducedVarsBddArray, var);
nSupports++;
} else if (info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
nSupports++;
} else { /* ps variables */
array_insert_last(mdd_t *, introducedVarsBddArray, var);
if (info->option->preLambdaMode != 0)
nSupports++;
}
} else {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *)) ||
(info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *)))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
nSupports++;
} else { /* ps variables */
array_insert_last(mdd_t *, introducedVarsBddArray, var);
if (info->option->preLambdaMode != 0)
nSupports++;
}
}
}
} else { /* image computation */
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
array_insert_last(mdd_t *, introducedVarsBddArray, var);
if (info->option->lambdaMode == 2)
nSupports++;
} else {
if (lambdaWithFrom)
array_insert_last(mdd_t *, smoothVarsBddArray, var);
else {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *)) ||
(info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *)))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
} else
array_insert_last(mdd_t *, domainVarsBddArray, var);
}
nSupports++;
}
}
}
}
if (preFlag)
direction = Img_Backward_c;
else
direction = Img_Forward_c;
if (info->option->lambdaFromMlp) {
FREE(support);
if (info->option->lambdaWithClustering) {
ImgMlpClusterRelationArray(info->manager, info->functionData,
newRelationArray, domainVarsBddArray,
smoothVarsBddArray, introducedVarsBddArray,
direction, &clusteredRelationArray, NIL(array_t *),
info->trmOption);
if (newRelationArray != relationArray)
mdd_array_free(newRelationArray);
newRelationArray = clusteredRelationArray;
}
prevArea = info->prevTotal;
asIs = newRelationFlag ? 0 : 1; /* 0 when relationArray is an array of
functions, i.e. without next state
variables */
lambda = ImgMlpComputeLambda(info->manager, newRelationArray,
domainVarsBddArray, smoothVarsBddArray,
introducedVarsBddArray, direction,
info->option->lambdaMode, asIs, &prevArea,
improvedLambda, info->trmOption);
info->prevTotal = prevArea;
} else {
smoothSchedule = ImgGetQuantificationSchedule(info->manager,
info->functionData, info->option->trMethod,
direction, info->trmOption, newRelationArray,
smoothVarsBddArray, domainVarsBddArray,
introducedVarsBddArray,
info->option->lambdaWithClustering,
&orderedRelationArray);
if (direction == Img_Forward_c) {
size = array_n(smoothSchedule);
lifetime = 0;
if (info->option->lambdaMode == 0) { /* total lifetime (lambda) */
for (i = 1; i < size; i++) {
smoothVars = array_fetch(array_t *, smoothSchedule, i);
lifetime += array_n(smoothVars) * i;
}
total = nSupports * (size - 1);
} else if (info->option->lambdaMode == 1) { /* active lifetime (lambda) */
lowest = ALLOC(int, sizeof(int) * nVars);
for (i = 0; i < nVars; i++)
lowest[i] = nVars;
highest = ALLOC(int, sizeof(int) * nVars);
memset(highest, 0, sizeof(int) * nVars);
comp = ImgComponentAlloc(info);
for (i = 0; i < size - 1; i++) {
relation = array_fetch(mdd_t *, orderedRelationArray, i);
comp->func = relation;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
for (j = 0; j < nVars; j++) {
if (!comp->support[j])
continue;
if (st_lookup(info->rangeVarsTable, (char *)(long)j, NIL(char *)))
continue;
if (i < lowest[j])
lowest[j] = i;
if (i > highest[j])
highest[j] = i;
}
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
for (i = 0; i < nVars; i++) {
if (lowest[i] == nVars)
continue;
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
continue;
lifetime += highest[i] - lowest[i] + 1;
}
if (newRelationFlag)
lifetime += array_n(newRelationArray);
total = nSupports * (size - 1);
FREE(lowest);
FREE(highest);
} else { /* total lifetime (lambda) with introduced variables */
for (i = 1; i < size; i++) {
smoothVars = array_fetch(array_t *, smoothSchedule, i);
lifetime += array_n(smoothVars) * i;
}
if (newRelationFlag) {
nIntroducedVars = array_n(newRelationArray);
lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
} else {
comp = ImgComponentAlloc(info);
for (i = 0; i < size - 1; i++) {
relation = array_fetch(mdd_t *, orderedRelationArray, i);
comp->func = relation;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
nIntroducedVars = 0;
for (j = 0; j < nVars; j++) {
if (!comp->support[j])
continue;
if (st_lookup(info->rangeVarsTable, (char *)(long)j, NIL(char *)))
nIntroducedVars++;
}
lifetime += (size - i - 1) * nIntroducedVars;
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
}
total = nSupports * (size - 1);
}
mdd_array_array_free(smoothSchedule);
} else if (info->option->preLambdaMode == 0) { /* total lifetime (lambda) */
/* direction == Img_Backward_c */
size = array_n(smoothSchedule);
lifetime = 0;
for (i = 1; i < size; i++) {
smoothVars = array_fetch(array_t *, smoothSchedule, i);
lifetime += array_n(smoothVars) * i;
}
total = nSupports * (size - 1);
mdd_array_array_free(smoothSchedule);
} else { /* direction == Img_Backward_c */
size = array_n(smoothSchedule);
mdd_array_array_free(smoothSchedule);
lifetime = 0;
lowest = ALLOC(int, sizeof(int) * nVars);
for (i = 0; i < nVars; i++)
lowest[i] = nVars;
highest = ALLOC(int, sizeof(int) * nVars);
memset(highest, 0, sizeof(int) * nVars);
comp = ImgComponentAlloc(info);
for (i = 0; i < size - 1; i++) {
relation = array_fetch(mdd_t *, orderedRelationArray, i);
comp->func = relation;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
for (j = 0; j < nVars; j++) {
if (!comp->support[j])
continue;
if (i < lowest[j])
lowest[j] = i;
if (i > highest[j])
highest[j] = i;
}
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
if (info->option->preLambdaMode == 1) { /* active lifetime (lambda) */
for (i = 0; i < nVars; i++) {
if (lowest[i] == nVars)
continue;
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)) ||
st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *)) ||
(info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *)))) {
lifetime += highest[i] - lowest[i] + 1;
}
}
if (newRelationFlag)
lifetime += array_n(newRelationArray);
total = nSupports * (size - 1);
} else if (info->option->preLambdaMode == 2) {
/* total lifetime (lambda) with introduced variables */
for (i = 0; i < nVars; i++) {
if (lowest[i] == nVars)
continue;
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)) ||
st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *)) ||
(info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *)))) {
lifetime += highest[i] + 1;
} else {
lifetime += size - lowest[i] - 1;
}
}
if (newRelationFlag) {
nIntroducedVars = array_n(newRelationArray);
lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
}
total = nSupports * (size - 1);
} else { /* total lifetime (lambda) with ps/pi variables */
for (i = 0; i < nVars; i++) {
if (lowest[i] == nVars)
continue;
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
continue;
if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *)) ||
(info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *)))) {
lifetime += highest[i] + 1;
} else {
lifetime += size - lowest[i] - 1;
}
}
if (newRelationFlag) {
nIntroducedVars = array_n(newRelationArray);
lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
}
total = nSupports * (size - 1);
}
FREE(lowest);
FREE(highest);
}
FREE(support);
mdd_array_free(orderedRelationArray);
if (total == 0.0) {
lambda = 0.0;
*improvedLambda = 0.0;
} else {
lambda = (float)lifetime / (float)total;
if (info->prevTotal) {
*improvedLambda = info->prevLambda -
(float)lifetime / (float)info->prevTotal;
} else
*improvedLambda = 0.0;
}
info->prevTotal = total;
}
mdd_array_free(smoothVarsBddArray);
mdd_array_free(domainVarsBddArray);
mdd_array_free(introducedVarsBddArray);
if (newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newRelationFlag && from && info->option->lambdaWithFrom &&
newFrom != from) {
mdd_free(newFrom);
}
if (info->option->verbosity >= 2) {
if (preFlag)
fprintf(vis_stdout, "** tfm info: lambda for preimage = %.2f\n", lambda);
else
fprintf(vis_stdout, "** tfm info: lambda for image = %.2f\n", lambda);
}
info->prevLambda = lambda;
return(lambda);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_PrintHybridOptions | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Prints the options for hybrid image computation.]
Description [Prints the options for hybrid image computation.]
SideEffects []
SeeAlso []
Definition at line 89 of file imgHybrid.c.
{
ImgTfmOption_t *options;
char dummy[80];
options = ImgTfmGetOptions(Img_Hybrid_c);
switch (options->hybridMode) {
case 0 :
sprintf(dummy, "with only transition function");
break;
case 1 :
sprintf(dummy, "with both transition function and relation");
break;
case 2 :
sprintf(dummy, "with only transition relation");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "HYB: hybrid_mode = %d (%s)\n",
options->hybridMode, dummy);
switch (options->trSplitMethod) {
case 0 :
sprintf(dummy, "support");
break;
case 1 :
sprintf(dummy, "estimate BDD size");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "HYB: hybrid_tr_split_method = %d (%s)\n",
options->trSplitMethod, dummy);
if (options->buildPartialTR)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_build_partial_tr = %s\n", dummy);
fprintf(vis_stdout, "HYB: hybrid_partial_num_vars = %d\n",
options->nPartialVars);
switch (options->partialMethod) {
case 0 :
sprintf(dummy, "BDD size");
break;
case 1 :
sprintf(dummy, "support");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "HYB: hybrid_partial_method = %d (%s)\n",
options->partialMethod, dummy);
if (options->delayedSplit)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_delayed_split = %s\n", dummy);
fprintf(vis_stdout, "HYB: hybrid_split_min_depth = %d\n",
options->splitMinDepth);
fprintf(vis_stdout, "HYB: hybrid_split_max_depth = %d\n",
options->splitMaxDepth);
fprintf(vis_stdout, "HYB: hybrid_pre_split_min_depth = %d\n",
options->preSplitMinDepth);
fprintf(vis_stdout, "HYB: hybrid_pre_split_max_depth = %d\n",
options->preSplitMaxDepth);
fprintf(vis_stdout, "HYB: hybrid_lambda_threshold = %.2f\n",
options->lambdaThreshold);
fprintf(vis_stdout, "HYB: hybrid_pre_lambda_threshold = %.2f\n",
options->preLambdaThreshold);
fprintf(vis_stdout, "HYB: hybrid_conjoin_vector_size = %d\n",
options->conjoinVectorSize);
fprintf(vis_stdout, "HYB: hybrid_conjoin_relation_size = %d\n",
options->conjoinRelationSize);
fprintf(vis_stdout, "HYB: hybrid_conjoin_relation_bdd_size = %d\n",
options->conjoinRelationBddSize);
fprintf(vis_stdout, "HYB: hybrid_improve_lambda = %.2f\n",
options->improveLambda);
fprintf(vis_stdout, "HYB: hybrid_improve_vector_size = %d\n",
options->improveVectorSize);
fprintf(vis_stdout, "HYB: hybrid_improve_vector_bdd_size = %.2f\n",
options->improveVectorBddSize);
switch (options->decideMode) {
case 0 :
sprintf(dummy, "use only lambda");
break;
case 1 :
sprintf(dummy, "lambda + special check");
break;
case 2 :
sprintf(dummy, "lambda + improvement");
break;
case 3 :
sprintf(dummy, "use all");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "HYB: hybrid_decide_mode = %d (%s)\n",
options->decideMode, dummy);
if (options->reorderWithFrom)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_reorder_with_from = %s\n", dummy);
if (options->preReorderWithFrom)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_pre_reorder_with_from = %s\n", dummy);
switch (options->lambdaMode) {
case 0 :
sprintf(dummy, "total lifetime with ps/pi variables");
break;
case 1 :
sprintf(dummy, "active lifetime with ps/pi variables");
break;
case 2 :
sprintf(dummy, "total lifetime with ps/ns/pi variables");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "HYB: hybrid_lambda_mode = %d (%s)\n",
options->lambdaMode, dummy);
switch (options->preLambdaMode) {
case 0 :
sprintf(dummy, "total lifetime with ns/pi variables");
break;
case 1 :
sprintf(dummy, "active lifetime with ps/pi variables");
break;
case 2 :
sprintf(dummy, "total lifetime with ps/ns/pi variables");
break;
case 3 :
sprintf(dummy, "total lifetime with ps/pi variables");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "HYB: hybrid_pre_lambda_mode = %d (%s)\n",
options->preLambdaMode, dummy);
if (options->lambdaWithFrom)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_lambda_with_from = %s\n", dummy);
if (options->lambdaWithTr)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_lambda_with_tr = %s\n", dummy);
if (options->lambdaWithClustering)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_lambda_with_clustering = %s\n", dummy);
if (options->synchronizeTr)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_synchronize_tr = %s\n", dummy);
if (options->imgKeepPiInTr)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_img_keep_pi = %s\n", dummy);
if (options->preKeepPiInTr)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_pre_keep_pi = %s\n", dummy);
if (options->preCanonical)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "HYB: hybrid_pre_canonical = %s\n", dummy);
switch (options->trMethod) {
case Img_Iwls95_c :
sprintf(dummy, "IWLS95");
break;
case Img_Mlp_c :
sprintf(dummy, "MLP");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "HYB: hybrid_tr_method = %s\n", dummy);
FREE(options);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int ImgCheckEquivalence | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube, | ||
| int | preFlag | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a vector is equivalent to a relation array.]
Description [Checks whether a vector is equivalent to a relation array.]
SideEffects []
Definition at line 1031 of file imgHybrid.c.
{
int i, equal;
mdd_t *product1, *product2;
mdd_t *var, *tmp, *relation;
ImgComponent_t *comp;
array_t *newRelationArray, *tmpRelationArray;
array_t *domainVarBddArray, *quantifyVarBddArray;
tmpRelationArray = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate)
relation = mdd_xnor(comp->var, comp->func);
else {
var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
relation = mdd_xnor(var, comp->func);
mdd_free(var);
}
array_insert_last(mdd_t *, tmpRelationArray, relation);
}
if (preFlag) {
if (info->preKeepPiInTr) {
quantifyVarBddArray = array_alloc(mdd_t *, 0);
domainVarBddArray = array_join(info->domainVarBddArray,
info->quantifyVarBddArray);
} else {
quantifyVarBddArray = info->quantifyVarBddArray;
domainVarBddArray = info->domainVarBddArray;
}
newRelationArray = ImgClusterRelationArray(info->manager,
info->functionData, info->option->trMethod, Img_Backward_c,
info->trmOption, tmpRelationArray, domainVarBddArray,
quantifyVarBddArray, info->rangeVarBddArray,
NIL(array_t *), NIL(array_t *), 0);
if (info->preKeepPiInTr) {
array_free(quantifyVarBddArray);
array_free(domainVarBddArray);
}
} else {
newRelationArray = ImgClusterRelationArray(info->manager,
info->functionData, info->option->trMethod, Img_Forward_c,
info->trmOption, tmpRelationArray, info->domainVarBddArray,
info->quantifyVarBddArray, info->rangeVarBddArray,
NIL(array_t *), NIL(array_t *), 0);
}
mdd_array_free(tmpRelationArray);
product1 = mdd_one(info->manager);
for (i = 0; i < array_n(newRelationArray); i++) {
relation = array_fetch(mdd_t *, newRelationArray, i);
tmp = product1;
product1 = mdd_and(tmp, relation, 1, 1);
mdd_free(tmp);
}
mdd_array_free(newRelationArray);
if (cofactorCube && abstractCube) {
newRelationArray = ImgGetCofactoredAbstractedRelationArray(info->manager,
relationArray, cofactorCube, abstractCube);
} else
newRelationArray = relationArray;
product2 = mdd_one(info->manager);
for (i = 0; i < array_n(newRelationArray); i++) {
relation = array_fetch(mdd_t *, newRelationArray, i);
tmp = product2;
product2 = mdd_and(tmp, relation, 1, 1);
mdd_free(tmp);
}
if (newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (mdd_equal(product1, product2))
equal = 1;
else
equal = 0;
mdd_free(product1);
mdd_free(product2);
return(equal);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int ImgCheckMatching | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| array_t * | relationArray | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a vector corresponds to its relation array.]
Description [Checks whether a vector corresponds to its relation array. This function is used only for debugging with image_cluster_size = 1. Checks each function vector whether its relation exists in the transition relation.]
SideEffects []
Definition at line 1132 of file imgHybrid.c.
{
int i, equal = 1;
mdd_t *var, *relation;
ImgComponent_t *comp;
st_table *relationTable;
int *ptr;
relationTable = st_init_table(st_ptrcmp, st_ptrhash);
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
ptr = (int *)bdd_pointer(relation);
st_insert(relationTable, (char *)ptr, NULL);
}
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate)
relation = mdd_xnor(comp->var, comp->func);
else {
var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
relation = mdd_xnor(var, comp->func);
mdd_free(var);
}
ptr = (int *)bdd_pointer(relation);
if (!st_lookup(relationTable, (char *)ptr, NULL)) {
if (comp->intermediate) {
fprintf(vis_stderr,
"Error : relation of varId[%d - intermediate] not found\n",
(int)bdd_top_var_id(comp->var));
} else {
fprintf(vis_stderr, "Error : relation of varId[%d] not found\n",
(int)bdd_top_var_id(comp->var));
}
equal = 0;
}
mdd_free(relation);
}
st_free_table(relationTable);
return(equal);
}
Here is the call graph for this function:
| int ImgDecideSplitOrConjoin | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from, | ||
| int | preFlag, | ||
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube, | ||
| int | useBothFlag, | ||
| int | depth | ||
| ) |
Function********************************************************************
Synopsis [Decides whether to split or to conjoin.]
Description [Decides whether to split or to conjoin.]
SideEffects []
Definition at line 325 of file imgHybrid.c.
{
int conjoin = 0;
float lambda, improvedLambda;
int vectorBddSize, vectorSize;
int improved;
int minDepth;
int checkSpecialCases;
int checkImprovement;
int relationSize = 0;
if (!preFlag) {
if (vector && array_n(vector) <= 2)
return(0); /* terminal case */
}
if (info->option->decideMode == 1 || info->option->decideMode == 3)
checkSpecialCases = 1;
else
checkSpecialCases = 0;
if (info->option->decideMode == 2 || info->option->decideMode == 3)
checkImprovement = 1;
else
checkImprovement = 0;
if (checkSpecialCases) {
if (vector && array_n(vector) <= info->option->conjoinVectorSize) {
if (preFlag)
info->nConjoinsB++;
else
info->nConjoins++;
if (info->option->printLambda) {
fprintf(vis_stdout, "%d: conjoin - small vector size (%d)\n",
depth, array_n(vector));
}
return(1);
}
}
if (preFlag)
minDepth = info->option->preSplitMinDepth;
else
minDepth = info->option->splitMinDepth;
if (useBothFlag && relationArray && vector) {
lambda = ComputeSupportLambda(info, relationArray, cofactorCube,
abstractCube, from, vector,
0, preFlag, &improvedLambda);
} else if (relationArray) {
if (checkSpecialCases) {
if (array_n(relationArray) <= info->option->conjoinRelationSize ||
(relationSize = (int)bdd_size_multiple(relationArray)) <=
info->option->conjoinRelationBddSize) {
if (preFlag)
info->nConjoinsB++;
else
info->nConjoins++;
if (info->option->printLambda) {
fprintf(vis_stdout, "%d: conjoin - small relation array (%d, %ld)\n",
depth, array_n(relationArray),
bdd_size_multiple(relationArray));
}
return(1);
}
}
lambda = ComputeSupportLambda(info, relationArray, cofactorCube,
abstractCube, from, NIL(array_t),
0, preFlag, &improvedLambda);
} else {
int i;
ImgComponent_t *comp;
relationArray = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
array_insert_last(mdd_t *, relationArray, comp->func);
}
lambda = ComputeSupportLambda(info, relationArray, NIL(mdd_t),
NIL(mdd_t), from, NIL(array_t),
1, preFlag, &improvedLambda);
array_free(relationArray);
}
if ((preFlag == 0 && lambda <= info->option->lambdaThreshold) ||
(preFlag == 1 && lambda <= info->option->preLambdaThreshold)) {
if (preFlag)
info->nConjoinsB++;
else
info->nConjoins++;
if (info->option->printLambda) {
fprintf(vis_stdout, "%d: conjoin - small lambda (%.2f)\n",
depth, lambda);
}
conjoin = 1;
} else {
if (checkImprovement) {
if (vector) {
vectorBddSize = ImgVectorBddSize(vector);
vectorSize = array_n(vector);
if (depth == minDepth ||
improvedLambda >= info->option->improveLambda ||
((float)vectorBddSize * 100.0 / (float)info->prevVectorBddSize) <=
info->option->improveVectorBddSize ||
(info->prevVectorSize - vectorSize) >=
info->option->improveVectorSize) {
improved = 1;
} else
improved = 0;
info->prevVectorBddSize = vectorBddSize;
info->prevVectorSize = vectorSize;
} else {
if (relationSize)
vectorBddSize = relationSize;
else
vectorBddSize = (int)bdd_size_multiple(relationArray);
if (depth == minDepth ||
improvedLambda >= info->option->improveLambda ||
((float)vectorBddSize * 100.0 / (float)info->prevVectorBddSize) <=
info->option->improveVectorBddSize) {
improved = 1;
} else
improved = 0;
info->prevVectorBddSize = vectorBddSize;
}
if (improved) {
if (preFlag)
info->nSplitsB++;
else
info->nSplits++;
if (info->option->printLambda) {
fprintf(vis_stdout, "%d: split - big lambda (%.2f) - improved\n",
depth, lambda);
}
conjoin = 0;
} else {
if (preFlag)
info->nConjoinsB++;
else
info->nConjoins++;
if (info->option->printLambda) {
fprintf(vis_stdout, "%d: conjon - big lambda (%.2f) - not improved\n",
depth, lambda);
}
conjoin = 1;
}
} else {
if (preFlag)
info->nSplitsB++;
else
info->nSplits++;
if (info->option->printLambda) {
fprintf(vis_stdout, "%d: split - big lambda (%.2f)\n",
depth, lambda);
}
conjoin = 0;
}
}
return(conjoin); /* 0 : split, 1 : conjoin */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* ImgImageByHybrid | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from | ||
| ) |
Function********************************************************************
Synopsis [Computes an image by transition relation.]
Description [Computes an image by transition relation.]
SideEffects []
Definition at line 503 of file imgHybrid.c.
{
int i, j, nVars;
array_t *relationArray;
mdd_t *result, *domain, *relation, *var, *nextVar;
ImgComponent_t *comp;
char *support;
array_t *smoothVarsBddArray, *introducedVarsBddArray;
array_t *domainVarsBddArray;
int bddId;
if (from && bdd_is_tautology(from, 0))
return(mdd_zero(info->manager));
nVars = info->nVars;
support = ALLOC(char, sizeof(char) * nVars);
memset(support, 0, sizeof(char) * nVars);
relationArray = array_alloc(mdd_t *, 0);
introducedVarsBddArray = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
relation = mdd_xnor(comp->var, comp->func);
bddId = (int)bdd_top_var_id(comp->var);
support[bddId] = 1;
} else {
nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
relation = mdd_xnor(nextVar, comp->func);
array_insert_last(mdd_t *, introducedVarsBddArray, nextVar);
}
array_insert_last(mdd_t *, relationArray, relation);
for (j = 0; j < nVars; j++)
support[j] = support[j] | comp->support[j];
}
if (from && (!bdd_is_tautology(from, 1))) {
if (info->option->reorderWithFrom)
array_insert_last(mdd_t *, relationArray, mdd_dup(from));
comp = ImgComponentAlloc(info);
comp->func = from;
ImgComponentGetSupport(comp);
for (i = 0; i < nVars; i++)
support[i] = support[i] | comp->support[i];
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
}
smoothVarsBddArray = array_alloc(mdd_t *, 0);
if (!info->option->reorderWithFrom)
domainVarsBddArray = array_alloc(mdd_t *, 0);
else
domainVarsBddArray = NIL(array_t);
for (i = 0; i < nVars; i++) {
if (support[i]) {
var = bdd_var_with_index(info->manager, i);
if ((!from) || info->option->reorderWithFrom)
array_insert_last(mdd_t *, smoothVarsBddArray, var);
else {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)) ||
(info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *)))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
} else {
array_insert_last(mdd_t *, domainVarsBddArray, var);
}
}
}
}
FREE(support);
if ((!from) || info->option->reorderWithFrom) {
result = ImgMultiwayLinearAndSmooth(info->manager,
relationArray,
smoothVarsBddArray,
introducedVarsBddArray,
info->option->trMethod,
Img_Forward_c,
info->trmOption);
} else {
result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
relationArray, from,
smoothVarsBddArray,
domainVarsBddArray,
introducedVarsBddArray,
info->option->trMethod,
Img_Forward_c,
info->trmOption);
mdd_array_free(domainVarsBddArray);
}
mdd_array_free(relationArray);
mdd_array_free(smoothVarsBddArray);
mdd_array_free(introducedVarsBddArray);
domain = ImgSubstitute(result, info->functionData, Img_R2D_c);
mdd_free(result);
return(domain);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* ImgImageByHybridWithStaticSplit | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from, | ||
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube | ||
| ) |
Function********************************************************************
Synopsis [Computes an image by transition relation.]
Description [Computes an image by transition relation.]
SideEffects []
Definition at line 616 of file imgHybrid.c.
{
int i, j;
array_t *mergedRelationArray;
mdd_t *result, *domain, *relation, *var, *nextVar;
ImgComponent_t *comp, *supportComp;
int nVars;
char *support;
array_t *smoothVarsBddArray, *introducedVarsBddArray;
array_t *domainVarsBddArray;
if (from && bdd_is_tautology(from, 0))
return(mdd_zero(info->manager));
if (cofactorCube && abstractCube) {
if (!bdd_is_tautology(cofactorCube, 1) &&
!bdd_is_tautology(abstractCube, 1)) {
mergedRelationArray = ImgGetCofactoredAbstractedRelationArray(
info->manager, relationArray,
cofactorCube, abstractCube);
} else if (!bdd_is_tautology(cofactorCube, 1)) {
mergedRelationArray = ImgGetCofactoredRelationArray(relationArray,
cofactorCube);
} else if (!bdd_is_tautology(abstractCube, 1)) {
mergedRelationArray = ImgGetAbstractedRelationArray(info->manager,
relationArray,
abstractCube);
} else
mergedRelationArray = mdd_array_duplicate(relationArray);
} else
mergedRelationArray = mdd_array_duplicate(relationArray);
nVars = info->nVars;
support = ALLOC(char, sizeof(char) * nVars);
memset(support, 0, sizeof(char) * nVars);
supportComp = ImgComponentAlloc(info);
for (i = 0; i < array_n(mergedRelationArray); i++) {
supportComp->func = array_fetch(mdd_t *, mergedRelationArray, i);;
ImgSupportClear(info, supportComp->support);
ImgComponentGetSupport(supportComp);
for (j = 0; j < nVars; j++)
support[j] = support[j] | supportComp->support[j];
}
if (vector && array_n(vector) > 0) {
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
relation = mdd_xnor(comp->var, comp->func);
support[(int)bdd_top_var_id(comp->var)] = 1;
} else {
nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
relation = mdd_xnor(nextVar, comp->func);
support[(int)bdd_top_var_id(nextVar)] = 1;
mdd_free(nextVar);
}
array_insert_last(mdd_t *, mergedRelationArray, relation);
for (j = 0; j < nVars; j++)
support[j] = support[j] | comp->support[j];
}
}
if (from) {
if ((!bdd_is_tautology(from, 1)) && info->option->reorderWithFrom)
array_insert_last(mdd_t *, mergedRelationArray, mdd_dup(from));
supportComp->func = from;
ImgSupportClear(info, supportComp->support);
ImgComponentGetSupport(supportComp);
for (i = 0; i < nVars; i++)
support[i] = support[i] | supportComp->support[i];
}
supportComp->func = NIL(mdd_t);
ImgComponentFree(supportComp);
smoothVarsBddArray = array_alloc(mdd_t *, 0);
introducedVarsBddArray = array_alloc(mdd_t *, 0);
if (!info->option->reorderWithFrom)
domainVarsBddArray = array_alloc(mdd_t *, 0);
else
domainVarsBddArray = NIL(array_t);
for (i = 0; i < nVars; i++) {
if (support[i]) {
var = bdd_var_with_index(info->manager, i);
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
array_insert_last(mdd_t *, introducedVarsBddArray, var);
else if ((!from) || info->option->reorderWithFrom)
array_insert_last(mdd_t *, smoothVarsBddArray, var);
else {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)) ||
(info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *)))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
} else {
array_insert_last(mdd_t *, domainVarsBddArray, var);
}
}
}
}
FREE(support);
if ((!from) || info->option->reorderWithFrom) {
result = ImgMultiwayLinearAndSmooth(info->manager,
mergedRelationArray,
smoothVarsBddArray,
introducedVarsBddArray,
info->option->trMethod,
Img_Forward_c,
info->trmOption);
} else {
result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
mergedRelationArray, from,
smoothVarsBddArray,
domainVarsBddArray,
introducedVarsBddArray,
info->option->trMethod,
Img_Forward_c,
info->trmOption);
mdd_array_free(domainVarsBddArray);
}
mdd_array_free(mergedRelationArray);
mdd_array_free(smoothVarsBddArray);
mdd_array_free(introducedVarsBddArray);
domain = ImgSubstitute(result, info->functionData, Img_R2D_c);
mdd_free(result);
return(domain);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* ImgPreImageByHybrid | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from | ||
| ) |
Function********************************************************************
Synopsis [Computes a preimage by transition relation.]
Description [Computes a preimage by transition relation.]
SideEffects []
Definition at line 761 of file imgHybrid.c.
{
int i, j, nVars;
array_t *relationArray;
mdd_t *result, *relation, *var, *nextVar;
ImgComponent_t *comp;
char *support;
array_t *smoothVarsBddArray, *introducedVarsBddArray;
array_t *rangeVarsBddArray;
mdd_t *fromRange;
if (bdd_is_tautology(from, 1))
return(mdd_one(info->manager));
else if (bdd_is_tautology(from, 0))
return(mdd_zero(info->manager));
nVars = info->nVars;
support = ALLOC(char, sizeof(char) * nVars);
memset(support, 0, sizeof(char) * nVars);
relationArray = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
relation = mdd_xnor(comp->var, comp->func);
support[(int)bdd_top_var_id(comp->var)] = 1;
} else {
nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
relation = mdd_xnor(nextVar, comp->func);
support[(int)bdd_top_var_id(nextVar)] = 1;
mdd_free(nextVar);
}
array_insert_last(mdd_t *, relationArray, relation);
for (j = 0; j < nVars; j++)
support[j] = support[j] | comp->support[j];
}
fromRange = ImgSubstitute(from, info->functionData, Img_D2R_c);
comp = ImgComponentAlloc(info);
comp->func = fromRange;
ImgComponentGetSupport(comp);
for (i = 0; i < nVars; i++)
support[i] = support[i] | comp->support[i];
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
smoothVarsBddArray = array_alloc(mdd_t *, 0);
introducedVarsBddArray = array_alloc(mdd_t *, 0);
if (!info->option->preReorderWithFrom)
rangeVarsBddArray = array_alloc(mdd_t *, 0);
else
rangeVarsBddArray = NIL(array_t);
for (i = 0; i < nVars; i++) {
if (support[i]) {
var = bdd_var_with_index(info->manager, i);
if (info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
} else if (st_lookup(info->rangeVarsTable, (char *)(long)i,
NIL(char *))) {
if (info->option->preReorderWithFrom)
array_insert_last(mdd_t *, smoothVarsBddArray, var);
else
array_insert_last(mdd_t *, rangeVarsBddArray, var);
} else {
if (info->preKeepPiInTr)
array_insert_last(mdd_t *, introducedVarsBddArray, var);
else {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
} else
array_insert_last(mdd_t *, introducedVarsBddArray, var);
}
}
}
}
FREE(support);
if (info->option->preReorderWithFrom) {
array_insert_last(mdd_t *, relationArray, fromRange);
result = ImgMultiwayLinearAndSmooth(info->manager,
relationArray,
smoothVarsBddArray,
introducedVarsBddArray,
info->option->trMethod,
Img_Backward_c,
info->trmOption);
} else {
result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
relationArray, fromRange,
smoothVarsBddArray,
rangeVarsBddArray,
introducedVarsBddArray,
info->option->trMethod,
Img_Backward_c,
info->trmOption);
mdd_free(fromRange);
mdd_array_free(rangeVarsBddArray);
}
mdd_array_free(relationArray);
mdd_array_free(smoothVarsBddArray);
mdd_array_free(introducedVarsBddArray);
return(result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* ImgPreImageByHybridWithStaticSplit | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from, | ||
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube | ||
| ) |
Function********************************************************************
Synopsis [Computes a preimage by transition relation.]
Description [Computes a preimage by transition relation.]
SideEffects []
Definition at line 881 of file imgHybrid.c.
{
int i, j;
array_t *mergedRelationArray;
mdd_t *result, *relation, *var, *nextVar, *fromRange;
ImgComponent_t *comp, *supportComp;
int nVars;
char *support;
array_t *smoothVarsBddArray, *introducedVarsBddArray;
array_t *rangeVarsBddArray;
if (bdd_is_tautology(from, 1))
return(mdd_one(info->manager));
if (bdd_is_tautology(from, 0))
return(mdd_zero(info->manager));
if (cofactorCube && abstractCube) {
if (!bdd_is_tautology(cofactorCube, 1) &&
!bdd_is_tautology(abstractCube, 1)) {
mergedRelationArray = ImgGetCofactoredAbstractedRelationArray(
info->manager, relationArray,
cofactorCube, abstractCube);
} else if (!bdd_is_tautology(cofactorCube, 1)) {
mergedRelationArray = ImgGetCofactoredRelationArray(relationArray,
cofactorCube);
} else if (!bdd_is_tautology(abstractCube, 1)) {
mergedRelationArray = ImgGetAbstractedRelationArray(info->manager,
relationArray,
abstractCube);
} else
mergedRelationArray = mdd_array_duplicate(relationArray);
} else
mergedRelationArray = mdd_array_duplicate(relationArray);
nVars = info->nVars;
support = ALLOC(char, sizeof(char) * nVars);
memset(support, 0, sizeof(char) * nVars);
supportComp = ImgComponentAlloc(info);
for (i = 0; i < array_n(mergedRelationArray); i++) {
supportComp->func = array_fetch(mdd_t *, mergedRelationArray, i);;
ImgSupportClear(info, supportComp->support);
ImgComponentGetSupport(supportComp);
for (j = 0; j < nVars; j++)
support[j] = support[j] | supportComp->support[j];
}
if (vector && array_n(vector) > 0) {
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
relation = mdd_xnor(comp->var, comp->func);
support[(int)bdd_top_var_id(comp->var)] = 1;
} else {
nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
relation = mdd_xnor(nextVar, comp->func);
support[(int)bdd_top_var_id(nextVar)] = 1;
mdd_free(nextVar);
}
array_insert_last(mdd_t *, mergedRelationArray, relation);
for (j = 0; j < nVars; j++)
support[j] = support[j] | comp->support[j];
}
}
fromRange = ImgSubstitute(from, info->functionData, Img_D2R_c);
supportComp->func = fromRange;
ImgSupportClear(info, supportComp->support);
ImgComponentGetSupport(supportComp);
for (i = 0; i < nVars; i++)
support[i] = support[i] | supportComp->support[i];
supportComp->func = NIL(mdd_t);
ImgComponentFree(supportComp);
smoothVarsBddArray = array_alloc(mdd_t *, 0);
introducedVarsBddArray = array_alloc(mdd_t *, 0);
if (!info->option->preReorderWithFrom)
rangeVarsBddArray = array_alloc(mdd_t *, 0);
else
rangeVarsBddArray = NIL(array_t);
for (i = 0; i < nVars; i++) {
if (support[i]) {
var = bdd_var_with_index(info->manager, i);
if (info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
} else if (st_lookup(info->rangeVarsTable, (char *)(long)i,
NIL(char *))) {
if (info->option->preReorderWithFrom)
array_insert_last(mdd_t *, smoothVarsBddArray, var);
else
array_insert_last(mdd_t *, rangeVarsBddArray, var);
} else {
if (info->preKeepPiInTr)
array_insert_last(mdd_t *, introducedVarsBddArray, var);
else {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *))) {
array_insert_last(mdd_t *, smoothVarsBddArray, var);
} else
array_insert_last(mdd_t *, introducedVarsBddArray, var);
}
}
}
}
FREE(support);
if (info->option->preReorderWithFrom) {
array_insert_last(mdd_t *, mergedRelationArray, fromRange);
result = ImgMultiwayLinearAndSmooth(info->manager,
mergedRelationArray,
smoothVarsBddArray,
introducedVarsBddArray,
info->option->trMethod,
Img_Backward_c,
info->trmOption);
} else {
result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
mergedRelationArray, fromRange,
smoothVarsBddArray,
rangeVarsBddArray,
introducedVarsBddArray,
info->option->trMethod,
Img_Backward_c,
info->trmOption);
mdd_free(fromRange);
mdd_array_free(rangeVarsBddArray);
}
mdd_array_free(mergedRelationArray);
mdd_array_free(smoothVarsBddArray);
mdd_array_free(introducedVarsBddArray);
return(result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: imgHybrid.c,v 1.27 2008/11/27 02:19:53 fabio Exp $" [static] |
CFile***********************************************************************
FileName [imgHybrid.c]
PackageName [img]
Synopsis [Routines for hybrid image computation.]
Description [The hybrid image computation method combines transition function and relation methods, in other words, combines splitting and conjunction methods.]
SeeAlso []
Author [In-Ho Moon]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
Definition at line 39 of file imgHybrid.c.
