/**CFile*********************************************************************** FileName [imgTfmBwd.c] PackageName [img] Synopsis [Routines for preimage computation using transition function method.] Description [] SeeAlso [] Author [In-Ho Moon] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] ******************************************************************************/ #include "imgInt.h" static char rcsid[] UNUSED = "$Id: imgTfmBwd.c,v 1.29 2002/08/18 04:47:07 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static bdd_t * PreImageByDomainCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int splitMethod, int turnDepth, int depth); static mdd_t * PreImageByStaticDomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth); static bdd_t * PreImageByConstraintCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, int splitMethod, int turnDepth, int depth); static mdd_t * PreImageBySubstitution(ImgTfmInfo_t *info, array_t *vector, mdd_t *from); static bdd_t * PreImageMakeVectorCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube); static bdd_t * PreImageMakeRelationCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray); static bdd_t * PreImageDeleteOneComponent(ImgTfmInfo_t *info, array_t *delta, int index, array_t **newDelta); static int PreImageChooseSplitVar(ImgTfmInfo_t *info, array_t *delta, bdd_t *img, int splitMethod, int split); static mdd_t * DomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *c, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube); static int CheckPreImageVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *image); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Computes a preimage with transition function method.] Description [Computes a preimage with transition function method.] SideEffects [] ******************************************************************************/ bdd_t * ImgTfmPreImage(ImgTfmInfo_t *info, bdd_t *image) { bdd_t *preImg, *pre; int turnDepth; bdd_t *refResult, *one; array_t *relationArray; int partial; bdd_t *from; array_t *vector; if (bdd_is_tautology(image, 1)) { preImg = mdd_one(info->manager); return(preImg); } else if (bdd_is_tautology(image, 0)) { preImg = mdd_zero(info->manager); return(preImg); } info->maxIntermediateSize = 0; if (info->buildTR) { if (info->option->preSplitMethod == 4 && info->option->preSplitMaxDepth < 0 && info->option->buildPartialTR == FALSE && info->preKeepPiInTr == FALSE && info->option->preCanonical == FALSE) { mdd_t *range; range = ImgSubstitute(image, info->functionData, Img_D2R_c); preImg = ImgBddLinearAndSmooth(info->manager, range, info->bwdClusteredRelationArray, info->bwdArraySmoothVarBddArray, info->bwdSmoothVarCubeArray, info->option->verbosity); mdd_free(range); return(preImg); } relationArray = mdd_array_duplicate(info->bwdClusteredRelationArray); } else relationArray = NIL(array_t); one = mdd_one(info->manager); vector = info->vector; from = image; partial = 0; if (info->option->preSplitMethod == 0) { preImg = PreImageByDomainCofactoring(info, vector, from, NIL(array_t), NIL(mdd_t), NIL(mdd_t), info->option->preSplitMethod, 0, 0); } else if (info->option->preSplitMethod == 1) { preImg = PreImageByConstraintCofactoring(info, vector, from, info->option->preSplitMethod, 0, 0); } else if (info->option->preSplitMethod == 3) { preImg = PreImageBySubstitution(info, vector, from); } else { turnDepth = info->option->turnDepth; if (turnDepth == 0) { if (info->option->preSplitMethod == 2) { preImg = PreImageByConstraintCofactoring(info, vector, from, info->option->preSplitMethod, turnDepth, 0); } else preImg = ImgPreImageByHybrid(info, vector, from); } else if (info->option->preSplitMethod == 2) { preImg = PreImageByDomainCofactoring(info, vector, from, relationArray, NIL(mdd_t), NIL(mdd_t), info->option->preSplitMethod, turnDepth, 0); } else { if (info->buildTR) { if (info->buildTR == 2) { if (info->buildPartialTR) { preImg = PreImageByStaticDomainCofactoring(info, vector, from, relationArray, turnDepth, 0); partial = 1; } else { preImg = PreImageByStaticDomainCofactoring(info, NIL(array_t), from, relationArray, turnDepth, 0); } } else if (info->option->delayedSplit) { preImg = PreImageByDomainCofactoring(info, vector, from, relationArray, one, one, info->option->preSplitMethod, turnDepth, 0); } else { preImg = PreImageByDomainCofactoring(info, vector, from, relationArray, NIL(mdd_t), NIL(mdd_t), info->option->preSplitMethod, turnDepth, 0); } } else { preImg = PreImageByDomainCofactoring(info, vector, from, relationArray, NIL(mdd_t), NIL(mdd_t), info->option->preSplitMethod, turnDepth, 0); } } } mdd_free(one); if (info->option->debug) { if (info->buildTR == 2) { refResult = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), image, relationArray, NIL(mdd_t), NIL(mdd_t)); } else { if (partial) { refResult = ImgPreImageByHybridWithStaticSplit(info, info->vector, image, relationArray, NIL(mdd_t), NIL(mdd_t)); } else refResult = ImgPreImageByHybrid(info, info->vector, image); } assert(mdd_equal_mod_care_set_array(refResult, preImg, info->toCareSetArray)); mdd_free(refResult); } if (relationArray) mdd_array_free(relationArray); if (info->preCache && info->option->autoFlushCache == 1) ImgFlushCache(info->preCache); if (info->preKeepPiInTr == TRUE) { if (info->functionData->quantifyCube) pre = bdd_smooth_with_cube(preImg, info->functionData->quantifyCube); else pre = bdd_smooth(preImg, info->functionData->quantifyBddVars); mdd_free(preImg); } else pre = preImg; if (info->option->verbosity) { fprintf(vis_stdout, "** tfm info: max BDD size for intermediate product = %d\n", info->maxIntermediateSize); } return(pre); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Computes preimage with domain cofactoring method.] Description [Computes preimage with domain cofactoring method.] SideEffects [] ******************************************************************************/ static bdd_t * PreImageByDomainCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int splitMethod, int turnDepth, int depth) { array_t *newDelta, *tmpDelta, *vectorT, *vectorE; bdd_t *preImg, *preImgT, *preImgE, *imgT, *imgE, *newImg, *tmpImg; int split; bdd_t *var, *varNot, *refResult; int nRecur; array_t *relationArrayT, *relationArrayE; array_t *newRelationArray, *tmpRelationArray; mdd_t *cofactorCubeT, *cofactorCubeE; mdd_t *abstractCubeT, *abstractCubeE; mdd_t *newCofactorCube, *newAbstractCube; mdd_t *cofactor, *abstract; mdd_t *essentialCube, *tmp; int findEssential; int foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE; int turnFlag, size; mdd_t *saveCareSet = NIL(mdd_t); newRelationArray = NIL(array_t); if (info->option->checkEquivalence && relationArray) { assert(ImgCheckEquivalence(info, delta, relationArray, cofactorCube, abstractCube, 1)); } info->nRecursionB++; if (info->option->debug) { if (relationArray) { refResult = ImgPreImageByHybrid(info, delta, image); preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), image, relationArray, cofactorCube, abstractCube); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = preImg; preImg = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); assert(mdd_equal_mod_care_set_array(refResult, preImg, info->toCareSetArray)); mdd_free(refResult); mdd_free(preImg); } } if (info->nIntermediateVars) size = ImgVectorFunctionSize(delta); else size = array_n(delta); if (size == 1) { preImg = PreImageBySubstitution(info, delta, image); info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; info->foundEssentialDepth = info->option->maxEssentialDepth; return(preImg); } if (info->option->findEssential) { if (info->option->findEssential == 1) findEssential = 1; else { if (depth >= info->lastFoundEssentialDepth) findEssential = 1; else findEssential = 0; } } else findEssential = 0; if (findEssential) { essentialCube = bdd_find_essential_cube(image); if (!bdd_is_tautology(essentialCube, 1)) { info->averageFoundEssential = (info->averageFoundEssential * (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) / (float)(info->nFoundEssentials + 1); info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth * (float)info->nFoundEssentials + (float)depth) / (float)(info->nFoundEssentials + 1); if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth) info->topFoundEssentialDepth = depth; if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH) info->foundEssentials[depth]++; info->nFoundEssentials++; if (info->option->delayedSplit && relationArray) { tmpRelationArray = relationArray; tmpImg = ImgVectorMinimize(info, delta, essentialCube, image, tmpRelationArray, &tmpDelta, NIL(mdd_t *), NIL(array_t *), &cofactor, &abstract); if (bdd_is_tautology(cofactor, 1)) newCofactorCube = cofactorCube; else newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1); mdd_free(cofactor); if (bdd_is_tautology(abstract, 1)) newAbstractCube = abstractCube; else newAbstractCube = mdd_and(abstractCube, abstract, 1, 1); mdd_free(abstract); } else { if (relationArray) tmpRelationArray = mdd_array_duplicate(relationArray); else tmpRelationArray = relationArray; tmpImg = ImgVectorMinimize(info, delta, essentialCube, image, tmpRelationArray, &tmpDelta, NIL(mdd_t *), NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *)); newCofactorCube = cofactorCube; newAbstractCube = abstractCube; } foundEssentialDepth = depth; } else { tmpDelta = delta; tmpRelationArray = relationArray; tmpImg = image; newCofactorCube = cofactorCube; newAbstractCube = abstractCube; foundEssentialDepth = info->option->maxEssentialDepth; } mdd_free(essentialCube); foundEssentialDepthT = info->option->maxEssentialDepth; foundEssentialDepthE = info->option->maxEssentialDepth; } else { tmpDelta = delta; tmpRelationArray = relationArray; tmpImg = image; newCofactorCube = cofactorCube; newAbstractCube = abstractCube; /* To remove compiler warnings */ foundEssentialDepth = -1; foundEssentialDepthT = -1; foundEssentialDepthE = -1; } if (!info->option->preCanonical) { newImg = tmpImg; newDelta = tmpDelta; newRelationArray = tmpRelationArray; } else if (info->option->delayedSplit && relationArray) { newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg, tmpRelationArray, &newDelta, &newRelationArray, &cofactor, &abstract); if (!bdd_is_tautology(cofactor, 1)) { if (newCofactorCube == cofactorCube) newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1); else { tmp = newCofactorCube; newCofactorCube = mdd_and(tmp, cofactor, 1, 1); mdd_free(tmp); } } mdd_free(cofactor); if (!bdd_is_tautology(abstract, 1)) { if (newAbstractCube == abstractCube) newAbstractCube = mdd_and(abstractCube, abstract, 1, 1); else { tmp = newAbstractCube; newAbstractCube = mdd_and(tmp, abstract, 1, 1); mdd_free(tmp); } } mdd_free(abstract); } else { newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg, tmpRelationArray, &newDelta, &newRelationArray, NIL(mdd_t *), NIL(mdd_t *)); } if (tmpDelta != delta) ImgVectorFree(tmpDelta); if (tmpImg != image) mdd_free(tmpImg); if (tmpRelationArray && tmpRelationArray != relationArray && tmpRelationArray != newRelationArray) { mdd_array_free(tmpRelationArray); } if (info->option->debug) { if (relationArray) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg, newRelationArray, newCofactorCube, newAbstractCube); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = preImg; preImg = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); assert(mdd_equal_mod_care_set_array(refResult, preImg, info->toCareSetArray)); mdd_free(refResult); mdd_free(preImg); } } if (bdd_is_tautology(newImg, 1) || bdd_is_tautology(newImg, 0)) { info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(newImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } if (newDelta != delta) ImgVectorFree(newDelta); if (relationArray && newRelationArray != relationArray) mdd_array_free(newRelationArray); if (newCofactorCube && newCofactorCube != cofactorCube) mdd_free(newCofactorCube); if (newAbstractCube && newAbstractCube != abstractCube) mdd_free(newAbstractCube); if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(newImg); } if (array_n(newDelta) <= 1) { if (array_n(newDelta) == 0) preImg = newImg; else { assert(array_n(newDelta) == 1); preImg = PreImageBySubstitution(info, newDelta, newImg); mdd_free(newImg); } info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; if (info->option->debug) { refResult = ImgPreImageByHybrid(info, delta, image); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(preImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } if (newDelta != delta) ImgVectorFree(newDelta); if (relationArray && newRelationArray != relationArray) mdd_array_free(newRelationArray); if (newCofactorCube && newCofactorCube != cofactorCube) mdd_free(newCofactorCube); if (newAbstractCube && newAbstractCube != abstractCube) mdd_free(newAbstractCube); if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(preImg); } if (info->preCache) { preImg = ImgCacheLookupTable(info, info->preCache, newDelta, newImg); if (preImg) { info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(preImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } if (newDelta != delta) ImgVectorFree(newDelta); if (newImg != image) mdd_free(newImg); if (relationArray && newRelationArray != relationArray) mdd_array_free(newRelationArray); if (newCofactorCube && newCofactorCube != cofactorCube) mdd_free(newCofactorCube); if (newAbstractCube && newAbstractCube != abstractCube) mdd_free(newAbstractCube); if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(preImg); } } turnFlag = 0; if (splitMethod == 4 && turnDepth == -1) { if (depth < info->option->preSplitMinDepth) { info->nSplitsB++; turnFlag = 0; } else if (depth > info->option->preSplitMaxDepth) { info->nConjoinsB++; turnFlag = 1; } else { turnFlag = ImgDecideSplitOrConjoin(info, newDelta, newImg, 1, newRelationArray, newCofactorCube, newAbstractCube, 0, depth); } } else { if (depth == turnDepth) turnFlag = 1; else turnFlag = 0; } if (turnFlag) { if (splitMethod == 2) { preImg = PreImageByConstraintCofactoring(info, newDelta, newImg, info->option->preSplitMethod, 0, depth + 1); } else { if (relationArray) { preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg, newRelationArray, newCofactorCube, newAbstractCube); } else preImg = ImgPreImageByHybrid(info, newDelta, newImg); } if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(preImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } if (splitMethod == 4) { if (info->preCache) ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); else { if (newDelta != delta) ImgVectorFree(newDelta); if (newImg != image) mdd_free(newImg); } info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; } else { if (newDelta != delta) ImgVectorFree(newDelta); if (newImg != image) mdd_free(newImg); } if (relationArray && newRelationArray != relationArray) mdd_array_free(newRelationArray); if (newCofactorCube && newCofactorCube != cofactorCube) mdd_free(newCofactorCube); if (newAbstractCube && newAbstractCube != abstractCube) mdd_free(newAbstractCube); info->nTurnsB++; if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(preImg); } split = PreImageChooseSplitVar(info, newDelta, newImg, 0, info->option->preInputSplit); /* No more present state variable to split */ if (split == -1) { if (info->option->preDcLeafMethod == 0 || info->option->preDcLeafMethod == 2) { if (info->option->preDcLeafMethod == 0) preImg = PreImageBySubstitution(info, newDelta, newImg); else if (relationArray) { preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg, newRelationArray, newCofactorCube, newAbstractCube); } else preImg = ImgPreImageByHybrid(info, newDelta, newImg); if (info->preCache) ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; } else { preImg = PreImageByConstraintCofactoring(info, newDelta, newImg, splitMethod, turnDepth, depth + 1); info->nRecursionB--; } if (splitMethod == 0) info->nTurnsB++; if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(preImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } if (info->option->preDcLeafMethod != 0 || !info->preCache) { if (newDelta != delta) ImgVectorFree(newDelta); if (newImg != image) mdd_free(newImg); } if (relationArray && newRelationArray != relationArray) mdd_array_free(newRelationArray); if (newCofactorCube && newCofactorCube != cofactorCube) mdd_free(newCofactorCube); if (newAbstractCube && newAbstractCube != abstractCube) mdd_free(newAbstractCube); if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(preImg); } var = bdd_var_with_index(info->manager, split); varNot = mdd_not(var); if (info->option->delayedSplit && relationArray) { imgT = DomainCofactoring(info, newDelta, newImg, newRelationArray, var, &vectorT, &relationArrayT, &cofactor, &abstract); if (bdd_is_tautology(cofactor, 1)) cofactorCubeT = newCofactorCube; else cofactorCubeT = mdd_and(newCofactorCube, cofactor, 1, 1); mdd_free(cofactor); if (bdd_is_tautology(abstract, 1)) abstractCubeT = newAbstractCube; else abstractCubeT = mdd_and(newAbstractCube, abstract, 1, 1); mdd_free(abstract); imgE = DomainCofactoring(info, newDelta, newImg, newRelationArray, varNot, &vectorE, &relationArrayE, &cofactor, &abstract); if (bdd_is_tautology(cofactor, 1)) cofactorCubeE = newCofactorCube; else cofactorCubeE = mdd_and(newCofactorCube, cofactor, 1, 1); mdd_free(cofactor); if (bdd_is_tautology(abstract, 1)) abstractCubeE = newAbstractCube; else abstractCubeE = mdd_and(newAbstractCube, abstract, 1, 1); mdd_free(abstract); } else { imgT = DomainCofactoring(info, newDelta, newImg, newRelationArray, var, &vectorT, &relationArrayT, NIL(mdd_t *), NIL(mdd_t *)); cofactorCubeT = NIL(mdd_t); abstractCubeT = NIL(mdd_t); imgE = DomainCofactoring(info, newDelta, newImg, newRelationArray, varNot, &vectorE, &relationArrayE, NIL(mdd_t *), NIL(mdd_t *)); cofactorCubeE = NIL(mdd_t); abstractCubeE = NIL(mdd_t); } if (relationArray && newRelationArray != relationArray) mdd_array_free(newRelationArray); mdd_free(varNot); if (!info->preCache && !info->option->debug) { if (newDelta != delta) ImgVectorFree(newDelta); if (newImg != image) mdd_free(newImg); } nRecur = 0; if (bdd_is_tautology(imgT, 1)) preImgT = mdd_one(info->manager); else if (bdd_is_tautology(imgT, 0)) preImgT = mdd_zero(info->manager); else { if (info->option->debug) { saveCareSet = info->debugCareSet; info->debugCareSet = mdd_and(saveCareSet, var, 1, 1); } preImgT = PreImageByDomainCofactoring(info, vectorT, imgT, relationArrayT, cofactorCubeT, abstractCubeT, splitMethod, turnDepth, depth + 1); if (info->option->debug) { mdd_free(info->debugCareSet); info->debugCareSet = saveCareSet; } if (findEssential) foundEssentialDepthT = info->foundEssentialDepth; nRecur++; } ImgVectorFree(vectorT); mdd_free(imgT); if (relationArrayT && relationArrayT != newRelationArray) mdd_array_free(relationArrayT); if (cofactorCubeT && cofactorCubeT != newCofactorCube) mdd_free(cofactorCubeT); if (abstractCubeT && abstractCubeT != newAbstractCube) mdd_free(abstractCubeT); if (bdd_is_tautology(imgE, 1)) preImgE = mdd_one(info->manager); else if (bdd_is_tautology(imgE, 0)) preImgE = mdd_zero(info->manager); else { if (info->option->debug) { saveCareSet = info->debugCareSet; info->debugCareSet = mdd_and(saveCareSet, var, 1, 0); } preImgE = PreImageByDomainCofactoring(info, vectorE, imgE, relationArrayE, cofactorCubeE, abstractCubeE, splitMethod, turnDepth, depth + 1); if (info->option->debug) { mdd_free(info->debugCareSet); info->debugCareSet = saveCareSet; } if (findEssential) foundEssentialDepthE = info->foundEssentialDepth; nRecur++; } ImgVectorFree(vectorE); mdd_free(imgE); if (relationArrayE && relationArrayT != newRelationArray) mdd_array_free(relationArrayE); if (cofactorCubeE && cofactorCubeE != newCofactorCube) mdd_free(cofactorCubeE); if (abstractCubeE && abstractCubeE != newAbstractCube) mdd_free(abstractCubeE); if (newCofactorCube && newCofactorCube != cofactorCube) mdd_free(newCofactorCube); if (newAbstractCube && newAbstractCube != abstractCube) mdd_free(newAbstractCube); preImg = bdd_ite(var, preImgT, preImgE, 1, 1, 1); if (info->option->verbosity) { size = bdd_size(preImg); if (size > info->maxIntermediateSize) info->maxIntermediateSize = size; if (info->option->printBddSize) { fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n", bdd_size(preImgT), bdd_size(preImgE), bdd_size(preImg)); } } mdd_free(var); mdd_free(preImgE); mdd_free(preImgT); if (info->preCache) ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(preImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); if (!info->preCache) { if (newDelta != delta) ImgVectorFree(newDelta); if (newImg != image) mdd_free(newImg); } } if (nRecur == 0) { info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; } if (findEssential) { if (foundEssentialDepth == info->option->maxEssentialDepth) { if (foundEssentialDepthT < foundEssentialDepthE) foundEssentialDepth = foundEssentialDepthT; else foundEssentialDepth = foundEssentialDepthE; } info->foundEssentialDepth = foundEssentialDepth; } return(preImg); } /**Function******************************************************************** Synopsis [Computes a preimage by static input splitting.] Description [Computes a preimage by static input splitting.] SideEffects [] ******************************************************************************/ static mdd_t * PreImageByStaticDomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth) { array_t *vectorT, *vectorE, *newVector; mdd_t *resT, *resE, *res, *cubeT, *cubeE; mdd_t *fromT, *fromE, *newFrom, *tmpFrom; mdd_t *var, *varNot; array_t *relationArrayT, *relationArrayE; array_t *newRelationArray, *tmpRelationArray; int nRecur; mdd_t *essentialCube, *refResult; int findEssential; int foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE; int turnFlag, size; mdd_t *saveCareSet = NIL(mdd_t), *tmp; info->nRecursionB++; turnFlag = 0; if (turnDepth == -1) { if (depth < info->option->preSplitMinDepth) { info->nSplitsB++; turnFlag = 0; } else if (depth > info->option->preSplitMaxDepth) { info->nConjoinsB++; turnFlag = 1; } else { turnFlag = ImgDecideSplitOrConjoin(info, vector, from, 1, relationArray, NIL(mdd_t), NIL(mdd_t), 1, depth); } } else { if (depth == turnDepth) turnFlag = 1; else turnFlag = 0; } if (turnFlag) { res = ImgPreImageByHybridWithStaticSplit(info, vector, from, relationArray, NIL(mdd_t), NIL(mdd_t)); info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; info->foundEssentialDepth = info->option->maxEssentialDepth; return(res); } if (info->option->findEssential) { if (info->option->findEssential == 1) findEssential = 1; else { if (depth >= info->lastFoundEssentialDepth) findEssential = 1; else findEssential = 0; } } else findEssential = 0; if (findEssential) { essentialCube = bdd_find_essential_cube(from); if (!bdd_is_tautology(essentialCube, 1)) { info->averageFoundEssential = (info->averageFoundEssential * (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) / (float)(info->nFoundEssentials + 1); info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth * (float)info->nFoundEssentials + (float)depth) / (float)(info->nFoundEssentials + 1); if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth) info->topFoundEssentialDepth = depth; if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH) info->foundEssentials[depth]++; info->nFoundEssentials++; if (vector) { array_t *tmpVector; if (info->option->preCanonical) { tmpFrom = PreImageMakeRelationCanonical(info, vector, from, relationArray, &newVector, &newRelationArray); } else { tmpFrom = from; newVector = vector; newRelationArray = relationArray; } tmpVector = newVector; newFrom = ImgVectorMinimize(info, tmpVector, essentialCube, tmpFrom, newRelationArray, &newVector, NIL(mdd_t *), NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *)); if (tmpVector != vector) ImgVectorFree(tmpVector); if (tmpFrom != from) mdd_free(tmpFrom); } else { tmpRelationArray = ImgGetCofactoredRelationArray(relationArray, essentialCube); if (info->option->preCanonical) { newFrom = PreImageMakeRelationCanonical(info, vector, from, tmpRelationArray, &newVector, &newRelationArray); mdd_array_free(tmpRelationArray); } else { newFrom = from; newVector = vector; newRelationArray = tmpRelationArray; } } foundEssentialDepth = depth; } else { if (info->option->preCanonical) { newFrom = PreImageMakeRelationCanonical(info, vector, from, relationArray, &newVector, &newRelationArray); } else { newFrom = from; newVector = vector; newRelationArray = relationArray; } foundEssentialDepth = info->option->maxEssentialDepth; } mdd_free(essentialCube); foundEssentialDepthT = info->option->maxEssentialDepth; foundEssentialDepthE = info->option->maxEssentialDepth; } else { if (info->option->preCanonical) { newFrom = PreImageMakeRelationCanonical(info, vector, from, relationArray, &newVector, &newRelationArray); } else { newFrom = from; newVector = vector; newRelationArray = relationArray; } /* To remove compiler warnings */ foundEssentialDepth = -1; foundEssentialDepthT = -1; foundEssentialDepthE = -1; } if (info->option->debug) { refResult = ImgPreImageByHybridWithStaticSplit(info, vector, from, relationArray, NIL(mdd_t), NIL(mdd_t)); res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom, newRelationArray, NIL(mdd_t), NIL(mdd_t)); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = res; res = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); assert(mdd_equal_mod_care_set_array(refResult, res, info->toCareSetArray)); mdd_free(refResult); mdd_free(res); } if (bdd_is_tautology(newFrom, 1)) { if (newVector && newVector != vector) ImgVectorFree(newVector); if (newRelationArray != relationArray) mdd_array_free(newRelationArray); if (newFrom != from) mdd_free(newFrom); info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(mdd_one(info->manager)); } if (depth == turnDepth || (info->option->splitCubeFunc && bdd_is_cube(newFrom))) { res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom, newRelationArray, NIL(mdd_t), NIL(mdd_t)); if (newVector && newVector != vector) ImgVectorFree(newVector); if (newRelationArray != relationArray) mdd_array_free(newRelationArray); if (newFrom != from) mdd_free(newFrom); info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(res); } var = ImgChooseTrSplitVar(info, newVector, newRelationArray, info->option->trSplitMethod, 0); if (!var) { res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom, newRelationArray, NIL(mdd_t), NIL(mdd_t)); if (newVector && newVector != vector) ImgVectorFree(newVector); if (newRelationArray != relationArray) mdd_array_free(newRelationArray); if (newFrom != from) mdd_free(newFrom); info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(res); } varNot = mdd_not(var); nRecur = 0; if (newVector) { ImgVectorConstrain(info, newVector, var, NIL(array_t), &vectorT, &cubeT, NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *), TRUE); fromT = bdd_cofactor(newFrom, cubeT); mdd_free(cubeT); } else { vectorT = NIL(array_t); fromT = mdd_dup(newFrom); } relationArrayT = ImgGetCofactoredRelationArray(newRelationArray, var); if (bdd_is_tautology(fromT, 1)) { resT = mdd_one(info->manager); if (vectorT) ImgVectorFree(vectorT); } else if (bdd_is_tautology(fromT, 0)) { resT = mdd_zero(info->manager); if (vectorT) ImgVectorFree(vectorT); } else { if (info->option->debug) { saveCareSet = info->debugCareSet; info->debugCareSet = mdd_and(saveCareSet, var, 1, 1); } resT = PreImageByStaticDomainCofactoring(info, vectorT, fromT, relationArrayT, turnDepth, depth + 1); if (info->option->debug) { mdd_free(info->debugCareSet); info->debugCareSet = saveCareSet; } if (findEssential) foundEssentialDepthE = info->foundEssentialDepth; if (vectorT) ImgVectorFree(vectorT); nRecur++; } mdd_free(fromT); mdd_array_free(relationArrayT); if (newVector) { ImgVectorConstrain(info, newVector, varNot, NIL(array_t), &vectorE, &cubeE, NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *), TRUE); if (newVector != vector) ImgVectorFree(newVector); fromE = bdd_cofactor(newFrom, cubeE); mdd_free(cubeE); } else { vectorE = NIL(array_t); fromE = mdd_dup(newFrom); } if (newFrom != from) mdd_free(newFrom); relationArrayE = ImgGetCofactoredRelationArray(newRelationArray, varNot); if (newRelationArray != relationArray) mdd_array_free(newRelationArray); if (bdd_is_tautology(fromE, 1)) { resE = mdd_one(info->manager); if (vectorE) ImgVectorFree(vectorE); } else if (bdd_is_tautology(fromE, 0)) { resE = mdd_zero(info->manager); if (vectorE) ImgVectorFree(vectorE); } else { if (info->option->debug) { saveCareSet = info->debugCareSet; info->debugCareSet = mdd_and(saveCareSet, var, 1, 0); } resE = PreImageByStaticDomainCofactoring(info, vectorE, fromE, relationArrayE, turnDepth, depth + 1); if (info->option->debug) { mdd_free(info->debugCareSet); info->debugCareSet = saveCareSet; } if (findEssential) foundEssentialDepthE = info->foundEssentialDepth; if (vectorE) ImgVectorFree(vectorE); nRecur++; } mdd_free(fromE); mdd_array_free(relationArrayE); res = bdd_ite(var, resT, resE, 1, 1, 1); if (info->option->verbosity) { size = bdd_size(res); if (size > info->maxIntermediateSize) info->maxIntermediateSize = size; if (info->option->printBddSize) { fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n", bdd_size(resT), bdd_size(resE), bdd_size(res)); } } mdd_free(resT); mdd_free(resE); mdd_free(var); mdd_free(varNot); if (info->option->debug) { refResult = ImgPreImageByHybridWithStaticSplit(info, vector, from, relationArray, NIL(mdd_t), NIL(mdd_t)); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(res, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } if (nRecur == 0) { info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; } if (findEssential) { if (foundEssentialDepth == info->option->maxEssentialDepth) { if (foundEssentialDepthT < foundEssentialDepthE) foundEssentialDepth = foundEssentialDepthT; else foundEssentialDepth = foundEssentialDepthE; } info->foundEssentialDepth = foundEssentialDepth; } return(res); } /**Function******************************************************************** Synopsis [Computes preimage with constraint cofactoring method.] Description [Computes preimage with constraint cofactoring method.] SideEffects [] ******************************************************************************/ static bdd_t * PreImageByConstraintCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, int splitMethod, int turnDepth, int depth) { array_t *newDelta, *tmpDelta, *vector; bdd_t *preImg, *preImgT, *preImgE, *imgT, *imgE; bdd_t *c, *newImg, *tmpImg; int split; bdd_t *var, *varNot, *refResult; ImgComponent_t *comp; int nRecur, size; mdd_t *essentialCube; int findEssential; int foundEssentialDepth; int foundEssentialDepthT, foundEssentialDepthE; mdd_t *saveCareSet = NIL(mdd_t), *tmp; info->nRecursionB++; if (info->nIntermediateVars) size = ImgVectorFunctionSize(delta); else size = array_n(delta); if (size == 1) { preImg = PreImageBySubstitution(info, delta, image); info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; info->foundEssentialDepth = info->option->maxEssentialDepth; return(preImg); } if (info->option->findEssential) { if (info->option->findEssential == 1) findEssential = 1; else { if (depth >= info->lastFoundEssentialDepth) findEssential = 1; else findEssential = 0; } } else findEssential = 0; if (findEssential) { essentialCube = bdd_find_essential_cube(image); if (!bdd_is_tautology(essentialCube, 1)) { info->averageFoundEssential = (info->averageFoundEssential * (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) / (float)(info->nFoundEssentials + 1); info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth * (float)info->nFoundEssentials + (float)depth) / (float)(info->nFoundEssentials + 1); if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth) info->topFoundEssentialDepth = depth; if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH) info->foundEssentials[depth]++; info->nFoundEssentials++; tmpImg = ImgVectorMinimize(info, delta, essentialCube, image, NIL(array_t), &tmpDelta, NIL(mdd_t *), NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *)); foundEssentialDepth = depth; } else { tmpDelta = delta; tmpImg = image; foundEssentialDepth = info->option->maxEssentialDepth; } mdd_free(essentialCube); foundEssentialDepthT = info->option->maxEssentialDepth; foundEssentialDepthE = info->option->maxEssentialDepth; } else { tmpDelta = delta; tmpImg = image; /* To remove compiler warnings */ foundEssentialDepth = -1; foundEssentialDepthT = -1; foundEssentialDepthE = -1; } if (info->option->preCanonical) { newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg, NIL(array_t), &newDelta, NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *)); } else { newImg = tmpImg; newDelta = tmpDelta; } if (tmpDelta != delta) ImgVectorFree(tmpDelta); if (tmpImg != image) mdd_free(tmpImg); if (bdd_is_tautology(newImg, 1) || bdd_is_tautology(newImg, 0)) { info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(newImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } ImgVectorFree(newDelta); if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(newImg); } if (info->preCache) { preImg = ImgCacheLookupTable(info, info->preCache, newDelta, newImg); if (preImg) { info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(preImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } ImgVectorFree(newDelta); mdd_free(newImg); if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(preImg); } } if (depth == turnDepth) { preImg = ImgPreImageByHybrid(info, newDelta, newImg); if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(preImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); } if (info->preCache) ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); else { ImgVectorFree(newDelta); mdd_free(newImg); } info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; info->nTurnsB++; if (findEssential) info->foundEssentialDepth = foundEssentialDepth; return(preImg); } split = PreImageChooseSplitVar(info, newDelta, newImg, 1, info->option->preOutputSplit); comp = array_fetch(ImgComponent_t *, newDelta, split); var = mdd_dup(comp->var); varNot = mdd_not(var); imgE = bdd_cofactor(newImg, varNot); mdd_free(varNot); imgT = bdd_cofactor(newImg, var); mdd_free(var); if (!info->preCache && !info->option->debug) mdd_free(newImg); c = PreImageDeleteOneComponent(info, newDelta, split, &vector); if (!info->preCache && !info->option->debug) ImgVectorFree(newDelta); nRecur = 0; if (bdd_is_tautology(imgT, 1)) preImgT = mdd_one(info->manager); else if (bdd_is_tautology(imgT, 0)) preImgT = mdd_zero(info->manager); else { if (info->option->debug) { saveCareSet = info->debugCareSet; info->debugCareSet = mdd_and(saveCareSet, c, 1, 1); } preImgT = PreImageByConstraintCofactoring(info, vector, imgT, splitMethod, turnDepth, depth + 1); if (info->option->debug) { mdd_free(info->debugCareSet); info->debugCareSet = saveCareSet; } if (findEssential) foundEssentialDepthT = info->foundEssentialDepth; nRecur++; } mdd_free(imgT); if (bdd_is_tautology(imgE, 1)) preImgE = mdd_one(info->manager); else if (bdd_is_tautology(imgE, 0)) preImgE = mdd_zero(info->manager); else { if (info->option->debug) { saveCareSet = info->debugCareSet; info->debugCareSet = mdd_and(saveCareSet, c, 1, 0); } preImgE = PreImageByConstraintCofactoring(info, vector, imgE, splitMethod, turnDepth, depth + 1); if (info->option->debug) { mdd_free(info->debugCareSet); info->debugCareSet = saveCareSet; } if (findEssential) foundEssentialDepthE = info->foundEssentialDepth; nRecur++; } mdd_free(imgE); ImgVectorFree(vector); preImg = bdd_ite(c, preImgT, preImgE, 1, 1, 1); if (info->option->verbosity) { size = bdd_size(preImg); if (size > info->maxIntermediateSize) info->maxIntermediateSize = size; if (info->option->printBddSize) { fprintf(vis_stdout, "** tfm info: bdd_ite(%d,%d,%d) = %d\n", bdd_size(c), bdd_size(preImgT), bdd_size(preImgE), bdd_size(preImg)); } } mdd_free(c); mdd_free(preImgT); mdd_free(preImgE); if (info->preCache) ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); if (info->option->debug) { refResult = ImgPreImageByHybrid(info, newDelta, newImg); tmp = refResult; refResult = mdd_and(tmp, info->debugCareSet, 1, 1); mdd_free(tmp); tmp = mdd_and(preImg, info->debugCareSet, 1, 1); assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); mdd_free(refResult); mdd_free(tmp); if (!info->preCache) { ImgVectorFree(newDelta); mdd_free(newImg); } } if (nRecur == 0) { info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + (float)depth) / (float)(info->nLeavesB + 1); if (depth > info->maxDepthB) info->maxDepthB = depth; info->nLeavesB++; } if (findEssential) { if (foundEssentialDepth == info->option->maxEssentialDepth) { if (foundEssentialDepthT < foundEssentialDepthE) foundEssentialDepth = foundEssentialDepthT; else foundEssentialDepth = foundEssentialDepthE; } info->foundEssentialDepth = foundEssentialDepth; } return(preImg); } /**Function******************************************************************** Synopsis [Computes a preimage by Filkorn's substitution.] Description [Computes a preimage by Filkorn's substitution.] SideEffects [] ******************************************************************************/ static mdd_t * PreImageBySubstitution(ImgTfmInfo_t *info, array_t *vector, mdd_t *from) { int i, index; ImgComponent_t *comp, *fromComp; array_t *varArray, *funcArray; mdd_t *result; if (bdd_is_tautology(from, 1)) return(mdd_one(info->manager)); else if (bdd_is_tautology(from, 0)) return(mdd_zero(info->manager)); fromComp = ImgComponentAlloc(info); fromComp->func = from; ImgComponentGetSupport(fromComp); varArray = array_alloc(mdd_t *, 0); funcArray = array_alloc(mdd_t *, 0); for (i = 0; i < array_n(vector); i++) { comp = array_fetch(ImgComponent_t *, vector, i); index = bdd_top_var_id(comp->var); if (fromComp->support[index] || comp->intermediate) { array_insert_last(mdd_t *, varArray, comp->var); array_insert_last(mdd_t *, funcArray, comp->func); } } fromComp->func = NIL(mdd_t); ImgComponentFree(fromComp); result = bdd_vector_compose(from, varArray, funcArray); array_free(varArray); array_free(funcArray); /* quantify all primary inputs */ if (info->preKeepPiInTr == FALSE) { array_t *quantifyVarBddArray; mdd_t *tmp; if (info->newQuantifyBddVars) quantifyVarBddArray = info->newQuantifyBddVars; else quantifyVarBddArray = info->quantifyVarBddArray; tmp = result; result = bdd_smooth(tmp, quantifyVarBddArray); mdd_free(tmp); } return(result); } /**Function******************************************************************** Synopsis [Makes a vector canonical for preimage.] Description [Makes a vector canonical for preimage. Delete all the components which doesn't appear as a support in the image. If a component is constant, simplify the image with the constant value and delete the corresponding component from delta Side effect on delta. Return new image.] SideEffects [] ******************************************************************************/ static bdd_t * PreImageMakeVectorCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube) { array_t *tmpVector, *cofactoredVector; bdd_t *simple, *tmp, *newImage; ImgComponent_t *comp, *comp1, *imgComp; int i, id, n, pos; st_table *equivTable; int *ptr, *regularPtr; mdd_t *var, *cofactor, *abstract, *nsVar; array_t *tmpRelationArray; int changed = 0; newImage = mdd_dup(image); imgComp = ImgComponentAlloc(info); imgComp->func = image; ImgComponentGetSupport(imgComp); if (relationArray) { cofactor = mdd_one(info->manager); abstract = mdd_one(info->manager); } else { cofactor = NIL(mdd_t); abstract = NIL(mdd_t); } if (info->nIntermediateVars) { mdd_t *tmpCofactor, *tmpAbstract; mdd_t *constIntermediate; if (ImgExistConstIntermediateVar(vector)) { constIntermediate = mdd_one(info->manager); for (i = 0; i < array_n(vector); i++) { comp = array_fetch(ImgComponent_t *, vector, i); if (comp->intermediate) { if (mdd_is_tautology(comp->func, 1)) { tmp = constIntermediate; constIntermediate = mdd_and(tmp, comp->var, 1, 1); mdd_free(tmp); } else if (mdd_is_tautology(comp->func, 0)) { tmp = constIntermediate; constIntermediate = mdd_and(tmp, comp->var, 1, 0); mdd_free(tmp); } } } if (relationArray) { cofactoredVector = ImgComposeConstIntermediateVars(info, vector, constIntermediate, &tmpCofactor, &tmpAbstract, NIL(mdd_t *), &newImage); if (!bdd_is_tautology(tmpCofactor, 1)) { tmp = cofactor; cofactor = mdd_and(tmp, tmpCofactor, 1, 1); mdd_free(tmp); } mdd_free(tmpCofactor); if (!bdd_is_tautology(tmpAbstract, 1)) { tmp = abstract; abstract = mdd_and(tmp, tmpAbstract, 1, 1); mdd_free(tmp); } mdd_free(tmpAbstract); } else { cofactoredVector = ImgComposeConstIntermediateVars(info, vector, constIntermediate, NIL(mdd_t *), NIL(mdd_t *), NIL(mdd_t *), &newImage); } mdd_free(constIntermediate); } else cofactoredVector = vector; } else cofactoredVector = vector; /* Simplify image -- canonicalize the image first */ n = 0; equivTable = st_init_table(st_ptrcmp, st_ptrhash); tmpVector = array_alloc(ImgComponent_t *, 0); for (i = 0; i < array_n(cofactoredVector); i++) { comp = array_fetch(ImgComponent_t *, cofactoredVector, i); if (comp->intermediate) { comp1 = ImgComponentCopy(info, comp); array_insert_last(ImgComponent_t *, tmpVector, comp1); n++; continue; } id = (int)bdd_top_var_id(comp->var); if (!imgComp->support[id]) { if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } continue; } if (mdd_is_tautology(comp->func, 1)) { changed = 1; simple = bdd_cofactor(newImage, comp->var); mdd_free(newImage); newImage = simple; if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } else if (mdd_is_tautology(comp->func, 0)) { changed = 1; tmp = mdd_not(comp->var); simple = bdd_cofactor(newImage, tmp); mdd_free(tmp); mdd_free(newImage); newImage = simple; if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } else { ptr = (int *)bdd_pointer(comp->func); regularPtr = (int *)((unsigned long)ptr & ~01); if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) { changed = 1; comp1 = array_fetch(ImgComponent_t *, tmpVector, pos); if (mdd_equal(comp->func, comp1->func)) { tmp = newImage; newImage = bdd_compose(tmp, comp->var, comp1->var); mdd_free(tmp); } else { tmp = newImage; var = mdd_not(comp1->var); newImage = bdd_compose(tmp, comp->var, var); mdd_free(tmp); mdd_free(var); } if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } else { comp1 = ImgComponentCopy(info, comp); array_insert_last(ImgComponent_t *, tmpVector, comp1); st_insert(equivTable, (char *)regularPtr, (char *)(long)n); n++; } } } st_free_table(equivTable); if (cofactoredVector && cofactoredVector != vector) ImgVectorFree(cofactoredVector); if (changed) { /* Now Simplify delta by deleting the non-affecting components */ *newVector = array_alloc(ImgComponent_t *, 0); imgComp->func = NIL(mdd_t); ImgComponentFree(imgComp); imgComp = ImgComponentAlloc(info); imgComp->func = newImage; ImgSupportClear(info, imgComp->support); ImgComponentGetSupport(imgComp); for (i = 0; i < array_n(tmpVector); i++) { comp = array_fetch(ImgComponent_t *, tmpVector, i); id = (int)bdd_top_var_id(comp->var); if (imgComp->support[id] || comp->intermediate) array_insert_last(ImgComponent_t *, *newVector, comp); else { if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } ImgComponentFree(comp); } } array_free(tmpVector); } else *newVector = tmpVector; imgComp->func = NIL(mdd_t); ImgComponentFree(imgComp); if (newRelationArray) *newRelationArray = relationArray; if (cofactor) { if (cofactorCube) *cofactorCube = cofactor; else { if (!bdd_is_tautology(cofactor, 1)) { tmpRelationArray = *newRelationArray; *newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray, cofactor); if (tmpRelationArray != relationArray) mdd_array_free(tmpRelationArray); } mdd_free(cofactor); } } if (abstract) { if (abstractCube) *abstractCube = abstract; else { if (bdd_is_tautology(abstract, 1)) mdd_free(abstract); else { tmpRelationArray = *newRelationArray; *newRelationArray = ImgGetAbstractedRelationArray(info->manager, tmpRelationArray, abstract); mdd_free(abstract); if (tmpRelationArray != relationArray) mdd_array_free(tmpRelationArray); } } } assert(CheckPreImageVector(info, *newVector, newImage)); return(newImage); } /**Function******************************************************************** Synopsis [Makes transition relation canonical for preimage.] Description [Makes transition relation canonical for preimage. Quantifies out the next state variables that do not occur in the image, and when a vector exists, delete the components which do not appear in the image. If a component is constant, simplify the image with the constant value and delete the corresponding component from delta Side effect on delta. Return new image.] SideEffects [] ******************************************************************************/ static bdd_t * PreImageMakeRelationCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray) { array_t *tmpVector, *cofactoredVector; bdd_t *simple, *tmp, *newImage; ImgComponent_t *comp, *comp1, *imgComp; int i, j, id; mdd_t *cofactor, *abstract, *var, *nsVar; array_t *tmpRelationArray; int changed = 0; mdd_t *yVarsCube, *rangeCube, *relation, *tmp2; array_t *supportIds; imgComp = ImgComponentAlloc(info); imgComp->func = image; ImgComponentGetSupport(imgComp); if (vector) { newImage = mdd_dup(image); cofactor = mdd_one(info->manager); abstract = mdd_one(info->manager); if (info->nIntermediateVars) { mdd_t *tmpCofactor, *tmpAbstract; mdd_t *constIntermediate; if (ImgExistConstIntermediateVar(vector)) { constIntermediate = mdd_one(info->manager); for (i = 0; i < array_n(vector); i++) { comp = array_fetch(ImgComponent_t *, vector, i); if (comp->intermediate) { if (mdd_is_tautology(comp->func, 1)) { tmp = constIntermediate; constIntermediate = mdd_and(tmp, comp->var, 1, 1); mdd_free(tmp); } else if (mdd_is_tautology(comp->func, 0)) { tmp = constIntermediate; constIntermediate = mdd_and(tmp, comp->var, 1, 0); mdd_free(tmp); } } } cofactoredVector = ImgComposeConstIntermediateVars(info, vector, constIntermediate, &tmpCofactor, &tmpAbstract, NIL(mdd_t *), &newImage); if (!bdd_is_tautology(tmpCofactor, 1)) { tmp = cofactor; cofactor = mdd_and(tmp, tmpCofactor, 1, 1); mdd_free(tmp); } mdd_free(tmpCofactor); if (!bdd_is_tautology(tmpAbstract, 1)) { tmp = abstract; abstract = mdd_and(tmp, tmpAbstract, 1, 1); mdd_free(tmp); } mdd_free(tmpAbstract); mdd_free(constIntermediate); } else cofactoredVector = vector; } else cofactoredVector = vector; /* Simplify image -- canonicalize vector */ tmpVector = array_alloc(ImgComponent_t *, 0); for (i = 0; i < array_n(cofactoredVector); i++) { comp = array_fetch(ImgComponent_t *, cofactoredVector, i); if (comp->intermediate) { comp1 = ImgComponentCopy(info, comp); array_insert_last(ImgComponent_t *, tmpVector, comp1); continue; } id = (int)bdd_top_var_id(comp->var); if (!imgComp->support[id]) { if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } continue; } if (mdd_is_tautology(comp->func, 1)) { changed = 1; simple = bdd_cofactor(newImage, comp->var); mdd_free(newImage); newImage = simple; if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } else if (mdd_is_tautology(comp->func, 0)) { changed = 1; tmp = mdd_not(comp->var); simple = bdd_cofactor(newImage, tmp); mdd_free(tmp); mdd_free(newImage); newImage = simple; if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } else { comp1 = ImgComponentCopy(info, comp); array_insert_last(ImgComponent_t *, tmpVector, comp1); } } if (cofactoredVector && cofactoredVector != vector) ImgVectorFree(cofactoredVector); if (changed) { /* Now Simplify delta by deleting the non-affecting components */ *newVector = array_alloc(ImgComponent_t *, 0); imgComp->func = NIL(mdd_t); ImgComponentFree(imgComp); imgComp = ImgComponentAlloc(info); imgComp->func = newImage; ImgSupportClear(info, imgComp->support); ImgComponentGetSupport(imgComp); for (i = 0; i < array_n(tmpVector); i++) { comp = array_fetch(ImgComponent_t *, tmpVector, i); id = (int)bdd_top_var_id(comp->var); if (imgComp->support[id] || comp->intermediate) array_insert_last(ImgComponent_t *, *newVector, comp); else { if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } ImgComponentFree(comp); } } array_free(tmpVector); } else *newVector = tmpVector; } else { newImage = image; *newVector = vector; cofactor = NIL(mdd_t); abstract = NIL(mdd_t); } yVarsCube = mdd_one(info->manager); for (i = 0; i < info->nVars; i++) { if (imgComp->support[i]) { imgComp->support[i] = 0; if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) continue; if (info->intermediateVarsTable && st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { continue; } var = bdd_var_with_index(info->manager, i); nsVar = ImgSubstitute(var, info->functionData, Img_D2R_c); mdd_free(var); id = (int)bdd_top_var_id(nsVar); imgComp->support[id] = 1; tmp = yVarsCube; yVarsCube = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } if (vector) { for (i = 0; i < array_n(*newVector); i++) { comp = array_fetch(ImgComponent_t *, *newVector, i); nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); id = (int)bdd_top_var_id(nsVar); imgComp->support[id] = 2; mdd_free(nsVar); } } for (i = 0; i < array_n(relationArray); i++) { relation = array_fetch(mdd_t *, relationArray, i); supportIds = mdd_get_bdd_support_ids(info->manager, relation); for (j = 0; j < array_n(supportIds); j++) { id = array_fetch(int, supportIds, j); imgComp->support[id] = 2; } array_free(supportIds); } for (i = 0; i < info->nVars; i++) { if (imgComp->support[i] == 1) { nsVar = bdd_var_with_index(info->manager, i); var = ImgSubstitute(nsVar, info->functionData, Img_R2D_c); mdd_free(nsVar); tmp = newImage; newImage = bdd_smooth_with_cube(tmp, var); if (tmp != image) mdd_free(tmp); mdd_free(var); } } imgComp->func = NIL(mdd_t); ImgComponentFree(imgComp); if (bdd_get_package_name() == CUDD) rangeCube = info->functionData->rangeCube; else { rangeCube = mdd_one(info->manager); for (i = 0; i < array_n(info->functionData->rangeBddVars); i++) { var = array_fetch(mdd_t *, info->functionData->rangeBddVars, i); tmp = rangeCube; rangeCube = mdd_and(tmp, var, 1, 1); mdd_free(tmp); } } cofactor = NIL(mdd_t); if (abstract) { tmp2 = bdd_smooth_with_cube(rangeCube, yVarsCube); tmp = abstract; abstract = mdd_and(tmp, tmp2, 1, 1); mdd_free(tmp); mdd_free(tmp2); } else abstract = bdd_smooth_with_cube(rangeCube, yVarsCube); mdd_free(yVarsCube); if (rangeCube != info->functionData->rangeCube) mdd_free(rangeCube); *newRelationArray = relationArray; if (cofactor) { if (!bdd_is_tautology(cofactor, 1)) { tmpRelationArray = *newRelationArray; *newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray, cofactor); if (tmpRelationArray != relationArray) mdd_array_free(tmpRelationArray); } mdd_free(cofactor); } if (bdd_is_tautology(abstract, 1)) mdd_free(abstract); else { tmpRelationArray = *newRelationArray; *newRelationArray = ImgGetAbstractedRelationArray(info->manager, tmpRelationArray, abstract); mdd_free(abstract); if (tmpRelationArray != relationArray) mdd_array_free(tmpRelationArray); } return(newImage); } /**Function******************************************************************** Synopsis [Deletes a component in a vector.] Description [Deletes a component in a vector. Deletes index-th component out of delta and copy it into newDelta.] SideEffects [] ******************************************************************************/ static bdd_t * PreImageDeleteOneComponent(ImgTfmInfo_t *info, array_t *delta, int index, array_t **newDelta) { int i; ImgComponent_t *comp, *tmpComp; bdd_t *func, *newFunc; int preMinimize = info->option->preMinimize; assert(array_n(delta) > 0); comp = array_fetch(ImgComponent_t *, delta, index); func = mdd_dup(comp->func); *newDelta = array_alloc(ImgComponent_t *, 0); for (i = 0; i < array_n(delta); i++) { if (i != index) { comp = array_fetch(ImgComponent_t *, delta, i); tmpComp = ImgComponentCopy(info, comp); if (preMinimize) { newFunc = bdd_minimize(tmpComp->func, func); if (mdd_equal(newFunc, tmpComp->func)) mdd_free(newFunc); else { mdd_free(tmpComp->func); tmpComp->func = newFunc; ImgSupportClear(info, tmpComp->support); ImgComponentGetSupport(tmpComp); } } array_insert_last(ImgComponent_t *, (*newDelta), tmpComp); } } return(func); } /**Function******************************************************************** Synopsis [Chooses a splitting variable for preimage.] Description [Chooses a splitting variable for preimage.] SideEffects [] ******************************************************************************/ static int PreImageChooseSplitVar(ImgTfmInfo_t *info, array_t *delta, bdd_t *img, int splitMethod, int split) { ImgComponent_t *comp, *imgComp; int i, j, bestCost, newCost; int index, bestVar, bestComp; int nFuncs, nVars, bestOccur = 0; int *varOccur, *varCost; mdd_t *var, *varNot, *pcFunc, *ncFunc; int tieCount = 0; assert(array_n(delta) > 0); if (splitMethod == 0) { bestVar = -1; bestComp = -1; nFuncs = array_n(delta); nVars = info->nVars; varOccur = ALLOC(int, nVars); memset(varOccur, 0, sizeof(int) * nVars); varCost = NIL(int); for (i = 0; i < nFuncs; i++) { comp = array_fetch(ImgComponent_t *, delta, i); for (j = 0; j < nVars; j++) { if (comp->support[j]) varOccur[j]++; } } switch (split) { case 0: /* largest support */ for (i = 0; i < nVars; i++) { if (varOccur[i] == 0) continue; if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) continue; if (info->intermediateVarsTable && st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { continue; } if (bestVar == -1 || varOccur[i] > bestOccur) { bestVar = i; bestOccur = varOccur[i]; tieCount = 1; } else if (varOccur[i] == bestOccur) { tieCount++; if (info->option->tieBreakMode == 0 && bdd_get_level_from_id(info->manager, i) < bdd_get_level_from_id(info->manager, bestVar)) { bestVar = i; } } } if (info->option->tieBreakMode == 1 && tieCount > 1) { bestCost = IMG_TF_MAX_INT; for (i = bestVar; i < nVars; i++) { if (varOccur[i] != bestOccur) continue; if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) continue; if (info->intermediateVarsTable && st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { continue; } var = bdd_var_with_index(info->manager, i); newCost = 0; for (j = 0; j < array_n(delta); j++) { comp = array_fetch(ImgComponent_t *, delta, j); newCost += bdd_estimate_cofactor(comp->func, var, 1); newCost += bdd_estimate_cofactor(comp->func, var, 0); } mdd_free(var); if (newCost < bestCost) { bestVar = i; bestCost = newCost; } else if (newCost == bestCost) { if (bdd_get_level_from_id(info->manager, i) < bdd_get_level_from_id(info->manager, bestVar)) { bestVar = i; } } } } break; case 1: /* smallest support after splitting */ /* Find the variable which makes the smallest support after splitting */ bestCost = IMG_TF_MAX_INT; varCost = ALLOC(int, nVars); memset(varCost, 0, sizeof(int) * nVars); for (i = 0; i < nVars; i++) { if (varOccur[i] == 0) continue; if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) continue; if (info->intermediateVarsTable && st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { continue; } var = bdd_var_with_index(info->manager, i); varNot = mdd_not(var); for (j = 0; j < array_n(delta); j++) { comp = array_fetch(ImgComponent_t *, delta, j); pcFunc = bdd_cofactor(comp->func, var); varCost[i] += ImgCountBddSupports(pcFunc); mdd_free(pcFunc); ncFunc = bdd_cofactor(comp->func, varNot); varCost[i] += ImgCountBddSupports(ncFunc); mdd_free(ncFunc); } mdd_free(var); mdd_free(varNot); if (varCost[i] < bestCost) { bestCost = varCost[i]; bestVar = i; } else if (varCost[i] == bestCost) { if (varOccur[i] < varOccur[bestVar]) { bestVar = i; } else if (varOccur[i] == varOccur[bestVar]) { if (bdd_get_level_from_id(info->manager, i) < bdd_get_level_from_id(info->manager, bestVar)) { bestVar = i; } } } } break; case 2: /* smallest BDD size after splitting */ /* Find the variable which makes the smallest BDDs of all functions after splitting */ bestCost = IMG_TF_MAX_INT; varCost = ALLOC(int, nVars); memset(varCost, 0, sizeof(int) * nVars); for (i = 0; i < nVars; i++) { if (varOccur[i] == 0) continue; if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) continue; if (info->intermediateVarsTable && st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { continue; } var = bdd_var_with_index(info->manager, i); for (j = 0; j < array_n(delta); j++) { comp = array_fetch(ImgComponent_t *, delta, j); varCost[i] += bdd_estimate_cofactor(comp->func, var, 1); varCost[i] += bdd_estimate_cofactor(comp->func, var, 0); } mdd_free(var); if (varCost[i] < bestCost) { bestCost = varCost[i]; bestVar = i; } else if (varCost[i] == bestCost) { if (varOccur[i] < varOccur[bestVar]) { bestVar = i; } else if (varOccur[i] == varOccur[bestVar]) { if (bdd_get_level_from_id(info->manager, i) < bdd_get_level_from_id(info->manager, bestVar)) { bestVar = i; } } } } break; case 3: /* top variable */ default: for (i = 0; i < nVars; i++) { if (varOccur[i] == 0) continue; if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) continue; if (info->intermediateVarsTable && st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { continue; } if (bestVar == -1) bestVar = i; else if (bdd_get_level_from_id(info->manager, i) < bdd_get_level_from_id(info->manager, bestVar)) { bestVar = i; } } } FREE(varOccur); if (varCost) FREE(varCost); } else { bestComp = -1; bestVar = -1; switch (split) { case 0: /* smallest BDD size */ bestCost = IMG_TF_MAX_INT; imgComp = ImgComponentAlloc(info); imgComp->func = img; ImgComponentGetSupport(imgComp); for (i = 0; i < array_n(delta); i++) { comp = array_fetch(ImgComponent_t *, delta, i); if (comp->intermediate) continue; index = (int)bdd_top_var_id(comp->var); if (imgComp->support[index]) { newCost = bdd_size(comp->func); if (newCost < bestCost) { bestComp = i; bestCost = newCost; } } } imgComp->func = NIL(mdd_t); ImgComponentFree(imgComp); break; case 1: /* largest BDD size */ bestCost = 0; imgComp = ImgComponentAlloc(info); imgComp->func = img; ImgComponentGetSupport(imgComp); for (i = 0; i < array_n(delta); i++) { comp = array_fetch(ImgComponent_t *, delta, i); if (comp->intermediate) continue; index = (int)bdd_top_var_id(comp->var); if (imgComp->support[index]) { newCost = bdd_size(comp->func); if (newCost > bestCost) { bestComp = i; bestCost = newCost; } } } imgComp->func = NIL(mdd_t); ImgComponentFree(imgComp); break; case 2: /* top variable */ default: for (i = 0; i < array_n(delta); i++) { comp = array_fetch(ImgComponent_t *, delta, i); if (comp->intermediate) continue; index = (int)bdd_top_var_id(comp->var); if (bestComp == -1 || bdd_get_level_from_id(info->manager, index) < bdd_get_level_from_id(info->manager, bestVar)) { bestVar = index; bestComp = i; } } break; } assert(bestComp != -1); } if (splitMethod == 0) return(bestVar); else return(bestComp); } /**Function******************************************************************** Synopsis [Performs domain cofactoring on a vector and from set with respect to a variable.] Description [Performs domain cofactoring on a vector and from set with respect to a variable.] SideEffects [] ******************************************************************************/ static mdd_t * DomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *c, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube) { mdd_t *res, *tmp; ImgComponent_t *comp, *comp1; array_t *vector1; int i, index, n, pos; mdd_t *newFrom, *var, *nsVar; mdd_t *cofactor, *abstract, *constIntermediate; array_t *tmpRelationArray; st_table *equivTable; int *ptr, *regularPtr; int size; newFrom = mdd_dup(from); vector1 = array_alloc(ImgComponent_t *, 0); if (relationArray) { cofactor = mdd_one(info->manager); abstract = mdd_one(info->manager); } else { cofactor = NIL(mdd_t); abstract = NIL(mdd_t); } if (info->nIntermediateVars) { size = ImgVectorFunctionSize(vector); if (size == array_n(vector)) constIntermediate = NIL(mdd_t); else constIntermediate = mdd_one(info->manager); } else constIntermediate = NIL(mdd_t); n = 0; equivTable = st_init_table(st_ptrcmp, st_ptrhash); index = (int)bdd_top_var_id(c); for (i = 0; i < array_n(vector); i++) { comp = array_fetch(ImgComponent_t *, vector, i); if (comp->support[index]) res = bdd_cofactor(comp->func, c); else res = mdd_dup(comp->func); if (bdd_is_tautology(res, 1)) { if (comp->intermediate) { tmp = constIntermediate; constIntermediate = mdd_and(tmp, comp->var, 1, 1); mdd_free(tmp); mdd_free(res); continue; } tmp = newFrom; newFrom = bdd_cofactor(tmp, comp->var); mdd_free(tmp); mdd_free(res); if (relationArray) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } else if (bdd_is_tautology(res, 0)) { if (comp->intermediate) { tmp = constIntermediate; constIntermediate = mdd_and(tmp, comp->var, 1, 0); mdd_free(tmp); mdd_free(res); continue; } tmp = newFrom; var = mdd_not(comp->var); newFrom = bdd_cofactor(tmp, var); mdd_free(tmp); mdd_free(var); mdd_free(res); if (relationArray) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } else { if (comp->intermediate) { comp1 = ImgComponentAlloc(info); comp1->var = mdd_dup(comp->var); comp1->func = res; if (mdd_equal(res, comp->func)) ImgSupportCopy(info, comp1->support, comp->support); else ImgComponentGetSupport(comp1); comp1->intermediate = 1; array_insert_last(ImgComponent_t *, vector1, comp1); n++; continue; } ptr = (int *)bdd_pointer(res); regularPtr = (int *)((unsigned long)ptr & ~01); if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) { comp1 = array_fetch(ImgComponent_t *, vector1, pos); if (mdd_equal(res, comp1->func)) { tmp = newFrom; newFrom = bdd_compose(tmp, comp->var, comp1->var); mdd_free(tmp); } else { tmp = newFrom; var = mdd_not(comp1->var); newFrom = bdd_compose(tmp, comp->var, var); mdd_free(tmp); mdd_free(var); } mdd_free(res); if (abstract) { nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); tmp = abstract; abstract = mdd_and(tmp, nsVar, 1, 1); mdd_free(tmp); mdd_free(nsVar); } } else { comp1 = ImgComponentAlloc(info); comp1->var = mdd_dup(comp->var); comp1->func = res; if (mdd_equal(res, comp->func)) ImgSupportCopy(info, comp1->support, comp->support); else ImgComponentGetSupport(comp1); array_insert_last(ImgComponent_t *, vector1, comp1); st_insert(equivTable, (char *)regularPtr, (char *)(long)n); n++; } } } st_free_table(equivTable); if (constIntermediate) { if (!bdd_is_tautology(constIntermediate, 1)) { mdd_t *tmpCofactor, *tmpAbstract; if (relationArray) { vector1 = ImgComposeConstIntermediateVars(info, vector1, constIntermediate, &tmpCofactor, &tmpAbstract, NIL(mdd_t *), &newFrom); if (!bdd_is_tautology(tmpCofactor, 1)) { tmp = cofactor; cofactor = mdd_and(tmp, tmpCofactor, 1, 1); mdd_free(tmp); } mdd_free(tmpCofactor); if (!bdd_is_tautology(tmpAbstract, 1)) { tmp = abstract; abstract = mdd_and(tmp, tmpAbstract, 1, 1); mdd_free(tmp); } mdd_free(tmpAbstract); tmp = cofactor; cofactor = mdd_and(tmp, constIntermediate, 1, 1); mdd_free(tmp); } else { vector1 = ImgComposeConstIntermediateVars(info, vector1, constIntermediate, NIL(mdd_t *), NIL(mdd_t *), NIL(mdd_t *), &newFrom); } } mdd_free(constIntermediate); } *newVector = vector1; if (relationArray) { if (newRelationArray) *newRelationArray = relationArray; if (cofactorCube && abstractCube) { if (cofactor) { if (bdd_is_tautology(cofactor, 1)) { mdd_free(cofactor); *cofactorCube = mdd_dup(c); } else { *cofactorCube = mdd_and(cofactor, c, 1, 1); mdd_free(cofactor); } } if (abstract) *abstractCube = abstract; } else { if (bdd_is_tautology(cofactor, 1)) { *newRelationArray = ImgGetCofactoredRelationArray(relationArray, c); mdd_free(cofactor); } else { tmp = cofactor; cofactor = mdd_and(tmp, c, 1, 1); mdd_free(tmp); *newRelationArray = ImgGetCofactoredRelationArray(relationArray, cofactor); mdd_free(cofactor); } if (bdd_is_tautology(abstract, 1)) mdd_free(abstract); else { tmpRelationArray = *newRelationArray; *newRelationArray = ImgGetAbstractedRelationArray(info->manager, tmpRelationArray, abstract); mdd_free(abstract); if (tmpRelationArray != relationArray) mdd_array_free(tmpRelationArray); } } } else *newRelationArray = NIL(array_t); return(newFrom); } /**Function******************************************************************** Synopsis [Checks sanity of a vector for preimage.] Description [Checks sanity of a vector for preimage.] SideEffects [] ******************************************************************************/ static int CheckPreImageVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *image) { ImgComponent_t *comp, *imgComp; int i, id, size, status; status = 1; if (info->nIntermediateVars) size = ImgVectorFunctionSize(vector); else size = array_n(vector); if (size != mdd_get_number_of_bdd_support(info->manager, image)) { fprintf(vis_stderr, "** tfm error: function vector length is different. (%d != %d)\n", size, mdd_get_number_of_bdd_support(info->manager, image)); status = 0; } imgComp = ImgComponentAlloc(info); imgComp->func = image; ImgComponentGetSupport(imgComp); for (i = 0; i < array_n(vector); i++) { comp = array_fetch(ImgComponent_t *, vector, i); id = (int)bdd_top_var_id(comp->var); if (comp->intermediate) imgComp->support[id] = 2; else if (imgComp->support[id] == 0) { fprintf(vis_stderr, "** tfm error: variable index[%d] is not in constraint\n", id); status = 0; } else imgComp->support[id] = 2; } for (i = 0; i < info->nVars; i++) { if (imgComp->support[i] == 1) { fprintf(vis_stderr, "** tfm error: variable index[%d] is not in function vector\n", i); status = 0; } } imgComp->func = NIL(mdd_t); ImgComponentFree(imgComp); return(status); }