#include "imgInt.h"
Include dependency graph for imgTfmBwd.c:
Go to the source code of this file.
Functions | |
| static bdd_t * | PreImageByDomainCofactoring (ImgTfmInfo_t *info, array_t *delta, bdd_t *image, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int splitMethod, int turnDepth, int depth) |
| static mdd_t * | PreImageByStaticDomainCofactoring (ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth) |
| static bdd_t * | PreImageByConstraintCofactoring (ImgTfmInfo_t *info, array_t *delta, bdd_t *image, int splitMethod, int turnDepth, int depth) |
| static mdd_t * | PreImageBySubstitution (ImgTfmInfo_t *info, array_t *vector, mdd_t *from) |
| static bdd_t * | PreImageMakeVectorCanonical (ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube) |
| static bdd_t * | PreImageMakeRelationCanonical (ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray) |
| static bdd_t * | PreImageDeleteOneComponent (ImgTfmInfo_t *info, array_t *delta, int index, array_t **newDelta) |
| static int | PreImageChooseSplitVar (ImgTfmInfo_t *info, array_t *delta, bdd_t *img, int splitMethod, int split) |
| static mdd_t * | DomainCofactoring (ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *c, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube) |
| static int | CheckPreImageVector (ImgTfmInfo_t *info, array_t *vector, mdd_t *image) |
| bdd_t * | ImgTfmPreImage (ImgTfmInfo_t *info, bdd_t *image) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: imgTfmBwd.c,v 1.29 2002/08/18 04:47:07 fabio Exp $" |
Function Documentation
| static int CheckPreImageVector | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | image | ||
| ) | [static] |
Function********************************************************************
Synopsis [Checks sanity of a vector for preimage.]
Description [Checks sanity of a vector for preimage.]
SideEffects []
Definition at line 2699 of file imgTfmBwd.c.
{
ImgComponent_t *comp, *imgComp;
int i, id, size, status;
status = 1;
if (info->nIntermediateVars)
size = ImgVectorFunctionSize(vector);
else
size = array_n(vector);
if (size != mdd_get_number_of_bdd_support(info->manager, image)) {
fprintf(vis_stderr,
"** tfm error: function vector length is different. (%d != %d)\n",
size, mdd_get_number_of_bdd_support(info->manager, image));
status = 0;
}
imgComp = ImgComponentAlloc(info);
imgComp->func = image;
ImgComponentGetSupport(imgComp);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
id = (int)bdd_top_var_id(comp->var);
if (comp->intermediate)
imgComp->support[id] = 2;
else if (imgComp->support[id] == 0) {
fprintf(vis_stderr,
"** tfm error: variable index[%d] is not in constraint\n", id);
status = 0;
} else
imgComp->support[id] = 2;
}
for (i = 0; i < info->nVars; i++) {
if (imgComp->support[i] == 1) {
fprintf(vis_stderr,
"** tfm error: variable index[%d] is not in function vector\n", i);
status = 0;
}
}
imgComp->func = NIL(mdd_t);
ImgComponentFree(imgComp);
return(status);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * DomainCofactoring | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from, | ||
| array_t * | relationArray, | ||
| mdd_t * | c, | ||
| array_t ** | newVector, | ||
| array_t ** | newRelationArray, | ||
| mdd_t ** | cofactorCube, | ||
| mdd_t ** | abstractCube | ||
| ) | [static] |
Function********************************************************************
Synopsis [Performs domain cofactoring on a vector and from set with respect to a variable.]
Description [Performs domain cofactoring on a vector and from set with respect to a variable.]
SideEffects []
Definition at line 2469 of file imgTfmBwd.c.
{
mdd_t *res, *tmp;
ImgComponent_t *comp, *comp1;
array_t *vector1;
int i, index, n, pos;
mdd_t *newFrom, *var, *nsVar;
mdd_t *cofactor, *abstract, *constIntermediate;
array_t *tmpRelationArray;
st_table *equivTable;
int *ptr, *regularPtr;
int size;
newFrom = mdd_dup(from);
vector1 = array_alloc(ImgComponent_t *, 0);
if (relationArray) {
cofactor = mdd_one(info->manager);
abstract = mdd_one(info->manager);
} else {
cofactor = NIL(mdd_t);
abstract = NIL(mdd_t);
}
if (info->nIntermediateVars) {
size = ImgVectorFunctionSize(vector);
if (size == array_n(vector))
constIntermediate = NIL(mdd_t);
else
constIntermediate = mdd_one(info->manager);
} else
constIntermediate = NIL(mdd_t);
n = 0;
equivTable = st_init_table(st_ptrcmp, st_ptrhash);
index = (int)bdd_top_var_id(c);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->support[index])
res = bdd_cofactor(comp->func, c);
else
res = mdd_dup(comp->func);
if (bdd_is_tautology(res, 1)) {
if (comp->intermediate) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
mdd_free(res);
continue;
}
tmp = newFrom;
newFrom = bdd_cofactor(tmp, comp->var);
mdd_free(tmp);
mdd_free(res);
if (relationArray) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else if (bdd_is_tautology(res, 0)) {
if (comp->intermediate) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
mdd_free(res);
continue;
}
tmp = newFrom;
var = mdd_not(comp->var);
newFrom = bdd_cofactor(tmp, var);
mdd_free(tmp);
mdd_free(var);
mdd_free(res);
if (relationArray) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
if (comp->intermediate) {
comp1 = ImgComponentAlloc(info);
comp1->var = mdd_dup(comp->var);
comp1->func = res;
if (mdd_equal(res, comp->func))
ImgSupportCopy(info, comp1->support, comp->support);
else
ImgComponentGetSupport(comp1);
comp1->intermediate = 1;
array_insert_last(ImgComponent_t *, vector1, comp1);
n++;
continue;
}
ptr = (int *)bdd_pointer(res);
regularPtr = (int *)((unsigned long)ptr & ~01);
if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
comp1 = array_fetch(ImgComponent_t *, vector1, pos);
if (mdd_equal(res, comp1->func)) {
tmp = newFrom;
newFrom = bdd_compose(tmp, comp->var, comp1->var);
mdd_free(tmp);
} else {
tmp = newFrom;
var = mdd_not(comp1->var);
newFrom = bdd_compose(tmp, comp->var, var);
mdd_free(tmp);
mdd_free(var);
}
mdd_free(res);
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
comp1 = ImgComponentAlloc(info);
comp1->var = mdd_dup(comp->var);
comp1->func = res;
if (mdd_equal(res, comp->func))
ImgSupportCopy(info, comp1->support, comp->support);
else
ImgComponentGetSupport(comp1);
array_insert_last(ImgComponent_t *, vector1, comp1);
st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
n++;
}
}
}
st_free_table(equivTable);
if (constIntermediate) {
if (!bdd_is_tautology(constIntermediate, 1)) {
mdd_t *tmpCofactor, *tmpAbstract;
if (relationArray) {
vector1 = ImgComposeConstIntermediateVars(info, vector1,
constIntermediate,
&tmpCofactor, &tmpAbstract,
NIL(mdd_t *), &newFrom);
if (!bdd_is_tautology(tmpCofactor, 1)) {
tmp = cofactor;
cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpCofactor);
if (!bdd_is_tautology(tmpAbstract, 1)) {
tmp = abstract;
abstract = mdd_and(tmp, tmpAbstract, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpAbstract);
tmp = cofactor;
cofactor = mdd_and(tmp, constIntermediate, 1, 1);
mdd_free(tmp);
} else {
vector1 = ImgComposeConstIntermediateVars(info, vector1,
constIntermediate,
NIL(mdd_t *), NIL(mdd_t *),
NIL(mdd_t *), &newFrom);
}
}
mdd_free(constIntermediate);
}
*newVector = vector1;
if (relationArray) {
if (newRelationArray)
*newRelationArray = relationArray;
if (cofactorCube && abstractCube) {
if (cofactor) {
if (bdd_is_tautology(cofactor, 1)) {
mdd_free(cofactor);
*cofactorCube = mdd_dup(c);
} else {
*cofactorCube = mdd_and(cofactor, c, 1, 1);
mdd_free(cofactor);
}
}
if (abstract)
*abstractCube = abstract;
} else {
if (bdd_is_tautology(cofactor, 1)) {
*newRelationArray = ImgGetCofactoredRelationArray(relationArray, c);
mdd_free(cofactor);
} else {
tmp = cofactor;
cofactor = mdd_and(tmp, c, 1, 1);
mdd_free(tmp);
*newRelationArray = ImgGetCofactoredRelationArray(relationArray,
cofactor);
mdd_free(cofactor);
}
if (bdd_is_tautology(abstract, 1))
mdd_free(abstract);
else {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetAbstractedRelationArray(info->manager,
tmpRelationArray,
abstract);
mdd_free(abstract);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
}
}
} else
*newRelationArray = NIL(array_t);
return(newFrom);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_t* ImgTfmPreImage | ( | ImgTfmInfo_t * | info, |
| bdd_t * | image | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Computes a preimage with transition function method.]
Description [Computes a preimage with transition function method.]
SideEffects []
Definition at line 100 of file imgTfmBwd.c.
{
bdd_t *preImg, *pre;
int turnDepth;
bdd_t *refResult, *one;
array_t *relationArray;
int partial;
bdd_t *from;
array_t *vector;
if (bdd_is_tautology(image, 1)) {
preImg = mdd_one(info->manager);
return(preImg);
} else if (bdd_is_tautology(image, 0)) {
preImg = mdd_zero(info->manager);
return(preImg);
}
info->maxIntermediateSize = 0;
if (info->buildTR) {
if (info->option->preSplitMethod == 4 &&
info->option->preSplitMaxDepth < 0 &&
info->option->buildPartialTR == FALSE &&
info->preKeepPiInTr == FALSE &&
info->option->preCanonical == FALSE) {
mdd_t *range;
range = ImgSubstitute(image, info->functionData, Img_D2R_c);
preImg = ImgBddLinearAndSmooth(info->manager, range,
info->bwdClusteredRelationArray,
info->bwdArraySmoothVarBddArray,
info->bwdSmoothVarCubeArray,
info->option->verbosity);
mdd_free(range);
return(preImg);
}
relationArray = mdd_array_duplicate(info->bwdClusteredRelationArray);
} else
relationArray = NIL(array_t);
one = mdd_one(info->manager);
vector = info->vector;
from = image;
partial = 0;
if (info->option->preSplitMethod == 0) {
preImg = PreImageByDomainCofactoring(info, vector, from,
NIL(array_t), NIL(mdd_t), NIL(mdd_t),
info->option->preSplitMethod, 0, 0);
} else if (info->option->preSplitMethod == 1) {
preImg = PreImageByConstraintCofactoring(info, vector, from,
info->option->preSplitMethod,
0, 0);
} else if (info->option->preSplitMethod == 3) {
preImg = PreImageBySubstitution(info, vector, from);
} else {
turnDepth = info->option->turnDepth;
if (turnDepth == 0) {
if (info->option->preSplitMethod == 2) {
preImg = PreImageByConstraintCofactoring(info, vector, from,
info->option->preSplitMethod,
turnDepth, 0);
} else
preImg = ImgPreImageByHybrid(info, vector, from);
} else if (info->option->preSplitMethod == 2) {
preImg = PreImageByDomainCofactoring(info, vector, from,
relationArray,
NIL(mdd_t), NIL(mdd_t),
info->option->preSplitMethod,
turnDepth, 0);
} else {
if (info->buildTR) {
if (info->buildTR == 2) {
if (info->buildPartialTR) {
preImg = PreImageByStaticDomainCofactoring(info, vector,
from, relationArray,
turnDepth, 0);
partial = 1;
} else {
preImg = PreImageByStaticDomainCofactoring(info, NIL(array_t),
from, relationArray,
turnDepth, 0);
}
} else if (info->option->delayedSplit) {
preImg = PreImageByDomainCofactoring(info, vector, from,
relationArray, one, one,
info->option->preSplitMethod,
turnDepth, 0);
} else {
preImg = PreImageByDomainCofactoring(info, vector, from,
relationArray,
NIL(mdd_t), NIL(mdd_t),
info->option->preSplitMethod,
turnDepth, 0);
}
} else {
preImg = PreImageByDomainCofactoring(info, vector, from,
relationArray,
NIL(mdd_t), NIL(mdd_t),
info->option->preSplitMethod,
turnDepth, 0);
}
}
}
mdd_free(one);
if (info->option->debug) {
if (info->buildTR == 2) {
refResult = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t),
image, relationArray,
NIL(mdd_t), NIL(mdd_t));
} else {
if (partial) {
refResult = ImgPreImageByHybridWithStaticSplit(info, info->vector,
image, relationArray,
NIL(mdd_t), NIL(mdd_t));
} else
refResult = ImgPreImageByHybrid(info, info->vector, image);
}
assert(mdd_equal_mod_care_set_array(refResult, preImg,
info->toCareSetArray));
mdd_free(refResult);
}
if (relationArray)
mdd_array_free(relationArray);
if (info->preCache && info->option->autoFlushCache == 1)
ImgFlushCache(info->preCache);
if (info->preKeepPiInTr == TRUE) {
if (info->functionData->quantifyCube)
pre = bdd_smooth_with_cube(preImg, info->functionData->quantifyCube);
else
pre = bdd_smooth(preImg, info->functionData->quantifyBddVars);
mdd_free(preImg);
} else
pre = preImg;
if (info->option->verbosity) {
fprintf(vis_stdout,
"** tfm info: max BDD size for intermediate product = %d\n",
info->maxIntermediateSize);
}
return(pre);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_t * PreImageByConstraintCofactoring | ( | ImgTfmInfo_t * | info, |
| array_t * | delta, | ||
| bdd_t * | image, | ||
| int | splitMethod, | ||
| int | turnDepth, | ||
| int | depth | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes preimage with constraint cofactoring method.]
Description [Computes preimage with constraint cofactoring method.]
SideEffects []
Definition at line 1248 of file imgTfmBwd.c.
{
array_t *newDelta, *tmpDelta, *vector;
bdd_t *preImg, *preImgT, *preImgE, *imgT, *imgE;
bdd_t *c, *newImg, *tmpImg;
int split;
bdd_t *var, *varNot, *refResult;
ImgComponent_t *comp;
int nRecur, size;
mdd_t *essentialCube;
int findEssential;
int foundEssentialDepth;
int foundEssentialDepthT, foundEssentialDepthE;
mdd_t *saveCareSet = NIL(mdd_t), *tmp;
info->nRecursionB++;
if (info->nIntermediateVars)
size = ImgVectorFunctionSize(delta);
else
size = array_n(delta);
if (size == 1) {
preImg = PreImageBySubstitution(info, delta, image);
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
info->foundEssentialDepth = info->option->maxEssentialDepth;
return(preImg);
}
if (info->option->findEssential) {
if (info->option->findEssential == 1)
findEssential = 1;
else {
if (depth >= info->lastFoundEssentialDepth)
findEssential = 1;
else
findEssential = 0;
}
} else
findEssential = 0;
if (findEssential) {
essentialCube = bdd_find_essential_cube(image);
if (!bdd_is_tautology(essentialCube, 1)) {
info->averageFoundEssential = (info->averageFoundEssential *
(float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) /
(float)(info->nFoundEssentials + 1);
info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth *
(float)info->nFoundEssentials + (float)depth) /
(float)(info->nFoundEssentials + 1);
if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth)
info->topFoundEssentialDepth = depth;
if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
info->foundEssentials[depth]++;
info->nFoundEssentials++;
tmpImg = ImgVectorMinimize(info, delta, essentialCube, image,
NIL(array_t), &tmpDelta, NIL(mdd_t *),
NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *));
foundEssentialDepth = depth;
} else {
tmpDelta = delta;
tmpImg = image;
foundEssentialDepth = info->option->maxEssentialDepth;
}
mdd_free(essentialCube);
foundEssentialDepthT = info->option->maxEssentialDepth;
foundEssentialDepthE = info->option->maxEssentialDepth;
} else {
tmpDelta = delta;
tmpImg = image;
/* To remove compiler warnings */
foundEssentialDepth = -1;
foundEssentialDepthT = -1;
foundEssentialDepthE = -1;
}
if (info->option->preCanonical) {
newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg, NIL(array_t),
&newDelta, NIL(array_t *), NIL(mdd_t *),
NIL(mdd_t *));
} else {
newImg = tmpImg;
newDelta = tmpDelta;
}
if (tmpDelta != delta)
ImgVectorFree(tmpDelta);
if (tmpImg != image)
mdd_free(tmpImg);
if (bdd_is_tautology(newImg, 1) || bdd_is_tautology(newImg, 0)) {
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(newImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
ImgVectorFree(newDelta);
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(newImg);
}
if (info->preCache) {
preImg = ImgCacheLookupTable(info, info->preCache, newDelta, newImg);
if (preImg) {
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
ImgVectorFree(newDelta);
mdd_free(newImg);
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(preImg);
}
}
if (depth == turnDepth) {
preImg = ImgPreImageByHybrid(info, newDelta, newImg);
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
if (info->preCache)
ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
else {
ImgVectorFree(newDelta);
mdd_free(newImg);
}
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
info->nTurnsB++;
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(preImg);
}
split = PreImageChooseSplitVar(info, newDelta, newImg,
1, info->option->preOutputSplit);
comp = array_fetch(ImgComponent_t *, newDelta, split);
var = mdd_dup(comp->var);
varNot = mdd_not(var);
imgE = bdd_cofactor(newImg, varNot);
mdd_free(varNot);
imgT = bdd_cofactor(newImg, var);
mdd_free(var);
if (!info->preCache && !info->option->debug)
mdd_free(newImg);
c = PreImageDeleteOneComponent(info, newDelta, split, &vector);
if (!info->preCache && !info->option->debug)
ImgVectorFree(newDelta);
nRecur = 0;
if (bdd_is_tautology(imgT, 1))
preImgT = mdd_one(info->manager);
else if (bdd_is_tautology(imgT, 0))
preImgT = mdd_zero(info->manager);
else {
if (info->option->debug) {
saveCareSet = info->debugCareSet;
info->debugCareSet = mdd_and(saveCareSet, c, 1, 1);
}
preImgT = PreImageByConstraintCofactoring(info, vector, imgT, splitMethod,
turnDepth, depth + 1);
if (info->option->debug) {
mdd_free(info->debugCareSet);
info->debugCareSet = saveCareSet;
}
if (findEssential)
foundEssentialDepthT = info->foundEssentialDepth;
nRecur++;
}
mdd_free(imgT);
if (bdd_is_tautology(imgE, 1))
preImgE = mdd_one(info->manager);
else if (bdd_is_tautology(imgE, 0))
preImgE = mdd_zero(info->manager);
else {
if (info->option->debug) {
saveCareSet = info->debugCareSet;
info->debugCareSet = mdd_and(saveCareSet, c, 1, 0);
}
preImgE = PreImageByConstraintCofactoring(info, vector, imgE, splitMethod,
turnDepth, depth + 1);
if (info->option->debug) {
mdd_free(info->debugCareSet);
info->debugCareSet = saveCareSet;
}
if (findEssential)
foundEssentialDepthE = info->foundEssentialDepth;
nRecur++;
}
mdd_free(imgE);
ImgVectorFree(vector);
preImg = bdd_ite(c, preImgT, preImgE, 1, 1, 1);
if (info->option->verbosity) {
size = bdd_size(preImg);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_ite(%d,%d,%d) = %d\n",
bdd_size(c), bdd_size(preImgT), bdd_size(preImgE),
bdd_size(preImg));
}
}
mdd_free(c);
mdd_free(preImgT);
mdd_free(preImgE);
if (info->preCache)
ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
if (!info->preCache) {
ImgVectorFree(newDelta);
mdd_free(newImg);
}
}
if (nRecur == 0) {
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
}
if (findEssential) {
if (foundEssentialDepth == info->option->maxEssentialDepth) {
if (foundEssentialDepthT < foundEssentialDepthE)
foundEssentialDepth = foundEssentialDepthT;
else
foundEssentialDepth = foundEssentialDepthE;
}
info->foundEssentialDepth = foundEssentialDepth;
}
return(preImg);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_t * PreImageByDomainCofactoring | ( | ImgTfmInfo_t * | info, |
| array_t * | delta, | ||
| bdd_t * | image, | ||
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube, | ||
| int | splitMethod, | ||
| int | turnDepth, | ||
| int | depth | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Computes preimage with domain cofactoring method.]
Description [Computes preimage with domain cofactoring method.]
SideEffects []
Definition at line 261 of file imgTfmBwd.c.
{
array_t *newDelta, *tmpDelta, *vectorT, *vectorE;
bdd_t *preImg, *preImgT, *preImgE, *imgT, *imgE, *newImg, *tmpImg;
int split;
bdd_t *var, *varNot, *refResult;
int nRecur;
array_t *relationArrayT, *relationArrayE;
array_t *newRelationArray, *tmpRelationArray;
mdd_t *cofactorCubeT, *cofactorCubeE;
mdd_t *abstractCubeT, *abstractCubeE;
mdd_t *newCofactorCube, *newAbstractCube;
mdd_t *cofactor, *abstract;
mdd_t *essentialCube, *tmp;
int findEssential;
int foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE;
int turnFlag, size;
mdd_t *saveCareSet = NIL(mdd_t);
newRelationArray = NIL(array_t);
if (info->option->checkEquivalence && relationArray) {
assert(ImgCheckEquivalence(info, delta, relationArray,
cofactorCube, abstractCube, 1));
}
info->nRecursionB++;
if (info->option->debug) {
if (relationArray) {
refResult = ImgPreImageByHybrid(info, delta, image);
preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), image,
relationArray,
cofactorCube, abstractCube);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = preImg;
preImg = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
assert(mdd_equal_mod_care_set_array(refResult, preImg,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(preImg);
}
}
if (info->nIntermediateVars)
size = ImgVectorFunctionSize(delta);
else
size = array_n(delta);
if (size == 1) {
preImg = PreImageBySubstitution(info, delta, image);
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
info->foundEssentialDepth = info->option->maxEssentialDepth;
return(preImg);
}
if (info->option->findEssential) {
if (info->option->findEssential == 1)
findEssential = 1;
else {
if (depth >= info->lastFoundEssentialDepth)
findEssential = 1;
else
findEssential = 0;
}
} else
findEssential = 0;
if (findEssential) {
essentialCube = bdd_find_essential_cube(image);
if (!bdd_is_tautology(essentialCube, 1)) {
info->averageFoundEssential = (info->averageFoundEssential *
(float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) /
(float)(info->nFoundEssentials + 1);
info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth *
(float)info->nFoundEssentials + (float)depth) /
(float)(info->nFoundEssentials + 1);
if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth)
info->topFoundEssentialDepth = depth;
if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
info->foundEssentials[depth]++;
info->nFoundEssentials++;
if (info->option->delayedSplit && relationArray) {
tmpRelationArray = relationArray;
tmpImg = ImgVectorMinimize(info, delta, essentialCube, image,
tmpRelationArray, &tmpDelta, NIL(mdd_t *),
NIL(array_t *), &cofactor, &abstract);
if (bdd_is_tautology(cofactor, 1))
newCofactorCube = cofactorCube;
else
newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1);
mdd_free(cofactor);
if (bdd_is_tautology(abstract, 1))
newAbstractCube = abstractCube;
else
newAbstractCube = mdd_and(abstractCube, abstract, 1, 1);
mdd_free(abstract);
} else {
if (relationArray)
tmpRelationArray = mdd_array_duplicate(relationArray);
else
tmpRelationArray = relationArray;
tmpImg = ImgVectorMinimize(info, delta, essentialCube, image,
tmpRelationArray, &tmpDelta, NIL(mdd_t *),
NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *));
newCofactorCube = cofactorCube;
newAbstractCube = abstractCube;
}
foundEssentialDepth = depth;
} else {
tmpDelta = delta;
tmpRelationArray = relationArray;
tmpImg = image;
newCofactorCube = cofactorCube;
newAbstractCube = abstractCube;
foundEssentialDepth = info->option->maxEssentialDepth;
}
mdd_free(essentialCube);
foundEssentialDepthT = info->option->maxEssentialDepth;
foundEssentialDepthE = info->option->maxEssentialDepth;
} else {
tmpDelta = delta;
tmpRelationArray = relationArray;
tmpImg = image;
newCofactorCube = cofactorCube;
newAbstractCube = abstractCube;
/* To remove compiler warnings */
foundEssentialDepth = -1;
foundEssentialDepthT = -1;
foundEssentialDepthE = -1;
}
if (!info->option->preCanonical) {
newImg = tmpImg;
newDelta = tmpDelta;
newRelationArray = tmpRelationArray;
} else if (info->option->delayedSplit && relationArray) {
newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg,
tmpRelationArray, &newDelta,
&newRelationArray,
&cofactor, &abstract);
if (!bdd_is_tautology(cofactor, 1)) {
if (newCofactorCube == cofactorCube)
newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1);
else {
tmp = newCofactorCube;
newCofactorCube = mdd_and(tmp, cofactor, 1, 1);
mdd_free(tmp);
}
}
mdd_free(cofactor);
if (!bdd_is_tautology(abstract, 1)) {
if (newAbstractCube == abstractCube)
newAbstractCube = mdd_and(abstractCube, abstract, 1, 1);
else {
tmp = newAbstractCube;
newAbstractCube = mdd_and(tmp, abstract, 1, 1);
mdd_free(tmp);
}
}
mdd_free(abstract);
} else {
newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg,
tmpRelationArray, &newDelta,
&newRelationArray,
NIL(mdd_t *), NIL(mdd_t *));
}
if (tmpDelta != delta)
ImgVectorFree(tmpDelta);
if (tmpImg != image)
mdd_free(tmpImg);
if (tmpRelationArray && tmpRelationArray != relationArray &&
tmpRelationArray != newRelationArray) {
mdd_array_free(tmpRelationArray);
}
if (info->option->debug) {
if (relationArray) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg,
newRelationArray,
newCofactorCube,
newAbstractCube);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = preImg;
preImg = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
assert(mdd_equal_mod_care_set_array(refResult, preImg,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(preImg);
}
}
if (bdd_is_tautology(newImg, 1) || bdd_is_tautology(newImg, 0)) {
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(newImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
if (newDelta != delta)
ImgVectorFree(newDelta);
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube && newCofactorCube != cofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube && newAbstractCube != abstractCube)
mdd_free(newAbstractCube);
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(newImg);
}
if (array_n(newDelta) <= 1) {
if (array_n(newDelta) == 0)
preImg = newImg;
else {
assert(array_n(newDelta) == 1);
preImg = PreImageBySubstitution(info, newDelta, newImg);
mdd_free(newImg);
}
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, delta, image);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
if (newDelta != delta)
ImgVectorFree(newDelta);
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube && newCofactorCube != cofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube && newAbstractCube != abstractCube)
mdd_free(newAbstractCube);
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(preImg);
}
if (info->preCache) {
preImg = ImgCacheLookupTable(info, info->preCache, newDelta, newImg);
if (preImg) {
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
if (newDelta != delta)
ImgVectorFree(newDelta);
if (newImg != image)
mdd_free(newImg);
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube && newCofactorCube != cofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube && newAbstractCube != abstractCube)
mdd_free(newAbstractCube);
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(preImg);
}
}
turnFlag = 0;
if (splitMethod == 4 && turnDepth == -1) {
if (depth < info->option->preSplitMinDepth) {
info->nSplitsB++;
turnFlag = 0;
} else if (depth > info->option->preSplitMaxDepth) {
info->nConjoinsB++;
turnFlag = 1;
} else {
turnFlag = ImgDecideSplitOrConjoin(info, newDelta, newImg, 1,
newRelationArray, newCofactorCube,
newAbstractCube, 0, depth);
}
} else {
if (depth == turnDepth)
turnFlag = 1;
else
turnFlag = 0;
}
if (turnFlag) {
if (splitMethod == 2) {
preImg = PreImageByConstraintCofactoring(info, newDelta, newImg,
info->option->preSplitMethod,
0, depth + 1);
} else {
if (relationArray) {
preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg,
newRelationArray,
newCofactorCube,
newAbstractCube);
} else
preImg = ImgPreImageByHybrid(info, newDelta, newImg);
}
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
if (splitMethod == 4) {
if (info->preCache)
ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
else {
if (newDelta != delta)
ImgVectorFree(newDelta);
if (newImg != image)
mdd_free(newImg);
}
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
} else {
if (newDelta != delta)
ImgVectorFree(newDelta);
if (newImg != image)
mdd_free(newImg);
}
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube && newCofactorCube != cofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube && newAbstractCube != abstractCube)
mdd_free(newAbstractCube);
info->nTurnsB++;
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(preImg);
}
split = PreImageChooseSplitVar(info, newDelta, newImg,
0, info->option->preInputSplit);
/* No more present state variable to split */
if (split == -1) {
if (info->option->preDcLeafMethod == 0 ||
info->option->preDcLeafMethod == 2) {
if (info->option->preDcLeafMethod == 0)
preImg = PreImageBySubstitution(info, newDelta, newImg);
else if (relationArray) {
preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg,
newRelationArray,
newCofactorCube,
newAbstractCube);
} else
preImg = ImgPreImageByHybrid(info, newDelta, newImg);
if (info->preCache)
ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
} else {
preImg = PreImageByConstraintCofactoring(info, newDelta, newImg,
splitMethod, turnDepth,
depth + 1);
info->nRecursionB--;
}
if (splitMethod == 0)
info->nTurnsB++;
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
if (info->option->preDcLeafMethod != 0 || !info->preCache) {
if (newDelta != delta)
ImgVectorFree(newDelta);
if (newImg != image)
mdd_free(newImg);
}
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube && newCofactorCube != cofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube && newAbstractCube != abstractCube)
mdd_free(newAbstractCube);
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(preImg);
}
var = bdd_var_with_index(info->manager, split);
varNot = mdd_not(var);
if (info->option->delayedSplit && relationArray) {
imgT = DomainCofactoring(info, newDelta, newImg, newRelationArray, var,
&vectorT, &relationArrayT, &cofactor, &abstract);
if (bdd_is_tautology(cofactor, 1))
cofactorCubeT = newCofactorCube;
else
cofactorCubeT = mdd_and(newCofactorCube, cofactor, 1, 1);
mdd_free(cofactor);
if (bdd_is_tautology(abstract, 1))
abstractCubeT = newAbstractCube;
else
abstractCubeT = mdd_and(newAbstractCube, abstract, 1, 1);
mdd_free(abstract);
imgE = DomainCofactoring(info, newDelta, newImg, newRelationArray, varNot,
&vectorE, &relationArrayE, &cofactor, &abstract);
if (bdd_is_tautology(cofactor, 1))
cofactorCubeE = newCofactorCube;
else
cofactorCubeE = mdd_and(newCofactorCube, cofactor, 1, 1);
mdd_free(cofactor);
if (bdd_is_tautology(abstract, 1))
abstractCubeE = newAbstractCube;
else
abstractCubeE = mdd_and(newAbstractCube, abstract, 1, 1);
mdd_free(abstract);
} else {
imgT = DomainCofactoring(info, newDelta, newImg, newRelationArray, var,
&vectorT, &relationArrayT,
NIL(mdd_t *), NIL(mdd_t *));
cofactorCubeT = NIL(mdd_t);
abstractCubeT = NIL(mdd_t);
imgE = DomainCofactoring(info, newDelta, newImg, newRelationArray, varNot,
&vectorE, &relationArrayE,
NIL(mdd_t *), NIL(mdd_t *));
cofactorCubeE = NIL(mdd_t);
abstractCubeE = NIL(mdd_t);
}
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
mdd_free(varNot);
if (!info->preCache && !info->option->debug) {
if (newDelta != delta)
ImgVectorFree(newDelta);
if (newImg != image)
mdd_free(newImg);
}
nRecur = 0;
if (bdd_is_tautology(imgT, 1))
preImgT = mdd_one(info->manager);
else if (bdd_is_tautology(imgT, 0))
preImgT = mdd_zero(info->manager);
else {
if (info->option->debug) {
saveCareSet = info->debugCareSet;
info->debugCareSet = mdd_and(saveCareSet, var, 1, 1);
}
preImgT = PreImageByDomainCofactoring(info, vectorT, imgT, relationArrayT,
cofactorCubeT, abstractCubeT,
splitMethod, turnDepth,
depth + 1);
if (info->option->debug) {
mdd_free(info->debugCareSet);
info->debugCareSet = saveCareSet;
}
if (findEssential)
foundEssentialDepthT = info->foundEssentialDepth;
nRecur++;
}
ImgVectorFree(vectorT);
mdd_free(imgT);
if (relationArrayT && relationArrayT != newRelationArray)
mdd_array_free(relationArrayT);
if (cofactorCubeT && cofactorCubeT != newCofactorCube)
mdd_free(cofactorCubeT);
if (abstractCubeT && abstractCubeT != newAbstractCube)
mdd_free(abstractCubeT);
if (bdd_is_tautology(imgE, 1))
preImgE = mdd_one(info->manager);
else if (bdd_is_tautology(imgE, 0))
preImgE = mdd_zero(info->manager);
else {
if (info->option->debug) {
saveCareSet = info->debugCareSet;
info->debugCareSet = mdd_and(saveCareSet, var, 1, 0);
}
preImgE = PreImageByDomainCofactoring(info, vectorE, imgE, relationArrayE,
cofactorCubeE, abstractCubeE,
splitMethod, turnDepth,
depth + 1);
if (info->option->debug) {
mdd_free(info->debugCareSet);
info->debugCareSet = saveCareSet;
}
if (findEssential)
foundEssentialDepthE = info->foundEssentialDepth;
nRecur++;
}
ImgVectorFree(vectorE);
mdd_free(imgE);
if (relationArrayE && relationArrayT != newRelationArray)
mdd_array_free(relationArrayE);
if (cofactorCubeE && cofactorCubeE != newCofactorCube)
mdd_free(cofactorCubeE);
if (abstractCubeE && abstractCubeE != newAbstractCube)
mdd_free(abstractCubeE);
if (newCofactorCube && newCofactorCube != cofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube && newAbstractCube != abstractCube)
mdd_free(newAbstractCube);
preImg = bdd_ite(var, preImgT, preImgE, 1, 1, 1);
if (info->option->verbosity) {
size = bdd_size(preImg);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n",
bdd_size(preImgT), bdd_size(preImgE), bdd_size(preImg));
}
}
mdd_free(var);
mdd_free(preImgE);
mdd_free(preImgT);
if (info->preCache)
ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
if (info->option->debug) {
refResult = ImgPreImageByHybrid(info, newDelta, newImg);
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp,
info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
if (!info->preCache) {
if (newDelta != delta)
ImgVectorFree(newDelta);
if (newImg != image)
mdd_free(newImg);
}
}
if (nRecur == 0) {
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
}
if (findEssential) {
if (foundEssentialDepth == info->option->maxEssentialDepth) {
if (foundEssentialDepthT < foundEssentialDepthE)
foundEssentialDepth = foundEssentialDepthT;
else
foundEssentialDepth = foundEssentialDepthE;
}
info->foundEssentialDepth = foundEssentialDepth;
}
return(preImg);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * PreImageByStaticDomainCofactoring | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from, | ||
| array_t * | relationArray, | ||
| int | turnDepth, | ||
| int | depth | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes a preimage by static input splitting.]
Description [Computes a preimage by static input splitting.]
SideEffects []
Definition at line 884 of file imgTfmBwd.c.
{
array_t *vectorT, *vectorE, *newVector;
mdd_t *resT, *resE, *res, *cubeT, *cubeE;
mdd_t *fromT, *fromE, *newFrom, *tmpFrom;
mdd_t *var, *varNot;
array_t *relationArrayT, *relationArrayE;
array_t *newRelationArray, *tmpRelationArray;
int nRecur;
mdd_t *essentialCube, *refResult;
int findEssential;
int foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE;
int turnFlag, size;
mdd_t *saveCareSet = NIL(mdd_t), *tmp;
info->nRecursionB++;
turnFlag = 0;
if (turnDepth == -1) {
if (depth < info->option->preSplitMinDepth) {
info->nSplitsB++;
turnFlag = 0;
} else if (depth > info->option->preSplitMaxDepth) {
info->nConjoinsB++;
turnFlag = 1;
} else {
turnFlag = ImgDecideSplitOrConjoin(info, vector, from, 1,
relationArray, NIL(mdd_t),
NIL(mdd_t), 1, depth);
}
} else {
if (depth == turnDepth)
turnFlag = 1;
else
turnFlag = 0;
}
if (turnFlag) {
res = ImgPreImageByHybridWithStaticSplit(info, vector, from, relationArray,
NIL(mdd_t), NIL(mdd_t));
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
info->foundEssentialDepth = info->option->maxEssentialDepth;
return(res);
}
if (info->option->findEssential) {
if (info->option->findEssential == 1)
findEssential = 1;
else {
if (depth >= info->lastFoundEssentialDepth)
findEssential = 1;
else
findEssential = 0;
}
} else
findEssential = 0;
if (findEssential) {
essentialCube = bdd_find_essential_cube(from);
if (!bdd_is_tautology(essentialCube, 1)) {
info->averageFoundEssential = (info->averageFoundEssential *
(float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) /
(float)(info->nFoundEssentials + 1);
info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth *
(float)info->nFoundEssentials + (float)depth) /
(float)(info->nFoundEssentials + 1);
if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth)
info->topFoundEssentialDepth = depth;
if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
info->foundEssentials[depth]++;
info->nFoundEssentials++;
if (vector) {
array_t *tmpVector;
if (info->option->preCanonical) {
tmpFrom = PreImageMakeRelationCanonical(info, vector, from,
relationArray, &newVector,
&newRelationArray);
} else {
tmpFrom = from;
newVector = vector;
newRelationArray = relationArray;
}
tmpVector = newVector;
newFrom = ImgVectorMinimize(info, tmpVector, essentialCube, tmpFrom,
newRelationArray, &newVector, NIL(mdd_t *),
NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *));
if (tmpVector != vector)
ImgVectorFree(tmpVector);
if (tmpFrom != from)
mdd_free(tmpFrom);
} else {
tmpRelationArray = ImgGetCofactoredRelationArray(relationArray,
essentialCube);
if (info->option->preCanonical) {
newFrom = PreImageMakeRelationCanonical(info, vector, from,
tmpRelationArray, &newVector,
&newRelationArray);
mdd_array_free(tmpRelationArray);
} else {
newFrom = from;
newVector = vector;
newRelationArray = tmpRelationArray;
}
}
foundEssentialDepth = depth;
} else {
if (info->option->preCanonical) {
newFrom = PreImageMakeRelationCanonical(info, vector, from,
relationArray,
&newVector, &newRelationArray);
} else {
newFrom = from;
newVector = vector;
newRelationArray = relationArray;
}
foundEssentialDepth = info->option->maxEssentialDepth;
}
mdd_free(essentialCube);
foundEssentialDepthT = info->option->maxEssentialDepth;
foundEssentialDepthE = info->option->maxEssentialDepth;
} else {
if (info->option->preCanonical) {
newFrom = PreImageMakeRelationCanonical(info, vector, from, relationArray,
&newVector, &newRelationArray);
} else {
newFrom = from;
newVector = vector;
newRelationArray = relationArray;
}
/* To remove compiler warnings */
foundEssentialDepth = -1;
foundEssentialDepthT = -1;
foundEssentialDepthE = -1;
}
if (info->option->debug) {
refResult = ImgPreImageByHybridWithStaticSplit(info, vector, from,
relationArray,
NIL(mdd_t), NIL(mdd_t));
res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom,
newRelationArray,
NIL(mdd_t), NIL(mdd_t));
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = res;
res = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
assert(mdd_equal_mod_care_set_array(refResult, res, info->toCareSetArray));
mdd_free(refResult);
mdd_free(res);
}
if (bdd_is_tautology(newFrom, 1)) {
if (newVector && newVector != vector)
ImgVectorFree(newVector);
if (newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newFrom != from)
mdd_free(newFrom);
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(mdd_one(info->manager));
}
if (depth == turnDepth ||
(info->option->splitCubeFunc && bdd_is_cube(newFrom))) {
res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom,
newRelationArray,
NIL(mdd_t), NIL(mdd_t));
if (newVector && newVector != vector)
ImgVectorFree(newVector);
if (newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newFrom != from)
mdd_free(newFrom);
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(res);
}
var = ImgChooseTrSplitVar(info, newVector, newRelationArray,
info->option->trSplitMethod, 0);
if (!var) {
res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom,
newRelationArray,
NIL(mdd_t), NIL(mdd_t));
if (newVector && newVector != vector)
ImgVectorFree(newVector);
if (newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newFrom != from)
mdd_free(newFrom);
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
return(res);
}
varNot = mdd_not(var);
nRecur = 0;
if (newVector) {
ImgVectorConstrain(info, newVector, var, NIL(array_t),
&vectorT, &cubeT, NIL(array_t *),
NIL(mdd_t *), NIL(mdd_t *), TRUE);
fromT = bdd_cofactor(newFrom, cubeT);
mdd_free(cubeT);
} else {
vectorT = NIL(array_t);
fromT = mdd_dup(newFrom);
}
relationArrayT = ImgGetCofactoredRelationArray(newRelationArray, var);
if (bdd_is_tautology(fromT, 1)) {
resT = mdd_one(info->manager);
if (vectorT)
ImgVectorFree(vectorT);
} else if (bdd_is_tautology(fromT, 0)) {
resT = mdd_zero(info->manager);
if (vectorT)
ImgVectorFree(vectorT);
} else {
if (info->option->debug) {
saveCareSet = info->debugCareSet;
info->debugCareSet = mdd_and(saveCareSet, var, 1, 1);
}
resT = PreImageByStaticDomainCofactoring(info, vectorT, fromT,
relationArrayT, turnDepth, depth + 1);
if (info->option->debug) {
mdd_free(info->debugCareSet);
info->debugCareSet = saveCareSet;
}
if (findEssential)
foundEssentialDepthE = info->foundEssentialDepth;
if (vectorT)
ImgVectorFree(vectorT);
nRecur++;
}
mdd_free(fromT);
mdd_array_free(relationArrayT);
if (newVector) {
ImgVectorConstrain(info, newVector, varNot, NIL(array_t),
&vectorE, &cubeE, NIL(array_t *),
NIL(mdd_t *), NIL(mdd_t *), TRUE);
if (newVector != vector)
ImgVectorFree(newVector);
fromE = bdd_cofactor(newFrom, cubeE);
mdd_free(cubeE);
} else {
vectorE = NIL(array_t);
fromE = mdd_dup(newFrom);
}
if (newFrom != from)
mdd_free(newFrom);
relationArrayE = ImgGetCofactoredRelationArray(newRelationArray, varNot);
if (newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (bdd_is_tautology(fromE, 1)) {
resE = mdd_one(info->manager);
if (vectorE)
ImgVectorFree(vectorE);
} else if (bdd_is_tautology(fromE, 0)) {
resE = mdd_zero(info->manager);
if (vectorE)
ImgVectorFree(vectorE);
} else {
if (info->option->debug) {
saveCareSet = info->debugCareSet;
info->debugCareSet = mdd_and(saveCareSet, var, 1, 0);
}
resE = PreImageByStaticDomainCofactoring(info, vectorE, fromE,
relationArrayE, turnDepth, depth + 1);
if (info->option->debug) {
mdd_free(info->debugCareSet);
info->debugCareSet = saveCareSet;
}
if (findEssential)
foundEssentialDepthE = info->foundEssentialDepth;
if (vectorE)
ImgVectorFree(vectorE);
nRecur++;
}
mdd_free(fromE);
mdd_array_free(relationArrayE);
res = bdd_ite(var, resT, resE, 1, 1, 1);
if (info->option->verbosity) {
size = bdd_size(res);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n",
bdd_size(resT), bdd_size(resE), bdd_size(res));
}
}
mdd_free(resT);
mdd_free(resE);
mdd_free(var);
mdd_free(varNot);
if (info->option->debug) {
refResult = ImgPreImageByHybridWithStaticSplit(info, vector, from,
relationArray,
NIL(mdd_t), NIL(mdd_t));
tmp = refResult;
refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
mdd_free(tmp);
tmp = mdd_and(res, info->debugCareSet, 1, 1);
assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray));
mdd_free(refResult);
mdd_free(tmp);
}
if (nRecur == 0) {
info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
(float)depth) / (float)(info->nLeavesB + 1);
if (depth > info->maxDepthB)
info->maxDepthB = depth;
info->nLeavesB++;
}
if (findEssential) {
if (foundEssentialDepth == info->option->maxEssentialDepth) {
if (foundEssentialDepthT < foundEssentialDepthE)
foundEssentialDepth = foundEssentialDepthT;
else
foundEssentialDepth = foundEssentialDepthE;
}
info->foundEssentialDepth = foundEssentialDepth;
}
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * PreImageBySubstitution | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes a preimage by Filkorn's substitution.]
Description [Computes a preimage by Filkorn's substitution.]
SideEffects []
Definition at line 1544 of file imgTfmBwd.c.
{
int i, index;
ImgComponent_t *comp, *fromComp;
array_t *varArray, *funcArray;
mdd_t *result;
if (bdd_is_tautology(from, 1))
return(mdd_one(info->manager));
else if (bdd_is_tautology(from, 0))
return(mdd_zero(info->manager));
fromComp = ImgComponentAlloc(info);
fromComp->func = from;
ImgComponentGetSupport(fromComp);
varArray = array_alloc(mdd_t *, 0);
funcArray = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
index = bdd_top_var_id(comp->var);
if (fromComp->support[index] || comp->intermediate) {
array_insert_last(mdd_t *, varArray, comp->var);
array_insert_last(mdd_t *, funcArray, comp->func);
}
}
fromComp->func = NIL(mdd_t);
ImgComponentFree(fromComp);
result = bdd_vector_compose(from, varArray, funcArray);
array_free(varArray);
array_free(funcArray);
/* quantify all primary inputs */
if (info->preKeepPiInTr == FALSE) {
array_t *quantifyVarBddArray;
mdd_t *tmp;
if (info->newQuantifyBddVars)
quantifyVarBddArray = info->newQuantifyBddVars;
else
quantifyVarBddArray = info->quantifyVarBddArray;
tmp = result;
result = bdd_smooth(tmp, quantifyVarBddArray);
mdd_free(tmp);
}
return(result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int PreImageChooseSplitVar | ( | ImgTfmInfo_t * | info, |
| array_t * | delta, | ||
| bdd_t * | img, | ||
| int | splitMethod, | ||
| int | split | ||
| ) | [static] |
Function********************************************************************
Synopsis [Chooses a splitting variable for preimage.]
Description [Chooses a splitting variable for preimage.]
SideEffects []
Definition at line 2192 of file imgTfmBwd.c.
{
ImgComponent_t *comp, *imgComp;
int i, j, bestCost, newCost;
int index, bestVar, bestComp;
int nFuncs, nVars, bestOccur = 0;
int *varOccur, *varCost;
mdd_t *var, *varNot, *pcFunc, *ncFunc;
int tieCount = 0;
assert(array_n(delta) > 0);
if (splitMethod == 0) {
bestVar = -1;
bestComp = -1;
nFuncs = array_n(delta);
nVars = info->nVars;
varOccur = ALLOC(int, nVars);
memset(varOccur, 0, sizeof(int) * nVars);
varCost = NIL(int);
for (i = 0; i < nFuncs; i++) {
comp = array_fetch(ImgComponent_t *, delta, i);
for (j = 0; j < nVars; j++) {
if (comp->support[j])
varOccur[j]++;
}
}
switch (split) {
case 0: /* largest support */
for (i = 0; i < nVars; i++) {
if (varOccur[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 (bestVar == -1 || varOccur[i] > bestOccur) {
bestVar = i;
bestOccur = varOccur[i];
tieCount = 1;
} else if (varOccur[i] == bestOccur) {
tieCount++;
if (info->option->tieBreakMode == 0 &&
bdd_get_level_from_id(info->manager, i) <
bdd_get_level_from_id(info->manager, bestVar)) {
bestVar = i;
}
}
}
if (info->option->tieBreakMode == 1 && tieCount > 1) {
bestCost = IMG_TF_MAX_INT;
for (i = bestVar; i < nVars; i++) {
if (varOccur[i] != bestOccur)
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;
}
var = bdd_var_with_index(info->manager, i);
newCost = 0;
for (j = 0; j < array_n(delta); j++) {
comp = array_fetch(ImgComponent_t *, delta, j);
newCost += bdd_estimate_cofactor(comp->func, var, 1);
newCost += bdd_estimate_cofactor(comp->func, var, 0);
}
mdd_free(var);
if (newCost < bestCost) {
bestVar = i;
bestCost = newCost;
} else if (newCost == bestCost) {
if (bdd_get_level_from_id(info->manager, i) <
bdd_get_level_from_id(info->manager, bestVar)) {
bestVar = i;
}
}
}
}
break;
case 1: /* smallest support after splitting */
/* Find the variable which makes the smallest support after splitting */
bestCost = IMG_TF_MAX_INT;
varCost = ALLOC(int, nVars);
memset(varCost, 0, sizeof(int) * nVars);
for (i = 0; i < nVars; i++) {
if (varOccur[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;
}
var = bdd_var_with_index(info->manager, i);
varNot = mdd_not(var);
for (j = 0; j < array_n(delta); j++) {
comp = array_fetch(ImgComponent_t *, delta, j);
pcFunc = bdd_cofactor(comp->func, var);
varCost[i] += ImgCountBddSupports(pcFunc);
mdd_free(pcFunc);
ncFunc = bdd_cofactor(comp->func, varNot);
varCost[i] += ImgCountBddSupports(ncFunc);
mdd_free(ncFunc);
}
mdd_free(var);
mdd_free(varNot);
if (varCost[i] < bestCost) {
bestCost = varCost[i];
bestVar = i;
} else if (varCost[i] == bestCost) {
if (varOccur[i] < varOccur[bestVar]) {
bestVar = i;
} else if (varOccur[i] == varOccur[bestVar]) {
if (bdd_get_level_from_id(info->manager, i) <
bdd_get_level_from_id(info->manager, bestVar)) {
bestVar = i;
}
}
}
}
break;
case 2: /* smallest BDD size after splitting */
/* Find the variable which makes the smallest BDDs of all functions
after splitting */
bestCost = IMG_TF_MAX_INT;
varCost = ALLOC(int, nVars);
memset(varCost, 0, sizeof(int) * nVars);
for (i = 0; i < nVars; i++) {
if (varOccur[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;
}
var = bdd_var_with_index(info->manager, i);
for (j = 0; j < array_n(delta); j++) {
comp = array_fetch(ImgComponent_t *, delta, j);
varCost[i] += bdd_estimate_cofactor(comp->func, var, 1);
varCost[i] += bdd_estimate_cofactor(comp->func, var, 0);
}
mdd_free(var);
if (varCost[i] < bestCost) {
bestCost = varCost[i];
bestVar = i;
} else if (varCost[i] == bestCost) {
if (varOccur[i] < varOccur[bestVar]) {
bestVar = i;
} else if (varOccur[i] == varOccur[bestVar]) {
if (bdd_get_level_from_id(info->manager, i) <
bdd_get_level_from_id(info->manager, bestVar)) {
bestVar = i;
}
}
}
}
break;
case 3: /* top variable */
default:
for (i = 0; i < nVars; i++) {
if (varOccur[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 (bestVar == -1)
bestVar = i;
else if (bdd_get_level_from_id(info->manager, i) <
bdd_get_level_from_id(info->manager, bestVar)) {
bestVar = i;
}
}
}
FREE(varOccur);
if (varCost)
FREE(varCost);
} else {
bestComp = -1;
bestVar = -1;
switch (split) {
case 0: /* smallest BDD size */
bestCost = IMG_TF_MAX_INT;
imgComp = ImgComponentAlloc(info);
imgComp->func = img;
ImgComponentGetSupport(imgComp);
for (i = 0; i < array_n(delta); i++) {
comp = array_fetch(ImgComponent_t *, delta, i);
if (comp->intermediate)
continue;
index = (int)bdd_top_var_id(comp->var);
if (imgComp->support[index]) {
newCost = bdd_size(comp->func);
if (newCost < bestCost) {
bestComp = i;
bestCost = newCost;
}
}
}
imgComp->func = NIL(mdd_t);
ImgComponentFree(imgComp);
break;
case 1: /* largest BDD size */
bestCost = 0;
imgComp = ImgComponentAlloc(info);
imgComp->func = img;
ImgComponentGetSupport(imgComp);
for (i = 0; i < array_n(delta); i++) {
comp = array_fetch(ImgComponent_t *, delta, i);
if (comp->intermediate)
continue;
index = (int)bdd_top_var_id(comp->var);
if (imgComp->support[index]) {
newCost = bdd_size(comp->func);
if (newCost > bestCost) {
bestComp = i;
bestCost = newCost;
}
}
}
imgComp->func = NIL(mdd_t);
ImgComponentFree(imgComp);
break;
case 2: /* top variable */
default:
for (i = 0; i < array_n(delta); i++) {
comp = array_fetch(ImgComponent_t *, delta, i);
if (comp->intermediate)
continue;
index = (int)bdd_top_var_id(comp->var);
if (bestComp == -1 ||
bdd_get_level_from_id(info->manager, index) <
bdd_get_level_from_id(info->manager, bestVar)) {
bestVar = index;
bestComp = i;
}
}
break;
}
assert(bestComp != -1);
}
if (splitMethod == 0)
return(bestVar);
else
return(bestComp);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_t * PreImageDeleteOneComponent | ( | ImgTfmInfo_t * | info, |
| array_t * | delta, | ||
| int | index, | ||
| array_t ** | newDelta | ||
| ) | [static] |
Function********************************************************************
Synopsis [Deletes a component in a vector.]
Description [Deletes a component in a vector. Deletes index-th component out of delta and copy it into newDelta.]
SideEffects []
Definition at line 2145 of file imgTfmBwd.c.
{
int i;
ImgComponent_t *comp, *tmpComp;
bdd_t *func, *newFunc;
int preMinimize = info->option->preMinimize;
assert(array_n(delta) > 0);
comp = array_fetch(ImgComponent_t *, delta, index);
func = mdd_dup(comp->func);
*newDelta = array_alloc(ImgComponent_t *, 0);
for (i = 0; i < array_n(delta); i++) {
if (i != index) {
comp = array_fetch(ImgComponent_t *, delta, i);
tmpComp = ImgComponentCopy(info, comp);
if (preMinimize) {
newFunc = bdd_minimize(tmpComp->func, func);
if (mdd_equal(newFunc, tmpComp->func))
mdd_free(newFunc);
else {
mdd_free(tmpComp->func);
tmpComp->func = newFunc;
ImgSupportClear(info, tmpComp->support);
ImgComponentGetSupport(tmpComp);
}
}
array_insert_last(ImgComponent_t *, (*newDelta), tmpComp);
}
}
return(func);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_t * PreImageMakeRelationCanonical | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| bdd_t * | image, | ||
| array_t * | relationArray, | ||
| array_t ** | newVector, | ||
| array_t ** | newRelationArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Makes transition relation canonical for preimage.]
Description [Makes transition relation canonical for preimage. Quantifies out the next state variables that do not occur in the image, and when a vector exists, delete the components which do not appear in the image. If a component is constant, simplify the image with the constant value and delete the corresponding component from delta Side effect on delta. Return new image.]
SideEffects []
Definition at line 1863 of file imgTfmBwd.c.
{
array_t *tmpVector, *cofactoredVector;
bdd_t *simple, *tmp, *newImage;
ImgComponent_t *comp, *comp1, *imgComp;
int i, j, id;
mdd_t *cofactor, *abstract, *var, *nsVar;
array_t *tmpRelationArray;
int changed = 0;
mdd_t *yVarsCube, *rangeCube, *relation, *tmp2;
array_t *supportIds;
imgComp = ImgComponentAlloc(info);
imgComp->func = image;
ImgComponentGetSupport(imgComp);
if (vector) {
newImage = mdd_dup(image);
cofactor = mdd_one(info->manager);
abstract = mdd_one(info->manager);
if (info->nIntermediateVars) {
mdd_t *tmpCofactor, *tmpAbstract;
mdd_t *constIntermediate;
if (ImgExistConstIntermediateVar(vector)) {
constIntermediate = mdd_one(info->manager);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
if (mdd_is_tautology(comp->func, 1)) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
} else if (mdd_is_tautology(comp->func, 0)) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
}
}
}
cofactoredVector = ImgComposeConstIntermediateVars(info, vector,
constIntermediate,
&tmpCofactor,
&tmpAbstract,
NIL(mdd_t *),
&newImage);
if (!bdd_is_tautology(tmpCofactor, 1)) {
tmp = cofactor;
cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpCofactor);
if (!bdd_is_tautology(tmpAbstract, 1)) {
tmp = abstract;
abstract = mdd_and(tmp, tmpAbstract, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpAbstract);
mdd_free(constIntermediate);
} else
cofactoredVector = vector;
} else
cofactoredVector = vector;
/* Simplify image -- canonicalize vector */
tmpVector = array_alloc(ImgComponent_t *, 0);
for (i = 0; i < array_n(cofactoredVector); i++) {
comp = array_fetch(ImgComponent_t *, cofactoredVector, i);
if (comp->intermediate) {
comp1 = ImgComponentCopy(info, comp);
array_insert_last(ImgComponent_t *, tmpVector, comp1);
continue;
}
id = (int)bdd_top_var_id(comp->var);
if (!imgComp->support[id]) {
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
continue;
}
if (mdd_is_tautology(comp->func, 1)) {
changed = 1;
simple = bdd_cofactor(newImage, comp->var);
mdd_free(newImage);
newImage = simple;
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else if (mdd_is_tautology(comp->func, 0)) {
changed = 1;
tmp = mdd_not(comp->var);
simple = bdd_cofactor(newImage, tmp);
mdd_free(tmp);
mdd_free(newImage);
newImage = simple;
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
comp1 = ImgComponentCopy(info, comp);
array_insert_last(ImgComponent_t *, tmpVector, comp1);
}
}
if (cofactoredVector && cofactoredVector != vector)
ImgVectorFree(cofactoredVector);
if (changed) {
/* Now Simplify delta by deleting the non-affecting components */
*newVector = array_alloc(ImgComponent_t *, 0);
imgComp->func = NIL(mdd_t);
ImgComponentFree(imgComp);
imgComp = ImgComponentAlloc(info);
imgComp->func = newImage;
ImgSupportClear(info, imgComp->support);
ImgComponentGetSupport(imgComp);
for (i = 0; i < array_n(tmpVector); i++) {
comp = array_fetch(ImgComponent_t *, tmpVector, i);
id = (int)bdd_top_var_id(comp->var);
if (imgComp->support[id] || comp->intermediate)
array_insert_last(ImgComponent_t *, *newVector, comp);
else {
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
ImgComponentFree(comp);
}
}
array_free(tmpVector);
} else
*newVector = tmpVector;
} else {
newImage = image;
*newVector = vector;
cofactor = NIL(mdd_t);
abstract = NIL(mdd_t);
}
yVarsCube = mdd_one(info->manager);
for (i = 0; i < info->nVars; i++) {
if (imgComp->support[i]) {
imgComp->support[i] = 0;
if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
continue;
if (info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *))) {
continue;
}
var = bdd_var_with_index(info->manager, i);
nsVar = ImgSubstitute(var, info->functionData, Img_D2R_c);
mdd_free(var);
id = (int)bdd_top_var_id(nsVar);
imgComp->support[id] = 1;
tmp = yVarsCube;
yVarsCube = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
}
if (vector) {
for (i = 0; i < array_n(*newVector); i++) {
comp = array_fetch(ImgComponent_t *, *newVector, i);
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
id = (int)bdd_top_var_id(nsVar);
imgComp->support[id] = 2;
mdd_free(nsVar);
}
}
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
supportIds = mdd_get_bdd_support_ids(info->manager, relation);
for (j = 0; j < array_n(supportIds); j++) {
id = array_fetch(int, supportIds, j);
imgComp->support[id] = 2;
}
array_free(supportIds);
}
for (i = 0; i < info->nVars; i++) {
if (imgComp->support[i] == 1) {
nsVar = bdd_var_with_index(info->manager, i);
var = ImgSubstitute(nsVar, info->functionData, Img_R2D_c);
mdd_free(nsVar);
tmp = newImage;
newImage = bdd_smooth_with_cube(tmp, var);
if (tmp != image)
mdd_free(tmp);
mdd_free(var);
}
}
imgComp->func = NIL(mdd_t);
ImgComponentFree(imgComp);
if (bdd_get_package_name() == CUDD)
rangeCube = info->functionData->rangeCube;
else {
rangeCube = mdd_one(info->manager);
for (i = 0; i < array_n(info->functionData->rangeBddVars); i++) {
var = array_fetch(mdd_t *, info->functionData->rangeBddVars, i);
tmp = rangeCube;
rangeCube = mdd_and(tmp, var, 1, 1);
mdd_free(tmp);
}
}
cofactor = NIL(mdd_t);
if (abstract) {
tmp2 = bdd_smooth_with_cube(rangeCube, yVarsCube);
tmp = abstract;
abstract = mdd_and(tmp, tmp2, 1, 1);
mdd_free(tmp);
mdd_free(tmp2);
} else
abstract = bdd_smooth_with_cube(rangeCube, yVarsCube);
mdd_free(yVarsCube);
if (rangeCube != info->functionData->rangeCube)
mdd_free(rangeCube);
*newRelationArray = relationArray;
if (cofactor) {
if (!bdd_is_tautology(cofactor, 1)) {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray,
cofactor);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
}
mdd_free(cofactor);
}
if (bdd_is_tautology(abstract, 1))
mdd_free(abstract);
else {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetAbstractedRelationArray(info->manager,
tmpRelationArray,
abstract);
mdd_free(abstract);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
}
return(newImage);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_t * PreImageMakeVectorCanonical | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| bdd_t * | image, | ||
| array_t * | relationArray, | ||
| array_t ** | newVector, | ||
| array_t ** | newRelationArray, | ||
| mdd_t ** | cofactorCube, | ||
| mdd_t ** | abstractCube | ||
| ) | [static] |
Function********************************************************************
Synopsis [Makes a vector canonical for preimage.]
Description [Makes a vector canonical for preimage. Delete all the components which doesn't appear as a support in the image. If a component is constant, simplify the image with the constant value and delete the corresponding component from delta Side effect on delta. Return new image.]
SideEffects []
Definition at line 1612 of file imgTfmBwd.c.
{
array_t *tmpVector, *cofactoredVector;
bdd_t *simple, *tmp, *newImage;
ImgComponent_t *comp, *comp1, *imgComp;
int i, id, n, pos;
st_table *equivTable;
int *ptr, *regularPtr;
mdd_t *var, *cofactor, *abstract, *nsVar;
array_t *tmpRelationArray;
int changed = 0;
newImage = mdd_dup(image);
imgComp = ImgComponentAlloc(info);
imgComp->func = image;
ImgComponentGetSupport(imgComp);
if (relationArray) {
cofactor = mdd_one(info->manager);
abstract = mdd_one(info->manager);
} else {
cofactor = NIL(mdd_t);
abstract = NIL(mdd_t);
}
if (info->nIntermediateVars) {
mdd_t *tmpCofactor, *tmpAbstract;
mdd_t *constIntermediate;
if (ImgExistConstIntermediateVar(vector)) {
constIntermediate = mdd_one(info->manager);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
if (mdd_is_tautology(comp->func, 1)) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
} else if (mdd_is_tautology(comp->func, 0)) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
}
}
}
if (relationArray) {
cofactoredVector = ImgComposeConstIntermediateVars(info, vector,
constIntermediate,
&tmpCofactor, &tmpAbstract,
NIL(mdd_t *), &newImage);
if (!bdd_is_tautology(tmpCofactor, 1)) {
tmp = cofactor;
cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpCofactor);
if (!bdd_is_tautology(tmpAbstract, 1)) {
tmp = abstract;
abstract = mdd_and(tmp, tmpAbstract, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpAbstract);
} else {
cofactoredVector = ImgComposeConstIntermediateVars(info, vector,
constIntermediate,
NIL(mdd_t *), NIL(mdd_t *),
NIL(mdd_t *), &newImage);
}
mdd_free(constIntermediate);
} else
cofactoredVector = vector;
} else
cofactoredVector = vector;
/* Simplify image -- canonicalize the image first */
n = 0;
equivTable = st_init_table(st_ptrcmp, st_ptrhash);
tmpVector = array_alloc(ImgComponent_t *, 0);
for (i = 0; i < array_n(cofactoredVector); i++) {
comp = array_fetch(ImgComponent_t *, cofactoredVector, i);
if (comp->intermediate) {
comp1 = ImgComponentCopy(info, comp);
array_insert_last(ImgComponent_t *, tmpVector, comp1);
n++;
continue;
}
id = (int)bdd_top_var_id(comp->var);
if (!imgComp->support[id]) {
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
continue;
}
if (mdd_is_tautology(comp->func, 1)) {
changed = 1;
simple = bdd_cofactor(newImage, comp->var);
mdd_free(newImage);
newImage = simple;
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else if (mdd_is_tautology(comp->func, 0)) {
changed = 1;
tmp = mdd_not(comp->var);
simple = bdd_cofactor(newImage, tmp);
mdd_free(tmp);
mdd_free(newImage);
newImage = simple;
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
ptr = (int *)bdd_pointer(comp->func);
regularPtr = (int *)((unsigned long)ptr & ~01);
if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
changed = 1;
comp1 = array_fetch(ImgComponent_t *, tmpVector, pos);
if (mdd_equal(comp->func, comp1->func)) {
tmp = newImage;
newImage = bdd_compose(tmp, comp->var, comp1->var);
mdd_free(tmp);
} else {
tmp = newImage;
var = mdd_not(comp1->var);
newImage = bdd_compose(tmp, comp->var, var);
mdd_free(tmp);
mdd_free(var);
}
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
comp1 = ImgComponentCopy(info, comp);
array_insert_last(ImgComponent_t *, tmpVector, comp1);
st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
n++;
}
}
}
st_free_table(equivTable);
if (cofactoredVector && cofactoredVector != vector)
ImgVectorFree(cofactoredVector);
if (changed) {
/* Now Simplify delta by deleting the non-affecting components */
*newVector = array_alloc(ImgComponent_t *, 0);
imgComp->func = NIL(mdd_t);
ImgComponentFree(imgComp);
imgComp = ImgComponentAlloc(info);
imgComp->func = newImage;
ImgSupportClear(info, imgComp->support);
ImgComponentGetSupport(imgComp);
for (i = 0; i < array_n(tmpVector); i++) {
comp = array_fetch(ImgComponent_t *, tmpVector, i);
id = (int)bdd_top_var_id(comp->var);
if (imgComp->support[id] || comp->intermediate)
array_insert_last(ImgComponent_t *, *newVector, comp);
else {
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
ImgComponentFree(comp);
}
}
array_free(tmpVector);
} else
*newVector = tmpVector;
imgComp->func = NIL(mdd_t);
ImgComponentFree(imgComp);
if (newRelationArray)
*newRelationArray = relationArray;
if (cofactor) {
if (cofactorCube)
*cofactorCube = cofactor;
else {
if (!bdd_is_tautology(cofactor, 1)) {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray,
cofactor);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
}
mdd_free(cofactor);
}
}
if (abstract) {
if (abstractCube)
*abstractCube = abstract;
else {
if (bdd_is_tautology(abstract, 1))
mdd_free(abstract);
else {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetAbstractedRelationArray(info->manager,
tmpRelationArray,
abstract);
mdd_free(abstract);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
}
}
}
assert(CheckPreImageVector(info, *newVector, newImage));
return(newImage);
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: imgTfmBwd.c,v 1.29 2002/08/18 04:47:07 fabio Exp $" [static] |
CFile***********************************************************************
FileName [imgTfmBwd.c]
PackageName [img]
Synopsis [Routines for preimage computation using transition function method.]
Description []
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 38 of file imgTfmBwd.c.
