/**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.] ******************************************************************************/ #include "imgInt.h" static char rcsid[] UNUSED = "$Id: imgTfmFwd.c,v 1.37 2005/04/22 19:45:46 jinh Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Computes an image with transition function method.] Description [Computes an image with transition function method.] SideEffects [] ******************************************************************************/ mdd_t * ImgTfmImage(ImgTfmInfo_t *info, mdd_t *from) { 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); } /**Function******************************************************************** Synopsis [Chooses splitting variables for static splitting.] Description [Chooses splitting variables for static splitting.] SideEffects [] ******************************************************************************/ mdd_t * ImgChooseTrSplitVar(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, int trSplitMethod, int piSplitFlag) { 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); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Computes an image by input splitting.] Description [Computes an image by input splitting.] SideEffects [] ******************************************************************************/ 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) { 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); } /**Function******************************************************************** Synopsis [Computes an image by static input splitting.] Description [Computes an image by static input splitting.] SideEffects [] ******************************************************************************/ static mdd_t * ImageByStaticInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth) { 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); } /**Function******************************************************************** Synopsis [Computes an image by output splitting.] Description [Computes an image by output splitting.] SideEffects [] ******************************************************************************/ static mdd_t * ImageByOutputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, int depth) { 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); } /**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 [] ******************************************************************************/ 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) { 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); } /**Function******************************************************************** Synopsis [Fast image computation when function vector contains only two functions.] Description [Fast image computation when function vector contains only two functions.] SideEffects [] ******************************************************************************/ static mdd_t * ImageFast2(ImgTfmInfo_t *info, array_t *vector) { 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); } /**Function******************************************************************** Synopsis [Finds a decomposable variable (articulation)] Description [Finds a decomposable variable (articulation)] SideEffects [] ******************************************************************************/ static int FindDecomposableVariable(ImgTfmInfo_t *info, array_t *vector) { 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); } /**Function******************************************************************** Synopsis [Checks the support of image.] Description [Checks the support of image.] SideEffects [] ******************************************************************************/ static int TfmCheckImageValidity(ImgTfmInfo_t *info, mdd_t *image) { 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); } /**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 [] ******************************************************************************/ 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) { 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); } } } } /**Function******************************************************************** Synopsis [Print the information of the decomposition.] Description [Print the information of the decomposition.] SideEffects [] ******************************************************************************/ static void PrintVectorDecomposition(ImgTfmInfo_t *info, array_t *vectorArray, array_t *varArray) { 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"); } } /**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 [] ******************************************************************************/ static int CheckIfValidSplitOrGetNew(ImgTfmInfo_t *info, int split, array_t *vector, array_t *relationArray, mdd_t *from) { 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); } /**Function******************************************************************** Synopsis [Finds a splitting variable for input splitting.] Description [Finds a splitting variable for input splitting.] SideEffects [] ******************************************************************************/ static int ChooseInputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, int splitMethod, int decompose, int piSplitFlag, int *varOccur) { 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); } /**Function******************************************************************** Synopsis [Finds a splitting variable for output splitting.] Description [Finds a splitting variable for output splitting.] SideEffects [] ******************************************************************************/ static int ChooseOutputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, int splitMethod) { 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); }