#include "imgInt.h"
Include dependency graph for imgTfmFwd.c:
Go to the source code of this file.
Functions | |
| static mdd_t * | ImageByInputSplit (ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int splitMethod, int turnDepth, int depth) |
| static mdd_t * | ImageByStaticInputSplit (ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth) |
| static mdd_t * | ImageByOutputSplit (ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, int depth) |
| static int | ImageDecomposeAndChooseSplitVar (ImgTfmInfo_t *info, array_t *vector, mdd_t *from, int splitMethod, int split, int piSplitFlag, array_t *vectorArray, array_t *varArray, mdd_t **singles, array_t *relationArray, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube) |
| static mdd_t * | ImageFast2 (ImgTfmInfo_t *info, array_t *vector) |
| static int | FindDecomposableVariable (ImgTfmInfo_t *info, array_t *vector) |
| static int | TfmCheckImageValidity (ImgTfmInfo_t *info, mdd_t *image) |
| static void | FindIntermediateSupport (array_t *vector, ImgComponent_t *comp, int nVars, int nGroups, int *stack, char *stackFlag, int *funcGroup, int *size, char *intermediateVarFlag, int *intermediateVarFuncMap) |
| static void | PrintVectorDecomposition (ImgTfmInfo_t *info, array_t *vectorArray, array_t *varArray) |
| static int | CheckIfValidSplitOrGetNew (ImgTfmInfo_t *info, int split, array_t *vector, array_t *relationArray, mdd_t *from) |
| static int | ChooseInputSplittingVariable (ImgTfmInfo_t *info, array_t *vector, mdd_t *from, int splitMethod, int decompose, int piSplitFlag, int *varOccur) |
| static int | ChooseOutputSplittingVariable (ImgTfmInfo_t *info, array_t *vector, int splitMethod) |
| mdd_t * | ImgTfmImage (ImgTfmInfo_t *info, mdd_t *from) |
| mdd_t * | ImgChooseTrSplitVar (ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, int trSplitMethod, int piSplitFlag) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: imgTfmFwd.c,v 1.37 2005/04/22 19:45:46 jinh Exp $" |
Function Documentation
| static int CheckIfValidSplitOrGetNew | ( | ImgTfmInfo_t * | info, |
| int | split, | ||
| array_t * | vector, | ||
| array_t * | relationArray, | ||
| mdd_t * | from | ||
| ) | [static] |
Function********************************************************************
Synopsis [Checks the splitting variable is valid and chooses new one if not valid.]
Description [Checks the splitting variable is already quantified from the transition relation. If yes, chooses new splitting variable. If there is no valid splitting variable, returns -1.]
SideEffects []
Definition at line 2983 of file imgTfmFwd.c.
{
int newSplit = split;
int i, j, nVars;
ImgComponent_t *comp;
char *support;
int *varOccur;
int decompose;
nVars = info->nVars;
support = ALLOC(char, sizeof(char) * nVars);
memset(support, 0, sizeof(char) * nVars);
comp = ImgComponentAlloc(info);
for (i = 0; i < array_n(relationArray); i++) {
comp->func = array_fetch(mdd_t *, relationArray, i);;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
for (j = 0; j < nVars; j++) {
if (comp->support[j]) {
if (j == split) {
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
FREE(support);
return(split);
}
support[j] = 1;
}
}
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
if (info->useConstraint && from)
decompose = 0;
else
decompose = 1;
varOccur = ALLOC(int, nVars);
memset(varOccur, 0, sizeof(int) * nVars);
if (from) {
comp = ImgComponentAlloc(info);
comp->func = from;
ImgComponentGetSupport(comp);
for (i = 0; i < nVars; i++) {
if (comp->support[i])
varOccur[i]++;
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
}
FREE(support);
newSplit = ChooseInputSplittingVariable(info, vector, from,
info->option->inputSplit, decompose,
info->option->piSplitFlag, varOccur);
FREE(varOccur);
return(newSplit);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int ChooseInputSplittingVariable | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from, | ||
| int | splitMethod, | ||
| int | decompose, | ||
| int | piSplitFlag, | ||
| int * | varOccur | ||
| ) | [static] |
Function********************************************************************
Synopsis [Finds a splitting variable for input splitting.]
Description [Finds a splitting variable for input splitting.]
SideEffects []
Definition at line 3060 of file imgTfmFwd.c.
{
int nVars = info->nVars;
int bestVar = -1;
int secondBestVar = -1;
int bestCost, newCost;
int bestOccur, tieCount;
int secondBestOccur, secondTieCount;
int i, j;
ImgComponent_t *comp;
mdd_t *var, *varNot, *pcFunc, *ncFunc;
int *varCost;
int size = ImgVectorFunctionSize(vector);
if (info->option->inputSplit > 0) {
varCost = ALLOC(int, nVars);
memset(varCost, 0, sizeof(int) * nVars);
} else
varCost = NIL(int);
switch (splitMethod) {
case 0:
/* Find the most frequently occurred variable */
bestOccur = 0;
tieCount = 0;
secondBestOccur = 0;
secondTieCount = 0;
for (i = 0; i < nVars; i++) {
if (varOccur[i] == 0)
continue;
if (piSplitFlag == 0) {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *))) {
if ((bestOccur == 0 && secondBestOccur == 0) ||
(varOccur[i] > bestOccur && varOccur[i] > secondBestOccur)) {
secondBestOccur = varOccur[i];
secondBestVar = i;
secondTieCount = 1;
} else if (secondBestOccur > bestOccur &&
varOccur[i] == secondBestOccur) {
secondTieCount++;
if (info->option->tieBreakMode == 0 &&
bdd_get_level_from_id(info->manager, i) <
bdd_get_level_from_id(info->manager, secondBestVar)) {
secondBestVar = i;
}
}
continue;
}
}
if (size < array_n(vector) &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *))) {
continue;
}
if (bestOccur == 0 || varOccur[i] > bestOccur) {
bestOccur = varOccur[i];
bestVar = 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 (piSplitFlag == 0 && bestVar == -1) {
bestVar = secondBestVar;
bestOccur = secondBestOccur;
tieCount = secondTieCount;
}
if (info->option->tieBreakMode == 1 && tieCount > 1) {
bestCost = IMG_TF_MAX_INT;
for (i = bestVar; i < nVars; i++) {
if (varOccur[i] != bestOccur)
continue;
if (size < array_n(vector) &&
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(vector); j++) {
comp = array_fetch(ImgComponent_t *, vector, j);
newCost += bdd_estimate_cofactor(comp->func, var, 1);
newCost += bdd_estimate_cofactor(comp->func, var, 0);
}
if (decompose == 0) {
newCost += bdd_estimate_cofactor(from, var, 1);
newCost += bdd_estimate_cofactor(from, 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:
/* Find the variable which makes the smallest support after splitting */
bestCost = IMG_TF_MAX_INT;
for (i = 0; i < nVars; i++) {
if (varOccur[i] == 0)
continue;
if (size < array_n(vector) &&
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(vector); j++) {
comp = array_fetch(ImgComponent_t *, vector, 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);
}
if (decompose == 0) {
pcFunc = bdd_cofactor(from, var);
varCost[i] += ImgCountBddSupports(pcFunc);
mdd_free(pcFunc);
ncFunc = bdd_cofactor(from, 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:
/* Find the variable which makes the smallest BDDs of all functions
after splitting */
bestCost = IMG_TF_MAX_INT;
for (i = 0; i < nVars; i++) {
if (varOccur[i] == 0)
continue;
if (size < array_n(vector) &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *))) {
continue;
}
var = bdd_var_with_index(info->manager, i);
for (j = 0; j < array_n(vector); j++) {
comp = array_fetch(ImgComponent_t *, vector, j);
varCost[i] += bdd_estimate_cofactor(comp->func, var, 1);
varCost[i] += bdd_estimate_cofactor(comp->func, var, 0);
}
if (decompose == 0) {
varCost[i] += bdd_estimate_cofactor(from, var, 1);
varCost[i] += bdd_estimate_cofactor(from, 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 */
for (i = 0; i < nVars; i++) {
if (varOccur[i] == 0)
continue;
if (size < array_n(vector) &&
st_lookup(info->intermediateVarsTable, (char *)(long)i,
NIL(char *))) {
continue;
}
if (piSplitFlag == 0) {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
NIL(char *))) {
if (bestVar == -1 && secondBestVar == -1)
secondBestVar = i;
else if (bdd_get_level_from_id(info->manager, i) <
bdd_get_level_from_id(info->manager, secondBestVar)) {
secondBestVar = i;
}
continue;
}
}
if (bestVar == -1 ||
bdd_get_level_from_id(info->manager, i) <
bdd_get_level_from_id(info->manager, bestVar)) {
bestVar = i;
}
}
if (piSplitFlag == 0 && bestVar == -1)
bestVar = secondBestVar;
break;
default:
break;
}
if (varCost)
FREE(varCost);
return(bestVar);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int ChooseOutputSplittingVariable | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| int | splitMethod | ||
| ) | [static] |
Function********************************************************************
Synopsis [Finds a splitting variable for output splitting.]
Description [Finds a splitting variable for output splitting.]
SideEffects []
Definition at line 3311 of file imgTfmFwd.c.
{
int bestVar = -1;
int bestCost, newCost;
int i;
ImgComponent_t *comp;
int size = ImgVectorFunctionSize(vector);
int index;
switch (splitMethod) {
case 0: /* smallest */
bestCost = IMG_TF_MAX_INT;
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (size < array_n(vector) &&
st_lookup(info->intermediateVarsTable,
(char *)(long)bdd_top_var_id(comp->var), NIL(char *))) {
continue;
}
newCost = bdd_size(comp->func);
if (newCost < bestCost) {
bestVar = i;
bestCost = newCost;
}
}
break;
case 1: /* largest */
bestCost = 0;
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (size < array_n(vector) &&
st_lookup(info->intermediateVarsTable,
(char *)(long)bdd_top_var_id(comp->var), NIL(char *))) {
continue;
}
newCost = bdd_size(comp->func);
if (newCost > bestCost) {
bestVar = i;
bestCost = newCost;
}
}
break;
case 2: /* top variable */
default:
comp = array_fetch(ImgComponent_t *, vector, 0);
bestVar = (int)bdd_top_var_id(comp->var);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
index = (int)bdd_top_var_id(comp->var);
if (size < array_n(vector) &&
st_lookup(info->intermediateVarsTable, (char *)(long)index,
NIL(char *))) {
continue;
}
if (bestVar == -1 ||
bdd_get_level_from_id(info->manager, index) <
bdd_get_level_from_id(info->manager, bestVar)) {
bestVar = i;
}
}
break;
}
return(bestVar);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int FindDecomposableVariable | ( | ImgTfmInfo_t * | info, |
| array_t * | vector | ||
| ) | [static] |
Function********************************************************************
Synopsis [Finds a decomposable variable (articulation)]
Description [Finds a decomposable variable (articulation)]
SideEffects []
Definition at line 2716 of file imgTfmFwd.c.
{
int i, j, f, split;
int nChosen, index, varId;
int nVars, nFuncs;
char *varFlag;
int *funcGroup;
int *stack, size;
ImgComponent_t *comp;
char *stackFlag;
char *support;
int arraySize;
char *intermediateVarFlag;
int *intermediateVarFuncMap;
arraySize = array_n(vector);
if (info->nIntermediateVars)
nFuncs = ImgVectorFunctionSize(vector);
else
nFuncs = arraySize;
nVars = info->nVars;
funcGroup = ALLOC(int, arraySize);
varFlag = ALLOC(char, nVars);
stack = ALLOC(int, arraySize);
stackFlag = ALLOC(char, arraySize);
if (arraySize > nFuncs) {
intermediateVarFlag = ALLOC(char, nVars);
memset(intermediateVarFlag, 0, sizeof(char) * nVars);
intermediateVarFuncMap = ALLOC(int, nVars);
memset(intermediateVarFuncMap, 0, sizeof(int) * nVars);
for (i = 0; i < arraySize; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
index = (int)bdd_top_var_id(comp->var);
intermediateVarFlag[index] = 1;
intermediateVarFuncMap[index] = i;
}
}
} else {
intermediateVarFlag = NIL(char);
intermediateVarFuncMap = NIL(int);
}
varId = -1;
for (split = 0; split < nVars; split++) {
if (intermediateVarFlag[split])
continue;
memset(funcGroup, 0, sizeof(int) * arraySize);
memset(varFlag, 0, sizeof(char) * nVars);
memset(stackFlag, 0, sizeof(char) * arraySize);
varFlag[split] = 1;
nChosen = 0;
stack[0] = 0;
size = 1;
stackFlag[0] = 1;
while (size) {
size--;
f = stack[size];
funcGroup[f] = 1;
comp = array_fetch(ImgComponent_t *, vector, f);
nChosen++;
if (nChosen == arraySize)
break;
support = comp->support;
if (comp->intermediate) {
index = (int)bdd_top_var_id(comp->var);
support[index] = 1;
}
for (i = 0; i < nVars; i++) {
if (!support[i])
continue;
if (varFlag[i])
continue;
varFlag[i] = 1;
for (j = 0; j < nFuncs; j++) {
if (j == f || stackFlag[j])
continue;
comp = array_fetch(ImgComponent_t *, vector, j);
if (arraySize != nFuncs) {
if (intermediateVarFlag[i] && comp->intermediate) {
index = (int)bdd_top_var_id(comp->var);
if (index == i) {
if (funcGroup[j] == 0) {
stack[size] = j;
size++;
stackFlag[j] = 1;
}
FindIntermediateSupport(vector, comp, nVars, 0,
stack, stackFlag, funcGroup, &size,
intermediateVarFlag,
intermediateVarFuncMap);
continue;
}
}
}
if (funcGroup[j])
continue;
if (comp->support[i]) {
stack[size] = j;
size++;
stackFlag[j] = 1;
}
}
}
if (comp->intermediate) {
index = (int)bdd_top_var_id(comp->var);
support[index] = 0;
}
}
if (nChosen < nFuncs) {
varId = split;
break;
}
}
FREE(stackFlag);
FREE(stack);
FREE(funcGroup);
FREE(varFlag);
if (arraySize > nFuncs) {
FREE(intermediateVarFlag);
FREE(intermediateVarFuncMap);
}
return(varId);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FindIntermediateSupport | ( | array_t * | vector, |
| ImgComponent_t * | comp, | ||
| int | nVars, | ||
| int | nGroups, | ||
| int * | stack, | ||
| char * | stackFlag, | ||
| int * | funcGroup, | ||
| int * | size, | ||
| char * | intermediateVarFlag, | ||
| int * | intermediateVarFuncMap | ||
| ) | [static] |
Function********************************************************************
Synopsis [Finds all other fanin intermediate functions of a given intermediate function.]
Description [Finds all other fanin intermediate functions of a given intermediate function. Adds the only intermediate functions are not in the stack. Updates the stack information.]
SideEffects []
Definition at line 2907 of file imgTfmFwd.c.
{
int i, f;
ImgComponent_t *intermediateComp;
for (i = 0; i < nVars; i++) {
if (comp->support[i]) {
if (intermediateVarFlag[i]) {
f = intermediateVarFuncMap[i];
if (stackFlag[f] || funcGroup[f] == nGroups + 1)
continue;
stack[*size] = f;
(*size)++;
stackFlag[f] = 1;
intermediateComp = array_fetch(ImgComponent_t *, vector, f);
FindIntermediateSupport(vector, intermediateComp, nVars, nGroups,
stack, stackFlag, funcGroup, size,
intermediateVarFlag, intermediateVarFuncMap);
}
}
}
}
Here is the caller graph for this function:
| static mdd_t * ImageByInputSplit | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | constraint, | ||
| mdd_t * | from, | ||
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube, | ||
| int | splitMethod, | ||
| int | turnDepth, | ||
| int | depth | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Computes an image by input splitting.]
Description [Computes an image by input splitting.]
SideEffects []
Definition at line 638 of file imgTfmFwd.c.
{
array_t *newVector, *tmpVector;
mdd_t *new_, *resT, *resE, *res, *resPart, *resTmp;
mdd_t *var, *varNot, *cube, *tmp, *func;
int size, i, j, k, vectorSize;
array_t *vectorArray, *varArray;
int hit, turnFlag;
int split, nGroups, cubeSize;
mdd_t *refResult, *product;
mdd_t *newFrom, *fromT, *fromE;
ImgComponent_t *comp;
array_t *relationArrayT, *relationArrayE, *partRelationArray;
int constConstrain;
int nRecur;
array_t *newRelationArray, *tmpRelationArray, *abstractVars;
mdd_t *cofactor, *abstract;
mdd_t *newCofactorCube, *newAbstractCube;
mdd_t *partCofactorCube, *partAbstractCube;
mdd_t *cofactorCubeT, *cofactorCubeE;
mdd_t *abstractCubeT, *abstractCubeE;
mdd_t *essentialCube, *tmpRes;
int findEssential;
int foundEssentialDepth;
int foundEssentialDepthT, foundEssentialDepthE;
array_t *vectorT, *vectorE;
mdd_t *andT, *andE, *one;
float prevLambda;
int prevTotal, prevVectorBddSize, prevVectorSize;
int arraySize, nFuncs;
newRelationArray = NIL(array_t);
if (info->option->delayedSplit && relationArray) {
ImgVectorConstrain(info, vector, constraint, relationArray,
&newVector, &res, &newRelationArray,
&cofactor, &abstract, TRUE);
newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1);
mdd_free(cofactor);
newAbstractCube = mdd_and(abstractCube, abstract, 1, 1);
mdd_free(abstract);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, from);
resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
newRelationArray,
newCofactorCube,
newAbstractCube);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
mdd_free(resPart);
}
} else {
ImgVectorConstrain(info, vector, constraint, relationArray,
&newVector, &res, &newRelationArray,
NIL(mdd_t *), NIL(mdd_t *), TRUE);
newCofactorCube = NIL(mdd_t);
newAbstractCube = NIL(mdd_t);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, from);
resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
newRelationArray,
NIL(mdd_t), NIL(mdd_t));
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
relationArray,
NIL(mdd_t), NIL(mdd_t));
resTmp = mdd_and(resPart, res, 1, 1);
mdd_free(resPart);
assert(mdd_equal(refResult, resTmp));
mdd_free(refResult);
mdd_free(resTmp);
}
}
if (info->option->checkEquivalence &&
relationArray && !info->option->buildPartialTR) {
assert(ImgCheckEquivalence(info, newVector, newRelationArray,
newCofactorCube, newAbstractCube, 0));
}
if (from && 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;
info->nFoundEssentials++;
if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
info->foundEssentials[depth]++;
tmpVector = newVector;
tmpRelationArray = newRelationArray;
if (info->option->delayedSplit && relationArray) {
ImgVectorMinimize(info, tmpVector, essentialCube, NIL(mdd_t),
tmpRelationArray, &newVector, &tmpRes,
&newRelationArray, &cofactor, &abstract);
tmp = newCofactorCube;
newCofactorCube = mdd_and(tmp, cofactor, 1, 1);
mdd_free(tmp);
mdd_free(cofactor);
tmp = newAbstractCube;
newAbstractCube = mdd_and(tmp, abstract, 1, 1);
mdd_free(tmp);
mdd_free(abstract);
} else {
ImgVectorMinimize(info, tmpVector, essentialCube, NIL(mdd_t),
tmpRelationArray, &newVector, &tmpRes,
&newRelationArray, NIL(mdd_t *), NIL(mdd_t *));
}
tmp = res;
res = mdd_and(tmp, tmpRes, 1, 1);
mdd_free(tmp);
ImgVectorFree(tmpVector);
if (tmpRelationArray && tmpRelationArray != relationArray &&
tmpRelationArray != newRelationArray)
mdd_array_free(tmpRelationArray);
foundEssentialDepth = depth;
} else
foundEssentialDepth = info->option->maxEssentialDepth;
mdd_free(essentialCube);
foundEssentialDepthT = info->option->maxEssentialDepth;
foundEssentialDepthE = info->option->maxEssentialDepth;
} else {
/* To remove compiler warnings */
foundEssentialDepth = -1;
foundEssentialDepthT = -1;
foundEssentialDepthE = -1;
}
if (info->option->debug) {
if (relationArray && from) {
refResult = ImgImageByHybrid(info, newVector, from);
resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
newRelationArray,
newCofactorCube,
newAbstractCube);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
mdd_free(resPart);
}
}
info->nRecursion++;
arraySize = array_n(newVector);
if (info->nIntermediateVars)
nFuncs = ImgVectorFunctionSize(newVector);
else
nFuncs = arraySize;
if (nFuncs <= 1) {
if (info->useConstraint) {
if (nFuncs == 1) {
comp = array_fetch(ImgComponent_t *, newVector, 0);
if (arraySize > 1)
func = ImgGetComposedFunction(newVector);
else
func = comp->func;
if (mdd_lequal(from, func, 1, 1)) { /* func | from = 1 */
tmp = res;
res = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
} else if (mdd_lequal(func, from, 1, 0)) { /* func | from = 0 */
tmp = res;
res = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
}
if (arraySize > 1)
mdd_free(func);
}
}
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube)
mdd_free(newAbstractCube);
ImgVectorFree(newVector);
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
if (info->option->debug)
assert(TfmCheckImageValidity(info, res));
return(res);
}
turnFlag = 0;
if (splitMethod == 3 && turnDepth == -1) {
if (depth < info->option->splitMinDepth) {
info->nSplits++;
turnFlag = 0;
} else if (depth > info->option->splitMaxDepth) {
info->nConjoins++;
turnFlag = 1;
} else {
turnFlag = ImgDecideSplitOrConjoin(info, newVector, from, 0,
newRelationArray, newCofactorCube,
newAbstractCube, 0, depth);
}
} else {
if (splitMethod != 0) {
if (depth == turnDepth)
turnFlag = 1;
}
}
if (turnFlag || nFuncs == 2) {
hit = 1;
if (!info->imgCache ||
!(resPart = ImgCacheLookupTable(info, info->imgCache, newVector,
from))) {
hit = 0;
if (nFuncs == 2) {
if (info->useConstraint) {
ImgVectorConstrain(info, newVector, from, NIL(array_t),
&tmpVector, &resTmp, NIL(array_t *),
NIL(mdd_t *), NIL(mdd_t *), FALSE);
if (array_n(tmpVector) <= 1)
resPart = resTmp;
else {
mdd_free(resTmp);
resPart = ImageFast2(info, tmpVector);
}
ImgVectorFree(tmpVector);
} else
resPart = ImageFast2(info, newVector);
} else if (splitMethod == 2) {
if (info->useConstraint) {
ImgVectorConstrain(info, newVector, from, NIL(array_t),
&tmpVector, &resTmp, NIL(array_t *),
NIL(mdd_t *), NIL(mdd_t *), FALSE);
if (array_n(tmpVector) <= 1)
resPart = resTmp;
else if (array_n(tmpVector) == 2) {
mdd_free(resTmp);
resPart = ImageFast2(info, tmpVector);
} else {
tmp = mdd_one(info->manager);
resPart = ImageByOutputSplit(info, tmpVector, tmp, depth + 1);
mdd_free(tmp);
tmp = resPart;
resPart = mdd_and(tmp, resTmp, 1, 1);
mdd_free(tmp);
mdd_free(resTmp);
}
ImgVectorFree(tmpVector);
} else {
tmp = mdd_one(info->manager);
resPart = ImageByOutputSplit(info, newVector, tmp, depth + 1);
mdd_free(tmp);
}
} else {
if (relationArray) {
resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
newRelationArray,
newCofactorCube,
newAbstractCube);
} else
resPart = ImgImageByHybrid(info, newVector, from);
}
if (info->imgCache) {
if (from) {
ImgCacheInsertTable(info->imgCache, newVector, mdd_dup(from),
resPart);
} else
ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t), resPart);
}
}
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube)
mdd_free(newAbstractCube);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, from);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
}
new_ = mdd_and(res, resPart, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(resPart), size);
}
}
mdd_free(res);
res = new_;
if (!info->imgCache || hit) {
mdd_free(resPart);
ImgVectorFree(newVector);
}
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
if (turnFlag)
info->nTurns++;
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
if (info->option->debug)
assert(TfmCheckImageValidity(info, res));
return(res);
}
if (info->imgCache) {
resPart = ImgCacheLookupTable(info, info->imgCache, newVector, from);
if (resPart) {
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, from);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
}
new_ = mdd_and(res, resPart, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(resPart), size);
}
}
mdd_free(res);
mdd_free(resPart);
res = new_;
ImgVectorFree(newVector);
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube)
mdd_free(newAbstractCube);
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
if (info->option->debug)
assert(TfmCheckImageValidity(info, res));
return(res);
}
}
if (info->option->splitCubeFunc) {
split = -1;
cubeSize = 0;
for (i = 0; i < array_n(newVector); i++) {
comp = array_fetch(ImgComponent_t *, newVector, i);
if (bdd_is_cube(comp->func)) {
if (split == -1 || info->option->splitCubeFunc == 1 ||
bdd_size(comp->func) > cubeSize) {
split = i;
cubeSize = bdd_size(comp->func);
break;
}
}
}
if (split != -1) {
comp = array_fetch(ImgComponent_t *, newVector, split);
info->nCubeSplits++;
if (info->option->delayedSplit && relationArray) {
ImgVectorConstrain(info, newVector, comp->func, newRelationArray,
&vectorT, &andT, &relationArrayT,
&cofactor, &abstract, FALSE);
cofactorCubeT = mdd_and(newCofactorCube, cofactor, 1, 1);
mdd_free(cofactor);
abstractCubeT = mdd_and(newAbstractCube, abstract, 1, 1);
mdd_free(abstract);
} else {
ImgVectorConstrain(info, newVector, comp->func, newRelationArray,
&vectorT, &andT, &relationArrayT,
NIL(mdd_t *), NIL(mdd_t *), FALSE);
cofactorCubeT = NIL(mdd_t);
abstractCubeT = NIL(mdd_t);
}
if (from)
newFrom = bdd_cofactor(from, comp->func);
else
newFrom = from;
if (info->option->checkEquivalence &&
relationArray && !info->option->buildPartialTR) {
assert(ImgCheckEquivalence(info, vectorT, relationArrayT,
cofactorCubeT, abstractCubeT, 0));
}
one = mdd_one(info->manager);
if (newFrom && bdd_is_tautology(newFrom, 0))
resT = mdd_zero(info->manager);
else {
prevLambda = info->prevLambda;
prevTotal = info->prevTotal;
prevVectorBddSize = info->prevVectorBddSize;
prevVectorSize = info->prevVectorSize;
resT = ImageByInputSplit(info, vectorT, one, newFrom,
relationArrayT, cofactorCubeT, abstractCubeT,
splitMethod, turnDepth, depth + 1);
info->prevLambda = prevLambda;
info->prevTotal = prevTotal;
info->prevVectorBddSize = prevVectorBddSize;
info->prevVectorSize = prevVectorSize;
}
ImgVectorFree(vectorT);
if (newFrom)
mdd_free(newFrom);
if (!bdd_is_tautology(andT, 1)) {
tmp = resT;
resT = mdd_and(tmp, andT, 1, 1);
mdd_free(tmp);
}
if (findEssential)
foundEssentialDepthT = info->foundEssentialDepth;
if (relationArrayT && relationArrayT != newRelationArray)
mdd_array_free(relationArrayT);
if (cofactorCubeT && cofactorCubeT != newCofactorCube)
mdd_free(cofactorCubeT);
if (abstractCubeT && abstractCubeT != newAbstractCube)
mdd_free(abstractCubeT);
tmp = mdd_not(comp->func);
if (info->option->delayedSplit && relationArray) {
ImgVectorConstrain(info, newVector, tmp, newRelationArray,
&vectorE, &andE, &relationArrayE,
&cofactor, &abstract, FALSE);
cofactorCubeE = mdd_and(newCofactorCube, cofactor, 1, 1);
mdd_free(cofactor);
abstractCubeE = mdd_and(newAbstractCube, abstract, 1, 1);
mdd_free(abstract);
} else {
ImgVectorConstrain(info, newVector, tmp, newRelationArray,
&vectorE, &andE, &relationArrayE,
NIL(mdd_t *), NIL(mdd_t *), FALSE);
cofactorCubeE = NIL(mdd_t);
abstractCubeE = NIL(mdd_t);
}
if (from)
newFrom = bdd_cofactor(from, tmp);
else
newFrom = from;
mdd_free(tmp);
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube)
mdd_free(newAbstractCube);
if (info->option->checkEquivalence &&
relationArray && !info->option->buildPartialTR) {
assert(ImgCheckEquivalence(info, vectorE, relationArrayE,
cofactorCubeE, abstractCubeE, 0));
}
if (newFrom && bdd_is_tautology(newFrom, 0))
resE = mdd_zero(info->manager);
else {
resE = ImageByInputSplit(info, vectorE, one, newFrom,
relationArrayE, cofactorCubeE, abstractCubeE,
splitMethod, turnDepth, depth + 1);
}
ImgVectorFree(vectorE);
if (newFrom)
mdd_free(newFrom);
if (!bdd_is_tautology(andE, 1)) {
tmp = resE;
resE = mdd_and(tmp, andE, 1, 1);
mdd_free(tmp);
}
if (findEssential)
foundEssentialDepthE = info->foundEssentialDepth;
if (relationArrayE && relationArrayE != newRelationArray)
mdd_array_free(relationArrayE);
if (cofactorCubeE && cofactorCubeE != newCofactorCube)
mdd_free(cofactorCubeE);
if (abstractCubeE && abstractCubeE != newAbstractCube)
mdd_free(abstractCubeE);
resPart = bdd_ite(comp->var, resT, resE, 1, 1, 1);
if (info->option->verbosity) {
size = bdd_size(resPart);
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), size);
}
}
mdd_free(one);
if (info->imgCache)
ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t), resPart);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, from);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
}
new_ = mdd_and(res, resPart, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(resPart), size);
}
}
mdd_free(res);
res = new_;
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, from);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
}
if (!info->imgCache) {
mdd_free(resPart);
ImgVectorFree(newVector);
}
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
if (turnFlag)
info->nTurns++;
if (findEssential) {
if (foundEssentialDepth == info->option->maxEssentialDepth) {
if (foundEssentialDepthT < foundEssentialDepthE)
foundEssentialDepth = foundEssentialDepthT;
else
foundEssentialDepth = foundEssentialDepthE;
}
info->foundEssentialDepth = foundEssentialDepth;
}
if (info->option->debug)
assert(TfmCheckImageValidity(info, res));
return(res);
}
}
/* compute disconnected component and best variable selection */
vectorArray = array_alloc(array_t *, 0);
varArray = array_alloc(int, 0);
if (info->option->delayedSplit && relationArray) {
nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, from, 0,
info->option->inputSplit,
info->option->piSplitFlag,
vectorArray, varArray, &product,
newRelationArray, &tmpRelationArray,
&cofactor, &abstract);
} else {
nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, from, 0,
info->option->inputSplit,
info->option->piSplitFlag,
vectorArray, varArray, &product,
newRelationArray, &tmpRelationArray,
NIL(mdd_t *), NIL(mdd_t *));
cofactor = NIL(mdd_t);
abstract = NIL(mdd_t);
if (info->option->debug && nGroups >= 1) {
if (info->option->verbosity > 1) {
ImgPrintVectorDependency(info, newVector, info->option->verbosity);
PrintVectorDecomposition(info, vectorArray, varArray);
}
refResult = ImgImageByHybrid(info, newVector, from);
resPart = mdd_dup(product);
for (i = 0; i < array_n(vectorArray); i++) {
vector = array_fetch(array_t *, vectorArray, i);
resTmp = ImgImageByHybrid(info, vector, from);
tmp = resPart;
resPart = mdd_and(tmp, resTmp, 1, 1);
mdd_free(tmp);
mdd_free(resTmp);
if (arraySize > nFuncs) {
split = array_fetch(int, varArray, i);
assert(!st_is_member(info->intermediateVarsTable,
(char *)(long)split));
}
}
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
mdd_free(resPart);
}
}
vectorSize = array_n(newVector);
if ((!info->imgCache || nGroups <= 1) && !info->option->debug)
ImgVectorFree(newVector);
if (newRelationArray) {
if (newRelationArray != relationArray &&
tmpRelationArray != newRelationArray) {
mdd_array_free(newRelationArray);
}
newRelationArray = tmpRelationArray;
}
if (nGroups == 0) {
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube)
mdd_free(newAbstractCube);
if (cofactor)
mdd_free(cofactor);
if (abstract)
mdd_free(abstract);
array_free(vectorArray);
array_free(varArray);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, from);
assert(mdd_equal(refResult, product));
mdd_free(refResult);
ImgVectorFree(newVector);
}
new_ = mdd_and(res, product, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(product), size);
}
}
mdd_free(res);
mdd_free(product);
res = new_;
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
if (findEssential)
info->foundEssentialDepth = foundEssentialDepth;
if (info->option->debug)
assert(TfmCheckImageValidity(info, res));
return(res);
}
if (info->option->delayedSplit && relationArray) {
tmp = newCofactorCube;
newCofactorCube = mdd_and(tmp, cofactor, 1, 1);
mdd_free(tmp);
mdd_free(cofactor);
tmp = newAbstractCube;
newAbstractCube = mdd_and(tmp, abstract, 1, 1);
mdd_free(tmp);
mdd_free(abstract);
}
if (nGroups > 1) {
if (info->nDecomps == 0 || depth < info->topDecomp)
info->topDecomp = depth;
if (info->nDecomps == 0 || vectorSize > info->maxDecomp)
info->maxDecomp = vectorSize;
info->averageDecomp = (info->averageDecomp * (float)info->nDecomps +
(float)nGroups) / (float)(info->nDecomps + 1);
info->nDecomps++;
}
if (relationArray && nGroups > 1) {
abstractVars = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(vectorArray); i++) {
vector = array_fetch(array_t *, vectorArray, i);
cube = mdd_one(info->manager);
for (j = 0; j < nGroups; j++) {
if (j == i)
continue;
tmpVector = array_fetch(array_t *, vectorArray, j);
for (k = 0; k < array_n(tmpVector); k++) {
comp = array_fetch(ImgComponent_t *, tmpVector, k);
tmp = cube;
cube = mdd_and(cube, comp->var, 1, 1);
mdd_free(tmp);
}
}
tmp = ImgSubstitute(cube, info->functionData, Img_D2R_c);
mdd_free(cube);
array_insert_last(mdd_t *, abstractVars, tmp);
}
} else
abstractVars = NIL(array_t);
for (i = 0; i < array_n(vectorArray); i++) {
vector = array_fetch(array_t *, vectorArray, i);
if (from)
newFrom = mdd_dup(from);
else
newFrom = from;
if (relationArray) {
if (nGroups == 1) {
partRelationArray = newRelationArray;
if (info->option->delayedSplit) {
partCofactorCube = newCofactorCube;
partAbstractCube = newAbstractCube;
} else {
partCofactorCube = NIL(mdd_t);
partAbstractCube = NIL(mdd_t);
}
} else {
cube = array_fetch(mdd_t *, abstractVars, i);
if (info->option->delayedSplit) {
partRelationArray = newRelationArray;
partCofactorCube = mdd_dup(newCofactorCube);
partAbstractCube = mdd_and(newAbstractCube, cube, 1, 1);
} else {
partRelationArray = ImgGetAbstractedRelationArray(info->manager,
newRelationArray,
cube);
mdd_free(cube);
partCofactorCube = NIL(mdd_t);
partAbstractCube = NIL(mdd_t);
}
}
if (info->option->debug) {
refResult = ImgImageByHybrid(info, vector, from);
resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
partRelationArray,
partCofactorCube,
partAbstractCube);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
mdd_free(resPart);
}
} else {
partRelationArray = newRelationArray;
partCofactorCube = NIL(mdd_t);
partAbstractCube = NIL(mdd_t);
}
hit = 1;
if (!info->imgCache || nGroups == 1 ||
!(resPart = ImgCacheLookupTable(info, info->imgCache, vector,
newFrom))) {
hit = 0;
if (arraySize > nFuncs)
size = ImgVectorFunctionSize(vector);
else
size = array_n(vector);
if (size == 1) {
comp = array_fetch(ImgComponent_t *, vector, 0);
if (array_n(vector) > 1)
func = ImgGetComposedFunction(vector);
else
func = comp->func;
if (info->useConstraint) {
constConstrain = ImgConstConstrain(func, newFrom);
if (constConstrain == 1)
resPart = mdd_dup(comp->var);
else if (constConstrain == 0)
resPart = mdd_not(comp->var);
else
resPart = mdd_one(info->manager);
} else {
if (bdd_is_tautology(func, 1))
resPart = mdd_dup(comp->var);
else if (bdd_is_tautology(func, 0))
resPart = mdd_not(comp->var);
else
resPart = mdd_one(info->manager);
}
if (array_n(vector) > 1)
mdd_free(func);
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
} else if (size == 2) {
if (info->useConstraint) {
ImgVectorConstrain(info, vector, newFrom, NIL(array_t),
&newVector, &resTmp, NIL(array_t *),
NIL(mdd_t *), NIL(mdd_t *), FALSE);
if (array_n(newVector) <= 1)
resPart = resTmp;
else {
mdd_free(resTmp);
resPart = ImageFast2(info, newVector);
}
ImgVectorFree(newVector);
} else
resPart = ImageFast2(info, vector);
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
} else {
nRecur = 0;
split = array_fetch(int, varArray, i);
if (partRelationArray && info->imgKeepPiInTr == FALSE) {
if (st_lookup(info->quantifyVarsTable, (char *)(long)split,
NIL(char *))) {
int newSplit;
/* checks the splitting is valid */
newSplit = CheckIfValidSplitOrGetNew(info, split, vector,
partRelationArray, from);
if (newSplit == -1) {
resPart = ImgImageByHybrid(info, vector, from);
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
info->nTurns++;
goto cache;
}
split = newSplit;
}
}
var = bdd_var_with_index(info->manager, split);
if (newFrom)
fromT = bdd_cofactor(newFrom, var);
else
fromT = NIL(mdd_t);
if (partRelationArray) {
if (info->option->delayedSplit) {
relationArrayT = partRelationArray;
cofactorCubeT = mdd_and(partCofactorCube, var, 1, 1);
} else {
relationArrayT = ImgGetCofactoredRelationArray(partRelationArray,
var);
cofactorCubeT = partCofactorCube;
}
} else {
relationArrayT = NIL(array_t);
cofactorCubeT = NIL(mdd_t);
}
if (!fromT || !bdd_is_tautology(fromT, 0)) {
prevLambda = info->prevLambda;
prevTotal = info->prevTotal;
prevVectorBddSize = info->prevVectorBddSize;
prevVectorSize = info->prevVectorSize;
resT = ImageByInputSplit(info, vector, var, fromT,
relationArrayT, cofactorCubeT, partAbstractCube,
splitMethod, turnDepth, depth + 1);
if (info->option->debug) {
refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t),
fromT, relationArrayT,
cofactorCubeT,
partAbstractCube);
assert(mdd_equal(refResult, resT));
mdd_free(refResult);
}
info->prevLambda = prevLambda;
info->prevTotal = prevTotal;
info->prevVectorBddSize = prevVectorBddSize;
info->prevVectorSize = prevVectorSize;
if (findEssential)
foundEssentialDepthT = info->foundEssentialDepth;
nRecur++;
} else
resT = mdd_zero(info->manager);
if (fromT)
mdd_free(fromT);
if (relationArrayT && relationArrayT != partRelationArray)
mdd_array_free(relationArrayT);
if (cofactorCubeT && cofactorCubeT != partCofactorCube)
mdd_free(cofactorCubeT);
if (bdd_is_tautology(resT, 1)) {
mdd_free(var);
resPart = resT;
info->nEmptySubImage++;
} else {
varNot = mdd_not(var);
mdd_free(var);
if (newFrom)
fromE = bdd_cofactor(newFrom, varNot);
else
fromE = NIL(mdd_t);
if (partRelationArray) {
if (info->option->delayedSplit) {
relationArrayE = partRelationArray;
cofactorCubeE = mdd_and(partCofactorCube, varNot, 1, 1);
} else {
relationArrayE = ImgGetCofactoredRelationArray(partRelationArray,
varNot);
cofactorCubeE = partCofactorCube;
}
} else {
relationArrayE = NIL(array_t);
cofactorCubeE = NIL(mdd_t);
}
if (!fromE || !bdd_is_tautology(fromE, 0)) {
resE = ImageByInputSplit(info, vector, varNot, fromE,
relationArrayE, cofactorCubeE, partAbstractCube,
splitMethod, turnDepth, depth + 1);
if (info->option->debug) {
refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t),
fromE, relationArrayE,
cofactorCubeE,
partAbstractCube);
assert(mdd_equal(refResult, resE));
mdd_free(refResult);
}
if (findEssential)
foundEssentialDepthE = info->foundEssentialDepth;
nRecur++;
} else
resE = mdd_zero(info->manager);
mdd_free(varNot);
if (fromE)
mdd_free(fromE);
if (relationArrayE && relationArrayE != partRelationArray)
mdd_array_free(relationArrayE);
if (cofactorCubeE && cofactorCubeE != partCofactorCube)
mdd_free(cofactorCubeE);
resPart = mdd_or(resT, resE, 1, 1);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, vector, from);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
}
if (info->option->verbosity) {
size = bdd_size(resPart);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_or(%d,%d) = %d\n",
bdd_size(resT), bdd_size(resE), size);
}
}
mdd_free(resT);
mdd_free(resE);
}
if (nRecur == 0) {
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
}
}
cache:
if (info->imgCache) {
ImgCacheInsertTable(info->imgCache, vector, newFrom, resPart);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, vector, newFrom);
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
}
}
}
if (!info->imgCache || hit) {
ImgVectorFree(vector);
if (newFrom)
mdd_free(newFrom);
}
new_ = mdd_and(product, resPart, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(product), bdd_size(resPart), size);
}
}
mdd_free(product);
if (!info->imgCache || hit)
mdd_free(resPart);
product = new_;
if (nGroups > 1 && partRelationArray != newRelationArray)
mdd_array_free(partRelationArray);
if (partCofactorCube && partCofactorCube != newCofactorCube)
mdd_free(partCofactorCube);
if (partAbstractCube && partAbstractCube != newAbstractCube)
mdd_free(partAbstractCube);
}
if (abstractVars)
array_free(abstractVars);
if (relationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (newCofactorCube)
mdd_free(newCofactorCube);
if (newAbstractCube)
mdd_free(newAbstractCube);
array_free(vectorArray);
array_free(varArray);
if (info->imgCache && nGroups > 1) {
if (from) {
ImgCacheInsertTable(info->imgCache, newVector, mdd_dup(from),
mdd_dup(product));
} else {
ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t),
mdd_dup(product));
}
}
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, from);
assert(mdd_equal(refResult, product));
mdd_free(refResult);
if (!info->imgCache || nGroups == 1)
ImgVectorFree(newVector);
}
new_ = mdd_and(res, product, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(product), size);
}
}
mdd_free(res);
mdd_free(product);
res = new_;
if (findEssential) {
if (foundEssentialDepth == info->option->maxEssentialDepth) {
if (foundEssentialDepthT < foundEssentialDepthE)
foundEssentialDepth = foundEssentialDepthT;
else
foundEssentialDepth = foundEssentialDepthE;
}
info->foundEssentialDepth = foundEssentialDepth;
}
if (info->option->debug)
assert(TfmCheckImageValidity(info, res));
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * ImageByOutputSplit | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | constraint, | ||
| int | depth | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes an image by output splitting.]
Description [Computes an image by output splitting.]
SideEffects []
Definition at line 1987 of file imgTfmFwd.c.
{
array_t *newVector;
mdd_t *new_, *resT, *resE, *res, *resPart;
mdd_t *constrain, *tmp, *func;
int size, i, vectorSize;
array_t *vectorArray, *varArray;
ImgComponent_t *comp;
int hit;
int split, nGroups;
mdd_t *product, *refResult;
ImgVectorConstrain(info, vector, constraint, NIL(array_t),
&newVector, &res, NIL(array_t *),
NIL(mdd_t *), NIL(mdd_t *), FALSE);
info->nRecursion++;
if (info->nIntermediateVars)
size = ImgVectorFunctionSize(newVector);
else
size = array_n(newVector);
if (size <= 1) {
ImgVectorFree(newVector);
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
return(res);
}
if (size == 2) {
hit = 1;
if (!info->imgCache ||
!(resPart = ImgCacheLookupTable(info, info->imgCache, newVector,
NIL(bdd_t)))) {
hit = 0;
resPart = ImageFast2(info, newVector);
if (info->imgCache)
ImgCacheInsertTable(info->imgCache, newVector, NIL(bdd_t), resPart);
}
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
}
new_ = mdd_and(res, resPart, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(resPart), size);
}
}
mdd_free(res);
if (!info->imgCache || hit) {
mdd_free(resPart);
ImgVectorFree(newVector);
}
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
return(new_);
}
if (info->imgCache) {
resPart = ImgCacheLookupTable(info, info->imgCache, newVector, NIL(mdd_t));
if (resPart) {
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
assert(mdd_equal(refResult, resPart));
mdd_free(refResult);
}
new_ = mdd_and(res, resPart, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(resPart), size);
}
}
mdd_free(res);
mdd_free(resPart);
res = new_;
ImgVectorFree(newVector);
return(res);
}
}
/* compute disconnected component and best variable selection */
vectorArray = array_alloc(array_t *, 0);
varArray = array_alloc(array_t *, 0);
nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, NIL(mdd_t), 1,
info->option->outputSplit, 0,
vectorArray, varArray, &product,
NIL(array_t), NIL(array_t *),
NIL(mdd_t *), NIL(mdd_t *));
vectorSize = array_n(newVector);
if ((!info->imgCache || nGroups <= 1) && !info->option->debug)
ImgVectorFree(newVector);
if (nGroups == 0) {
array_free(vectorArray);
array_free(varArray);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
assert(mdd_equal(refResult, product));
mdd_free(refResult);
ImgVectorFree(newVector);
}
new_ = mdd_and(res, product, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(product), size);
}
}
mdd_free(res);
mdd_free(product);
res = new_;
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
return(res);
} else if (nGroups > 1) {
if (info->nDecomps == 0 || depth < info->topDecomp)
info->topDecomp = depth;
if (info->nDecomps == 0 || vectorSize > info->maxDecomp)
info->maxDecomp = vectorSize;
info->averageDecomp = (info->averageDecomp * (float)info->nDecomps +
(float)nGroups) / (float)(info->nDecomps + 1);
info->nDecomps++;
}
product = mdd_one(info->manager);
for (i = 0; i < array_n(vectorArray); i++) {
vector = array_fetch(array_t *, vectorArray, i);
hit = 1;
if (!info->imgCache || nGroups == 1 ||
!(resPart = ImgCacheLookupTable(info, info->imgCache, vector,
NIL(bdd_t)))) {
hit = 0;
if (info->nIntermediateVars)
size = ImgVectorFunctionSize(vector);
else
size = array_n(vector);
if (size == 1) {
comp = array_fetch(ImgComponent_t *, vector, 0);
if (array_n(vector) > 1)
func = ImgGetComposedFunction(vector);
else
func = comp->func;
if (bdd_is_tautology(func, 1))
resPart = mdd_dup(comp->var);
else if (bdd_is_tautology(func, 0))
resPart = mdd_not(comp->var);
else
resPart = mdd_one(info->manager);
if (array_n(vector) > 1)
mdd_free(func);
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
} else if (size == 2) {
resPart = ImageFast2(info, vector);
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
} else {
split = array_fetch(int, varArray, i);
comp = array_fetch(ImgComponent_t *, vector, split);
constrain = comp->func;
resT = ImageByOutputSplit(info, vector, constrain, depth + 1);
tmp = mdd_not(constrain);
resE = ImageByOutputSplit(info, vector, tmp, depth + 1);
mdd_free(tmp);
resPart = bdd_ite(comp->var, resT, resE, 1, 1, 1);
if (info->option->verbosity) {
size = bdd_size(resPart);
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), size);
}
}
mdd_free(resT);
mdd_free(resE);
}
if (info->imgCache)
ImgCacheInsertTable(info->imgCache, vector, NIL(bdd_t), resPart);
}
if (!info->imgCache || hit)
ImgVectorFree(vector);
new_ = mdd_and(product, resPart, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(product), bdd_size(resPart), size);
}
}
mdd_free(product);
if (!info->imgCache || hit)
mdd_free(resPart);
product = new_;
}
array_free(vectorArray);
array_free(varArray);
if (info->imgCache && nGroups > 1) {
ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t),
mdd_dup(product));
}
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
assert(mdd_equal(refResult, product));
mdd_free(refResult);
if (!info->imgCache || nGroups == 1)
ImgVectorFree(newVector);
}
new_ = mdd_and(res, product, 1, 1);
if (info->option->verbosity) {
size = bdd_size(new_);
if (size > info->maxIntermediateSize)
info->maxIntermediateSize = size;
if (info->option->printBddSize) {
fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
bdd_size(res), bdd_size(product), size);
}
}
mdd_free(res);
mdd_free(product);
res = new_;
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * ImageByStaticInputSplit | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from, | ||
| array_t * | relationArray, | ||
| int | turnDepth, | ||
| int | depth | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes an image by static input splitting.]
Description [Computes an image by static input splitting.]
SideEffects []
Definition at line 1714 of file imgTfmFwd.c.
{
array_t *vectorT, *vectorE, *tmpVector;
mdd_t *resT, *resE, *res, *tmp, *cubeT, *cubeE;
mdd_t *fromT, *fromE;
mdd_t *var, *varNot;
array_t *relationArrayT, *relationArrayE;
array_t *newRelationArray, *tmpRelationArray;
int nRecur;
mdd_t *refResult, *and_;
mdd_t *essentialCube;
int findEssential;
int foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE;
int turnFlag, size;
info->nRecursion++;
turnFlag = 0;
if (turnDepth == -1) {
if (depth < info->option->splitMinDepth) {
info->nSplits++;
turnFlag = 0;
} else if (depth > info->option->splitMaxDepth) {
info->nConjoins++;
turnFlag = 1;
} else {
turnFlag = ImgDecideSplitOrConjoin(info, vector, from, 0,
relationArray, NIL(mdd_t),
NIL(mdd_t), 1, depth);
}
} else {
if (depth == turnDepth)
turnFlag = 1;
else
turnFlag = 0;
}
if (turnFlag) {
res = ImgImageByHybridWithStaticSplit(info, vector, from, relationArray,
NIL(mdd_t), NIL(mdd_t));
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
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++;
ImgVectorMinimize(info, vector, essentialCube, NIL(mdd_t), relationArray,
&tmpVector, &and_,
&tmpRelationArray, NIL(mdd_t *), NIL(mdd_t *));
foundEssentialDepth = depth;
} else {
tmpVector = vector;
tmpRelationArray = relationArray;
and_ = NIL(mdd_t);
foundEssentialDepth = info->option->maxEssentialDepth;
}
mdd_free(essentialCube);
foundEssentialDepthT = info->option->maxEssentialDepth;
foundEssentialDepthE = info->option->maxEssentialDepth;
} else {
tmpVector = vector;
tmpRelationArray = relationArray;
and_ = NIL(mdd_t);
/* To remove compiler warnings */
foundEssentialDepth = -1;
foundEssentialDepthT = -1;
foundEssentialDepthE = -1;
}
var = ImgChooseTrSplitVar(info, tmpVector, tmpRelationArray,
info->option->trSplitMethod,
info->option->piSplitFlag);
if (!var) {
res = ImgImageByHybridWithStaticSplit(info, vector, from, relationArray,
NIL(mdd_t), NIL(mdd_t));
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
info->foundEssentialDepth = info->option->maxEssentialDepth;
return(res);
}
nRecur = 0;
if (tmpVector) {
ImgVectorConstrain(info, tmpVector, var, tmpRelationArray,
&vectorT, &cubeT, &newRelationArray,
NIL(mdd_t *), NIL(mdd_t *), TRUE);
} else {
vectorT = NIL(array_t);
cubeT = NIL(mdd_t);
newRelationArray = tmpRelationArray;
}
fromT = bdd_cofactor(from, var);
relationArrayT = ImgGetCofactoredRelationArray(newRelationArray, var);
if (relationArray && newRelationArray != tmpRelationArray)
mdd_array_free(newRelationArray);
if (!bdd_is_tautology(fromT, 0)) {
resT = ImageByStaticInputSplit(info, vectorT, fromT,
relationArrayT, turnDepth, depth + 1);
if (findEssential)
foundEssentialDepthT = info->foundEssentialDepth;
if (vectorT) {
ImgVectorFree(vectorT);
if (!bdd_is_tautology(cubeT, 1)) {
tmp = resT;
resT = mdd_and(tmp, cubeT, 1, 1);
mdd_free(tmp);
}
mdd_free(cubeT);
}
nRecur++;
} else {
resT = mdd_zero(info->manager);
if (vectorT) {
ImgVectorFree(vectorT);
mdd_free(cubeT);
}
}
mdd_free(fromT);
mdd_array_free(relationArrayT);
if (bdd_is_tautology(resT, 1)) {
mdd_free(var);
if (vector && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
res = resT;
info->nEmptySubImage++;
} else {
varNot = mdd_not(var);
mdd_free(var);
if (tmpVector) {
ImgVectorConstrain(info, tmpVector, varNot, tmpRelationArray,
&vectorE, &cubeE, &newRelationArray,
NIL(mdd_t *), NIL(mdd_t *), TRUE);
} else {
vectorE = NIL(array_t);
cubeE = NIL(mdd_t);
newRelationArray = tmpRelationArray;
}
fromE = bdd_cofactor(from, varNot);
relationArrayE = ImgGetCofactoredRelationArray(newRelationArray, varNot);
if (vector && newRelationArray != tmpRelationArray)
mdd_array_free(newRelationArray);
if (!bdd_is_tautology(fromE, 0)) {
resE = ImageByStaticInputSplit(info, vectorE, fromE,
relationArrayE, turnDepth, depth + 1);
if (findEssential)
foundEssentialDepthE = info->foundEssentialDepth;
if (vectorE) {
ImgVectorFree(vectorE);
if (!bdd_is_tautology(cubeE, 1)) {
tmp = resE;
resE = mdd_and(tmp, cubeE, 1, 1);
mdd_free(tmp);
}
mdd_free(cubeE);
}
nRecur++;
} else {
resE = mdd_zero(info->manager);
if (vectorE) {
ImgVectorFree(vectorE);
mdd_free(cubeE);
}
}
mdd_free(fromE);
mdd_array_free(relationArrayE);
res = mdd_or(resT, resE, 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_or(%d,%d) = %d\n",
bdd_size(resT), bdd_size(resE), size);
}
}
mdd_free(resT);
mdd_free(resE);
mdd_free(varNot);
}
if (tmpVector && tmpVector != vector)
ImgVectorFree(tmpVector);
if (tmpRelationArray && tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
if (and_) {
tmp = res;
res = mdd_and(tmp, and_, 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_and(%d,%d) = %d\n",
bdd_size(tmp), bdd_size(and_), size);
}
}
mdd_free(tmp);
}
if (info->option->debug) {
refResult = ImgImageByHybridWithStaticSplit(info, vector, from,
relationArray,
NIL(mdd_t), NIL(mdd_t));
assert(mdd_equal(refResult, res));
mdd_free(refResult);
}
if (nRecur == 0) {
info->averageDepth = (info->averageDepth * (float)info->nLeaves +
(float)depth) / (float)(info->nLeaves + 1);
if (depth > info->maxDepth)
info->maxDepth = depth;
info->nLeaves++;
}
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 int ImageDecomposeAndChooseSplitVar | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | from, | ||
| int | splitMethod, | ||
| int | split, | ||
| int | piSplitFlag, | ||
| array_t * | vectorArray, | ||
| array_t * | varArray, | ||
| mdd_t ** | singles, | ||
| array_t * | relationArray, | ||
| array_t ** | newRelationArray, | ||
| mdd_t ** | cofactorCube, | ||
| mdd_t ** | abstractCube | ||
| ) | [static] |
Function********************************************************************
Synopsis [Try to decompose function vector and find a splitting variable for each decomposed block.]
Description [Try to decompose function vector and find a splitting variable for each decomposed block.]
SideEffects []
Definition at line 2264 of file imgTfmFwd.c.
{
int i, j, f, index;
int nGroups, nSingles, nChosen;
int nVars, nFuncs, arraySize;
char *varFlag;
int *funcGroup;
int *varOccur;
int bestVar;
int *stack, size;
ImgComponent_t *comp, *newComp;
array_t *partVector;
char *stackFlag;
char *support;
mdd_t *func;
int *varCost;
int decompose;
int res, constConstrain;
mdd_t *tmp, *cofactor, *abstract, *nsVar;
array_t *tmpRelationArray;
char *intermediateVarFlag;
int *intermediateVarFuncMap;
if (info->useConstraint && from && splitMethod == 0)
decompose = 0;
else
decompose = 1;
arraySize = array_n(vector);
if (info->nIntermediateVars)
nFuncs = ImgVectorFunctionSize(vector);
else
nFuncs = arraySize;
nVars = info->nVars;
*singles = mdd_one(info->manager);
if (relationArray) {
cofactor = mdd_one(info->manager);
abstract = mdd_one(info->manager);
} else {
cofactor = NIL(mdd_t);
abstract = NIL(mdd_t);
}
if (decompose) {
funcGroup = ALLOC(int, arraySize);
memset(funcGroup, 0, sizeof(int) * arraySize);
varFlag = ALLOC(char, nVars);
memset(varFlag, 0, sizeof(char) * nVars);
stack = ALLOC(int, arraySize);
stackFlag = ALLOC(char, arraySize);
memset(stackFlag, 0, sizeof(char) * arraySize);
if (arraySize > nFuncs) {
intermediateVarFlag = ALLOC(char, nVars);
memset(intermediateVarFlag, 0, sizeof(char) * nVars);
intermediateVarFuncMap = ALLOC(int, nVars);
memset(intermediateVarFuncMap, 0, sizeof(int) * nVars);
for (i = 0; i < arraySize; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
index = (int)bdd_top_var_id(comp->var);
intermediateVarFlag[index] = 1;
intermediateVarFuncMap[index] = i;
}
}
} else {
/* To remove compiler warnings */
intermediateVarFlag = NIL(char);
intermediateVarFuncMap = NIL(int);
}
} else {
/* To remove compiler warnings */
funcGroup = NIL(int);
varFlag = NIL(char);
stack = NIL(int);
stackFlag = NIL(char);
intermediateVarFlag = NIL(char);
intermediateVarFuncMap = NIL(int);
}
varOccur = ALLOC(int, nVars);
if (splitMethod == 0 && split > 0)
varCost = ALLOC(int, nVars);
else
varCost = NIL(int);
nGroups = 0;
nSingles = 0;
nChosen = 0;
while (nChosen < nFuncs) {
bestVar = -1;
memset(varOccur, 0, sizeof(int) * nVars);
if (varCost)
memset(varCost, 0, sizeof(int) * nVars);
if (decompose) {
size = 0;
for (i = 0; i < arraySize; i++) {
if (funcGroup[i] == 0) {
stack[0] = i;
size = 1;
stackFlag[i] = 1;
break;
}
}
assert(size == 1);
while (size) {
size--;
f = stack[size];
funcGroup[f] = nGroups + 1;
comp = array_fetch(ImgComponent_t *, vector, f);
nChosen++;
if (nChosen == arraySize)
break;
support = comp->support;
if (comp->intermediate) {
index = (int)bdd_top_var_id(comp->var);
support[index] = 1;
}
for (i = 0; i < nVars; i++) {
if (!support[i])
continue;
varOccur[i]++;
if (varFlag[i])
continue;
varFlag[i] = 1;
for (j = 0; j < arraySize; j++) {
if (j == f || stackFlag[j])
continue;
comp = array_fetch(ImgComponent_t *, vector, j);
if (arraySize != nFuncs) {
if (intermediateVarFlag[i] && comp->intermediate) {
index = (int)bdd_top_var_id(comp->var);
if (index == i) {
if (funcGroup[j] == 0) {
stack[size] = j;
size++;
stackFlag[j] = 1;
}
FindIntermediateSupport(vector, comp, nVars, nGroups,
stack, stackFlag, funcGroup, &size,
intermediateVarFlag,
intermediateVarFuncMap);
continue;
}
}
}
if (funcGroup[j])
continue;
if (comp->support[i]) {
stack[size] = j;
size++;
stackFlag[j] = 1;
}
}
}
if (comp->intermediate) {
index = (int)bdd_top_var_id(comp->var);
support[index] = 0;
}
}
} else {
for (i = 0; i < arraySize; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
support = comp->support;
for (j = 0; j < nVars; j++) {
if (support[j])
varOccur[j]++;
}
}
nChosen = nFuncs;
}
nGroups++;
/* Collect the functions which belong to the current group */
partVector = array_alloc(ImgComponent_t *, 0);
for (i = 0; i < arraySize; i++) {
if (decompose == 0 || funcGroup[i] == nGroups) {
comp = array_fetch(ImgComponent_t *, vector, i);
newComp = ImgComponentCopy(info, comp);
array_insert_last(ImgComponent_t *, partVector, newComp);
}
}
if (arraySize == nFuncs)
size = array_n(partVector);
else
size = ImgVectorFunctionSize(partVector);
if (size == 1) {
nSingles++;
if (size == array_n(partVector)) {
comp = array_fetch(ImgComponent_t *, partVector, 0);
func = comp->func;
} else {
comp = ImgGetLatchComponent(partVector);
func = ImgGetComposedFunction(partVector);
}
if (from) {
constConstrain = ImgConstConstrain(func, from);
if (constConstrain == 1)
res = 1;
else if (constConstrain == 0)
res = 0;
else
res = 2;
} else {
if (bdd_is_tautology(func, 1))
res = 1;
else if (bdd_is_tautology(func, 0))
res = 0;
else
res = 2;
}
if (size != array_n(partVector))
mdd_free(func);
if (res == 1) {
tmp = *singles;
*singles = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
} else if (res == 0) {
tmp = *singles;
*singles = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
}
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);
}
ImgVectorFree(partVector);
continue;
}
array_insert_last(array_t *, vectorArray, partVector);
if (splitMethod == 0) { /* input splitting */
if (decompose) {
if (info->option->findDecompVar) {
bestVar = FindDecomposableVariable(info, partVector);
if (bestVar != -1)
split = -1;
}
} else if (from) {
comp = ImgComponentAlloc(info);
comp->func = from;
ImgComponentGetSupport(comp);
for (i = 0; i < nVars; i++) {
if (comp->support[i])
varOccur[i]++;
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
}
if (split != -1) {
bestVar = ChooseInputSplittingVariable(info, partVector, from,
info->option->inputSplit, decompose,
info->option->piSplitFlag, varOccur);
}
} else { /* output splitting */
bestVar = ChooseOutputSplittingVariable(info, partVector,
info->option->outputSplit);
}
assert(bestVar != -1);
array_insert_last(int, varArray, bestVar);
}
if (newRelationArray)
*newRelationArray = relationArray;
if (cofactorCube && abstractCube) {
if (cofactor)
*cofactorCube = cofactor;
if (abstract)
*abstractCube = abstract;
} else {
if (cofactor) {
if (bdd_is_tautology(cofactor, 1))
mdd_free(cofactor);
else {
*newRelationArray = ImgGetCofactoredRelationArray(relationArray,
cofactor);
mdd_free(cofactor);
}
}
if (abstract) {
if (bdd_is_tautology(abstract, 1))
mdd_free(abstract);
else {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetAbstractedRelationArray(info->manager,
tmpRelationArray,
abstract);
mdd_free(abstract);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
}
}
}
if (decompose) {
FREE(stackFlag);
FREE(stack);
FREE(funcGroup);
FREE(varFlag);
if (arraySize > nFuncs) {
FREE(intermediateVarFlag);
FREE(intermediateVarFuncMap);
}
}
FREE(varOccur);
if (varCost)
FREE(varCost);
nGroups -= nSingles;
return(nGroups);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * ImageFast2 | ( | ImgTfmInfo_t * | info, |
| array_t * | vector | ||
| ) | [static] |
Function********************************************************************
Synopsis [Fast image computation when function vector contains only two functions.]
Description [Fast image computation when function vector contains only two functions.]
SideEffects []
Definition at line 2603 of file imgTfmFwd.c.
{
mdd_t *f1, *f2;
int f21n, f21p;
mdd_t *res, *resp, *resn;
mdd_t *i1, *i2;
ImgComponent_t *comp;
mdd_t *refResult;
int i, freeFlag, size;
array_t *varArray, *funcArray;
assert(ImgVectorFunctionSize(vector) == 2);
if (info->option->debug)
refResult = ImgImageByHybrid(info, vector, NIL(mdd_t));
else
refResult = NIL(mdd_t);
if (array_n(vector) == 2) {
comp = array_fetch(ImgComponent_t *, vector, 0);
f1 = comp->func;
i1 = comp->var;
comp = array_fetch(ImgComponent_t *, vector, 1);
f2 = comp->func;
i2 = comp->var;
freeFlag = 0;
} else {
varArray = array_alloc(mdd_t *, 0);
funcArray = array_alloc(mdd_t *, 0);
i1 = NIL(mdd_t);
i2 = NIL(mdd_t);
f1 = NIL(mdd_t);
f2 = NIL(mdd_t);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
array_insert_last(mdd_t *, varArray, comp->var);
array_insert_last(mdd_t *, funcArray, comp->func);
continue;
}
if (f1) {
f2 = comp->func;
i2 = comp->var;
} else {
f1 = comp->func;
i1 = comp->var;
}
}
f1 = bdd_vector_compose(f1, varArray, funcArray);
f2 = bdd_vector_compose(f2, varArray, funcArray);
array_free(varArray);
array_free(funcArray);
freeFlag = 1;
}
ImgCheckConstConstrain(f1, f2, &f21p, &f21n);
if (f21p == 1)
resp = mdd_dup(i2);
else if (f21p == 0)
resp = mdd_not(i2);
else
resp = mdd_one(info->manager);
if (f21n == 1)
resn = mdd_dup(i2);
else if (f21n == 0)
resn = mdd_not(i2);
else
resn = mdd_one(info->manager);
/* merge final result */
res = bdd_ite(i1, resp, resn, 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(resp), bdd_size(resn), size);
}
}
mdd_free(resp);
mdd_free(resn);
if (freeFlag) {
mdd_free(f1);
mdd_free(f2);
}
if (info->option->debug) {
assert(mdd_equal(refResult, res));
mdd_free(refResult);
}
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* ImgChooseTrSplitVar | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| array_t * | relationArray, | ||
| int | trSplitMethod, | ||
| int | piSplitFlag | ||
| ) |
Function********************************************************************
Synopsis [Chooses splitting variables for static splitting.]
Description [Chooses splitting variables for static splitting.]
SideEffects []
Definition at line 536 of file imgTfmFwd.c.
{
int i, j, nVars;
ImgComponent_t *comp;
char *support;
int *varCost, bestCost = 0;
int id, split;
mdd_t *var, *relation;
nVars = info->nVars;
varCost = ALLOC(int, nVars);
memset(varCost, 0, sizeof(int) * nVars);
if (trSplitMethod == 0) {
if (vector) {
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
support = comp->support;
for (j = 0; j < nVars; j++) {
if (support[j])
varCost[j]++;
}
}
}
comp = ImgComponentAlloc(info);
support = comp->support;
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
comp->func = relation;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
for (j = 0; j < nVars; j++) {
if (support[j])
varCost[j]++;
}
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
} else {
for (i = 0; i < array_n(info->domainVarBddArray); i++) {
var = array_fetch(mdd_t *, info->domainVarBddArray, i);
id = (int)bdd_top_var_id(var);
if (vector) {
for (j = 0; j < array_n(vector); j++) {
comp = array_fetch(ImgComponent_t *, vector, j);
varCost[id] += bdd_estimate_cofactor(comp->func, var, 1);
varCost[id] += bdd_estimate_cofactor(comp->func, var, 0);
}
}
for (j = 0; j < array_n(relationArray); j++) {
relation = array_fetch(mdd_t *, relationArray, j);
varCost[id] += bdd_estimate_cofactor(relation, var, 1);
varCost[id] += bdd_estimate_cofactor(relation, var, 0);
}
varCost[id] = IMG_TF_MAX_INT - varCost[id];
}
}
split = -1;
for (i = 0; i < nVars; i++) {
if (varCost[i] == 0)
continue;
if (!piSplitFlag) {
if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
continue;
}
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
continue;
if (info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) {
continue;
}
if (split == -1 || varCost[i] > bestCost) {
bestCost = varCost[i];
split = i;
}
}
FREE(varCost);
if (split == -1)
return(NIL(mdd_t));
var = bdd_var_with_index(info->manager, split);
return(var);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* ImgTfmImage | ( | ImgTfmInfo_t * | info, |
| mdd_t * | from | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Computes an image with transition function method.]
Description [Computes an image with transition function method.]
SideEffects []
Definition at line 101 of file imgTfmFwd.c.
{
mdd_t *res, *r, *cube, *newFrom, *one;
array_t *newVector, *depVector;
int splitMethod, turnDepth;
mdd_t *refResult;
array_t *relationArray, *newRelationArray, *tmpRelationArray;
int eliminateDepend;
int partial, saveUseConstraint;
long size1, size2;
mdd_t *cofactorCube, *abstractCube;
int i, maxDepth, size, nDependVars;
info->maxIntermediateSize = 0;
if (info->eliminateDepend == 1 ||
(info->eliminateDepend == 2 && info->nPrevEliminatedFwd > 0)) {
eliminateDepend = 1;
} else
eliminateDepend = 0;
saveUseConstraint = info->useConstraint;
if (info->buildTR) {
if (eliminateDepend == 0 &&
info->option->splitMethod == 3 &&
info->option->splitMaxDepth < 0 &&
info->option->buildPartialTR == FALSE &&
info->option->rangeComp == 0 &&
info->option->findEssential == FALSE) {
r = ImgBddLinearAndSmooth(info->manager, from,
info->fwdClusteredRelationArray,
info->fwdArraySmoothVarBddArray,
info->fwdSmoothVarCubeArray,
info->option->verbosity);
res = ImgSubstitute(r, info->functionData, Img_R2D_c);
mdd_free(r);
return(res);
}
relationArray = mdd_array_duplicate(info->fwdClusteredRelationArray);
} else
relationArray = NIL(array_t);
if (info->useConstraint == 1 ||
(info->useConstraint == 2 &&
info->nImageComps == info->option->rangeTryThreshold)) {
if (info->buildTR == 2) {
newVector = NIL(array_t);
cube = mdd_one(info->manager);
if (eliminateDepend) {
newFrom = ImgTrmEliminateDependVars(info->functionData, relationArray,
from, NIL(mdd_t *), &nDependVars);
if (nDependVars) {
if (info->option->verbosity > 0)
(void)fprintf(vis_stdout, "Eliminated %d vars.\n", nDependVars);
info->averageFoundDependVars = (info->averageFoundDependVars *
(float)info->nFoundDependVars + (float)nDependVars) /
(float)(info->nFoundDependVars + 1);
info->nFoundDependVars++;
}
info->nPrevEliminatedFwd = nDependVars;
} else
newFrom = from;
cofactorCube = NIL(mdd_t);
abstractCube = NIL(mdd_t);
} else {
newVector = ImgVectorCopy(info, info->vector);
cube = mdd_one(info->manager);
if (eliminateDepend) {
newFrom = ImgTfmEliminateDependVars(info, newVector, relationArray,
from, NIL(array_t *), NIL(mdd_t *));
} else
newFrom = from;
if (info->option->delayedSplit && relationArray && info->buildTR != 2) {
cofactorCube = mdd_one(info->manager);
abstractCube = mdd_one(info->manager);
} else {
cofactorCube = NIL(mdd_t);
abstractCube = NIL(mdd_t);
}
}
} else {
if (eliminateDepend) {
depVector = ImgVectorCopy(info, info->vector);
newFrom = ImgTfmEliminateDependVars(info, depVector, relationArray, from,
NIL(array_t *), NIL(mdd_t *));
/* constrain delta w.r.t. from here */
if (info->option->delayedSplit && relationArray && info->buildTR != 2) {
ImgVectorConstrain(info, depVector, newFrom, relationArray,
&newVector, &cube, &newRelationArray, &cofactorCube,
&abstractCube, FALSE);
} else if (relationArray) {
ImgVectorConstrain(info, depVector, newFrom, relationArray,
&newVector, &cube, NIL(array_t *), &cofactorCube,
&abstractCube, FALSE);
newRelationArray = NIL(array_t);
} else {
ImgVectorConstrain(info, depVector, newFrom, NIL(array_t),
&newVector, &cube, NIL(array_t *), NIL(mdd_t *),
NIL(mdd_t *), FALSE);
newRelationArray = NIL(array_t);
cofactorCube = NIL(mdd_t);
abstractCube = NIL(mdd_t);
}
if (info->useConstraint == 2) {
size1 = ImgVectorBddSize(depVector);
size2 = ImgVectorBddSize(newVector);
if (info->option->rangeCheckReorder) {
bdd_reorder(info->manager);
size1 = ImgVectorBddSize(depVector);
size2 = ImgVectorBddSize(newVector);
}
if (size2 > size1 * info->option->rangeThreshold) { /* cancel */
if (info->option->verbosity)
fprintf(vis_stdout, "** tfm info: canceled range computation.\n");
info->useConstraint = 1;
ImgVectorFree(newVector);
newVector = depVector;
mdd_free(cube);
cube = mdd_one(info->manager);
if (newRelationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (cofactorCube) {
mdd_free(cofactorCube);
cofactorCube = mdd_one(info->manager);
}
if (abstractCube) {
mdd_free(abstractCube);
abstractCube = mdd_one(info->manager);
}
info->nImageComps++;
} else {
info->useConstraint = 0;
info->nImageComps = 0;
info->nRangeComps++;
}
}
if (info->useConstraint == 0)
ImgVectorFree(depVector);
} else {
newFrom = from;
/* constrain delta w.r.t. from here */
if (info->option->delayedSplit && relationArray && info->buildTR != 2) {
ImgVectorConstrain(info, info->vector, newFrom, relationArray,
&newVector, &cube, &newRelationArray, &cofactorCube,
&abstractCube, FALSE);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), NIL(mdd_t),
newRelationArray,
cofactorCube, abstractCube);
assert(mdd_equal(refResult, res));
mdd_free(refResult);
mdd_free(res);
}
} else if (relationArray) {
ImgVectorConstrain(info, info->vector, newFrom, relationArray,
&newVector, &cube, NIL(array_t *), &cofactorCube,
&abstractCube, FALSE);
newRelationArray = NIL(array_t);
} else {
ImgVectorConstrain(info, info->vector, newFrom, NIL(array_t),
&newVector, &cube, NIL(array_t *), NIL(mdd_t *),
NIL(mdd_t *), FALSE);
newRelationArray = NIL(array_t);
cofactorCube = NIL(mdd_t);
abstractCube = NIL(mdd_t);
}
if (info->useConstraint == 2) {
size1 = ImgVectorBddSize(info->vector);
size2 = ImgVectorBddSize(newVector);
if (info->option->rangeCheckReorder) {
bdd_reorder(info->manager);
size1 = ImgVectorBddSize(info->vector);
size2 = ImgVectorBddSize(newVector);
}
if (size2 > size1 * info->option->rangeThreshold) { /* cancel */
if (info->option->verbosity)
fprintf(vis_stdout, "** tfm info: canceled range computation.\n");
info->useConstraint = 1;
ImgVectorFree(newVector);
newVector = info->vector;
mdd_free(cube);
cube = mdd_one(info->manager);
if (newRelationArray && newRelationArray != relationArray)
mdd_array_free(newRelationArray);
if (cofactorCube) {
mdd_free(cofactorCube);
cofactorCube = mdd_one(info->manager);
}
if (abstractCube) {
mdd_free(abstractCube);
abstractCube = mdd_one(info->manager);
}
info->nImageComps++;
} else {
info->useConstraint = 0;
info->nImageComps = 0;
info->nRangeComps++;
}
}
}
if (info->useConstraint == 0 && relationArray) {
if (!newRelationArray) {
if (bdd_is_tautology(cofactorCube, 1) &&
bdd_is_tautology(abstractCube, 1)) {
newRelationArray = ImgGetConstrainedRelationArray(info, relationArray,
newFrom);
} else {
tmpRelationArray = ImgGetConstrainedRelationArray(info, relationArray,
newFrom);
newRelationArray = ImgGetCofactoredAbstractedRelationArray(
info->manager, tmpRelationArray,
cofactorCube, abstractCube);
if (info->option->debug) {
array_t *tmpVector;
tmpVector = ImgGetConstrainedVector(info, info->vector, newFrom);
if (info->option->checkEquivalence) {
assert(ImgCheckEquivalence(info, tmpVector, tmpRelationArray,
NIL(mdd_t), NIL(mdd_t), 0));
}
refResult = ImgImageByHybrid(info, tmpVector, NIL(mdd_t));
ImgVectorFree(tmpVector);
res = ImgImageByHybridWithStaticSplit(info, NIL(array_t),
NIL(mdd_t),
tmpRelationArray,
NIL(mdd_t), NIL(mdd_t));
assert(mdd_equal(refResult, res));
mdd_free(refResult);
mdd_free(res);
}
mdd_array_free(tmpRelationArray);
}
mdd_free(cofactorCube);
cofactorCube = NIL(mdd_t);
mdd_free(abstractCube);
abstractCube = NIL(mdd_t);
if (info->option->debug) {
refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), NIL(mdd_t),
newRelationArray,
NIL(mdd_t), NIL(mdd_t));
assert(mdd_equal(refResult, res));
mdd_free(refResult);
mdd_free(res);
if (info->nIntermediateVars) {
mdd_t *tmp;
refResult = ImgImageByHybrid(info, info->vector, newFrom);
res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), newFrom,
relationArray,
NIL(mdd_t), NIL(mdd_t));
assert(mdd_equal(refResult, res));
mdd_free(res);
tmp = ImgImageByHybrid(info, newVector, NIL(mdd_t));
res = mdd_and(tmp, cube, 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_and(%d,%d) = %d\n",
bdd_size(tmp), bdd_size(cube), size);
}
}
mdd_free(tmp);
assert(mdd_equal(refResult, res));
mdd_free(refResult);
mdd_free(res);
}
}
}
if (relationArray != newRelationArray) {
mdd_array_free(relationArray);
relationArray = newRelationArray;
}
}
if (info->option->checkEquivalence) {
assert(ImgCheckEquivalence(info, newVector, newRelationArray,
NIL(mdd_t), NIL(mdd_t), 0));
}
}
partial = 0;
one = mdd_one(info->manager);
splitMethod = info->option->splitMethod;
if (splitMethod == 0) {
r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t),
NIL(mdd_t), NIL(mdd_t), 0, 0, 0);
} else if (splitMethod == 1)
r = ImageByOutputSplit(info, newVector, one, 0);
else {
if (info->option->splitMethod == 0)
turnDepth = info->nVars + 1;
else
turnDepth = info->option->turnDepth;
if (turnDepth == 0) {
if (splitMethod == 2)
r = ImageByOutputSplit(info, newVector, one, 0);
else {
if (info->useConstraint && info->buildTR == 2) {
if (info->buildPartialTR) {
r = ImgImageByHybridWithStaticSplit(info, newVector, newFrom,
relationArray,
NIL(mdd_t), NIL(mdd_t));
} else {
r = ImgImageByHybridWithStaticSplit(info, NIL(array_t), newFrom,
relationArray,
NIL(mdd_t), NIL(mdd_t));
}
} else
r = ImgImageByHybrid(info, newVector, newFrom);
}
} else if (splitMethod == 2) {
r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t),
NIL(mdd_t), NIL(mdd_t),
splitMethod, turnDepth, 0);
} else {
if (info->useConstraint) {
if (info->buildTR) {
if (info->buildTR == 2) {
if (info->buildPartialTR) {
r = ImageByStaticInputSplit(info, newVector, newFrom,
relationArray, turnDepth, 0);
partial = 1;
} else {
r = ImageByStaticInputSplit(info, NIL(array_t), newFrom,
relationArray, turnDepth, 0);
}
} else if (info->option->delayedSplit) {
r = ImageByInputSplit(info, newVector, one, newFrom, relationArray,
cofactorCube, abstractCube,
splitMethod, turnDepth, 0);
} else {
r = ImageByInputSplit(info, newVector, one, newFrom, relationArray,
NIL(mdd_t), NIL(mdd_t),
splitMethod, turnDepth, 0);
}
} else {
r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t),
NIL(mdd_t), NIL(mdd_t),
splitMethod, turnDepth, 0);
}
} else if (info->buildTR == 1 && info->option->delayedSplit) {
r = ImageByInputSplit(info, newVector, one, NIL(mdd_t), relationArray,
cofactorCube, abstractCube,
splitMethod, turnDepth, 0);
} else {
r = ImageByInputSplit(info, newVector, one, NIL(mdd_t), relationArray,
NIL(mdd_t), NIL(mdd_t),
splitMethod, turnDepth, 0);
}
}
}
info->useConstraint = saveUseConstraint;
if (relationArray &&
!(info->option->debug && (partial || info->buildTR == 2))) {
mdd_array_free(relationArray);
}
if (info->imgCache && info->option->autoFlushCache == 1)
ImgFlushCache(info->imgCache);
mdd_free(one);
if (cofactorCube)
mdd_free(cofactorCube);
if (abstractCube)
mdd_free(abstractCube);
if (newFrom && newFrom != from)
mdd_free(newFrom);
res = bdd_and(r, cube, 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_and(%d,%d) = %d\n",
bdd_size(r), bdd_size(cube), size);
}
}
mdd_free(r);
mdd_free(cube);
if (newVector != info->vector)
ImgVectorFree(newVector);
if (info->option->debug) {
if (info->buildTR == 2) {
refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
relationArray,
NIL(mdd_t), NIL(mdd_t));
mdd_array_free(relationArray);
} else {
if (partial) {
refResult = ImgImageByHybrid(info, info->fullVector, from);
assert(mdd_equal(refResult, res));
mdd_free(refResult);
refResult = ImgImageByHybridWithStaticSplit(info, info->vector, from,
relationArray,
NIL(mdd_t), NIL(mdd_t));
mdd_array_free(relationArray);
} else
refResult = ImgImageByHybrid(info, info->vector, from);
}
assert(mdd_equal(refResult, res));
mdd_free(refResult);
}
if (info->option->findEssential)
info->lastFoundEssentialDepth = info->foundEssentialDepth;
if (info->option->printEssential == 2) {
maxDepth = info->maxDepth < IMG_TF_MAX_PRINT_DEPTH ?
info->maxDepth : IMG_TF_MAX_PRINT_DEPTH;
fprintf(vis_stdout, "foundEssential:");
for (i = 0; i < maxDepth; i++)
fprintf(vis_stdout, " [%d]%d", i, info->foundEssentials[i]);
fprintf(vis_stdout, "\n");
}
if (info->option->verbosity) {
fprintf(vis_stdout, "** tfm info: max intermediate BDD size = %d\n",
info->maxIntermediateSize);
}
if (info->option->debug)
assert(TfmCheckImageValidity(info, res));
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void PrintVectorDecomposition | ( | ImgTfmInfo_t * | info, |
| array_t * | vectorArray, | ||
| array_t * | varArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Print the information of the decomposition.]
Description [Print the information of the decomposition.]
SideEffects []
Definition at line 2945 of file imgTfmFwd.c.
{
int i, j, n;
int var, index;
ImgComponent_t *comp;
array_t *vector;
fprintf(vis_stdout, "** tfm info: vector decomposition\n");
n = array_n(vectorArray);
for (i = 0; i < n; i++) {
vector = array_fetch(array_t *, vectorArray, i);
var = array_fetch(int, varArray, i);
fprintf(vis_stdout, "Group[%d] : num = %d, split = %d\n",
i, array_n(vector), var);
for (j = 0; j < array_n(vector); j++) {
comp = array_fetch(ImgComponent_t *, vector, j);
index = (int)bdd_top_var_id(comp->var);
fprintf(vis_stdout, " %d", index);
}
fprintf(vis_stdout, "\n");
}
}
Here is the caller graph for this function:
| static int TfmCheckImageValidity | ( | ImgTfmInfo_t * | info, |
| mdd_t * | image | ||
| ) | [static] |
Function********************************************************************
Synopsis [Checks the support of image.]
Description [Checks the support of image.]
SideEffects []
Definition at line 2861 of file imgTfmFwd.c.
{
int i, id;
array_t *supportIds;
int status = 1;
supportIds = mdd_get_bdd_support_ids(info->manager, image);
for (i = 0; i < array_n(supportIds); i++) {
id = array_fetch(int, supportIds, i);
if (st_lookup(info->quantifyVarsTable, (char *)(long)id, NIL(char *))) {
fprintf(vis_stderr,
"** tfm error: image contains a primary input variable (%d)\n",
id);
status = 0;
}
if (st_lookup(info->rangeVarsTable, (char *)(long)id, NIL(char *))) {
fprintf(vis_stderr,
"** tfm error: image contains a range variable (%d)\n", id);
status = 0;
}
if (info->intermediateVarsTable &&
st_lookup(info->intermediateVarsTable, (char *)(long)id, NIL(char *))) {
fprintf(vis_stderr,
"** tfm error: image contains an intermediate variable (%d)\n",
id);
status = 0;
}
}
array_free(supportIds);
return(status);
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: imgTfmFwd.c,v 1.37 2005/04/22 19:45:46 jinh Exp $" [static] |
CFile***********************************************************************
FileName [imgTfmFwd.c]
PackageName [img]
Synopsis [Routines for image 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 37 of file imgTfmFwd.c.
