#include "imgInt.h"
Include dependency graph for imgUtil.c:
Go to the source code of this file.
Functions | |
| static int | CheckImageValidity (mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray) |
| Img_OptimizeType | Img_ImageInfoObtainOptimizeType (Img_ImageInfo_t *imageInfo) |
| void | Img_ImageInfoSetUseOptimizedRelationFlag (Img_ImageInfo_t *imageInfo) |
| void | Img_ImageInfoResetUseOptimizedRelationFlag (Img_ImageInfo_t *imageInfo) |
| void | Img_ImageInfoResetLinearComputeRange (Img_ImageInfo_t *imageInfo) |
| void | Img_ImageInfoSetLinearComputeRange (Img_ImageInfo_t *imageInfo) |
| void | Img_Init (void) |
| void | Img_End (void) |
| Img_MethodType | Img_UserSpecifiedMethod (void) |
| Img_ImageInfo_t * | Img_ImageInfoInitialize (Img_ImageInfo_t *imageInfo, graph_t *mddNetwork, array_t *roots, array_t *domainVars, array_t *rangeVars, array_t *quantifyVars, mdd_t *domainCube, mdd_t *rangeCube, mdd_t *quantifyCube, Ntk_Network_t *network, Img_MethodType methodType, Img_DirectionType directionType, int FAFWFlag, mdd_t *Winning) |
| int | Img_IsQuantifyCubeSame (Img_ImageInfo_t *imageInfo, mdd_t *quantifyCube) |
| int | Img_IsQuantifyArraySame (Img_ImageInfo_t *imageInfo, array_t *quantifyArray) |
| void | Img_ImageInfoUpdateVariables (Img_ImageInfo_t *imageInfo, graph_t *mddNetwork, array_t *domainVars, array_t *quantifyVars, mdd_t *domainCube, mdd_t *quantifyCube) |
| void | Img_ImageAllowPartialImage (Img_ImageInfo_t *info, boolean value) |
| void | Img_ImagePrintPartialImageOptions (void) |
| boolean | Img_ImageWasPartial (Img_ImageInfo_t *info) |
| mdd_t * | Img_ImageInfoComputeImageWithDomainVars (Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
| mdd_t * | Img_ImageInfoComputeFwdWithDomainVars (Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet) |
| mdd_t * | Img_ImageInfoComputeFwd (Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
| mdd_t * | Img_ImageInfoComputePreImageWithDomainVars (Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
| mdd_t * | Img_ImageInfoComputeEXWithDomainVars (Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
| mdd_t * | Img_ImageInfoComputeBwdWithDomainVars (Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet) |
| mdd_t * | Img_ImageInfoComputeBwd (Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
| void | Img_ImageInfoFree (Img_ImageInfo_t *imageInfo) |
| void | Img_ImageInfoFreeFAFW (Img_ImageInfo_t *imageInfo) |
| char * | Img_ImageInfoObtainMethodTypeAsString (Img_ImageInfo_t *imageInfo) |
| Img_MethodType | Img_ImageInfoObtainMethodType (Img_ImageInfo_t *imageInfo) |
| void | Img_ImageInfoPrintMethodParams (Img_ImageInfo_t *imageInfo, FILE *fp) |
| void | Img_ResetTrMinimizedFlag (Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) |
| Img_MinimizeType | Img_ReadMinimizeMethod (void) |
| void | Img_MinimizeTransitionRelation (Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, boolean reorderIwls95Clusters) |
| mdd_t * | Img_MinimizeImage (mdd_t *image, mdd_t *constraint, Img_MinimizeType method, boolean underapprox) |
| mdd_t * | Img_AddDontCareToImage (mdd_t *image, mdd_t *constraint, Img_MinimizeType method) |
| mdd_t * | Img_MinimizeImageArray (mdd_t *image, array_t *constraintArray, Img_MinimizeType method, boolean underapprox) |
| void | Img_SetPrintMinimizeStatus (Img_ImageInfo_t *imageInfo, int status) |
| int | Img_ReadPrintMinimizeStatus (Img_ImageInfo_t *imageInfo) |
| void | Img_AbstractTransitionRelation (Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType) |
| void | Img_DupTransitionRelation (Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) |
| void | Img_RestoreTransitionRelation (Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) |
| int | Img_ApproximateTransitionRelation (Img_ImageInfo_t *imageInfo, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, Img_DirectionType directionType, mdd_t *bias) |
| mdd_t * | Img_ApproximateImage (mdd_manager *mgr, mdd_t *image, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, mdd_t *bias) |
| int | Img_IsPartitionedTransitionRelation (Img_ImageInfo_t *imageInfo) |
| void | Img_ResetNumberOfImageComputation (Img_DirectionType imgDir) |
| int | Img_GetNumberOfImageComputation (Img_DirectionType imgDir) |
| array_t * | Img_GetPartitionedTransitionRelation (Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) |
| void | Img_ReplaceIthPartitionedTransitionRelation (Img_ImageInfo_t *imageInfo, int i, mdd_t *relation, Img_DirectionType directionType) |
| void | Img_ReplacePartitionedTransitionRelation (Img_ImageInfo_t *imageInfo, array_t *relationArray, Img_DirectionType directionType) |
| mdd_t * | Img_ComposeIntermediateNodes (graph_t *partition, mdd_t *node, array_t *psVars, array_t *nsVars, array_t *inputVars) |
| void | Img_ImageConstrainAndClusterTransitionRelation (Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus) |
| Img_MinimizeType | Img_GuidedSearchReadUnderApproxMinimizeMethod (void) |
| Img_MinimizeType | Img_GuidedSearchReadOverApproxMinimizeMethod (void) |
| mdd_t * | Img_Substitute (Img_ImageInfo_t *imageInfo, mdd_t *f, Img_SubstituteDir dir) |
| array_t * | ImgMinimizeImageArrayWithCareSetArray (array_t *imageArray, array_t *careSetArray, Img_MinimizeType minimizeMethod, boolean underapprox, boolean printInfo, Img_DirectionType dir) |
| void | ImgMinimizeImageArrayWithCareSetArrayInSitu (array_t *imageArray, array_t *careSetArray, Img_MinimizeType minimizeMethod, boolean underapprox, boolean printInfo, Img_DirectionType dir) |
| mdd_t * | ImgSubstitute (mdd_t *f, ImgFunctionData_t *functionData, Img_SubstituteDir dir) |
| array_t * | ImgSubstituteArray (array_t *f_array, ImgFunctionData_t *functionData, Img_SubstituteDir dir) |
| void | ImgPrintPartialImageOptions (void) |
| ImgPartialImageOption_t * | ImgGetPartialImageOptions (void) |
| int | ImgArrayBddArrayCheckValidity (array_t *arrayBddArray) |
| int | ImgBddArrayCheckValidity (array_t *bddArray) |
| int | ImgBddCheckValidity (bdd_t *bdd) |
| void | ImgPrintVarIdTable (st_table *table) |
| int | ImgCheckToCareSetArrayChanged (array_t *toCareSetArray1, array_t *toCareSetArray2) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: imgUtil.c,v 1.74 2005/05/14 21:08:32 jinh Exp $" |
| static int | nImgComps = 0 |
| static int | nPreComps = 0 |
Function Documentation
| static int CheckImageValidity | ( | mdd_manager * | mddManager, |
| mdd_t * | image, | ||
| array_t * | domainVarMddIdArray, | ||
| array_t * | quantifyVarMddIdArray | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Checks the validity of image]
Description [In a properly formed image, there should not be any domain or quantify variables in its support. This function checks for that fact.]
SideEffects []
Definition at line 2533 of file imgUtil.c.
{
int i;
array_t *imageSupportArray = mdd_get_support(mddManager, image);
st_table *imageSupportTable = st_init_table(st_numcmp, st_numhash);
for (i=0; i<array_n(imageSupportArray); i++){
long mddId = (long) array_fetch(int, imageSupportArray, i);
(void) st_insert(imageSupportTable, (char *) mddId, NIL(char));
}
for (i=0; i<array_n(domainVarMddIdArray); i++){
int domainVarId;
domainVarId = array_fetch(int, domainVarMddIdArray, i);
assert(st_is_member(imageSupportTable, (char *)(long)domainVarId) == 0);
}
for (i=0; i<array_n(quantifyVarMddIdArray); i++){
int quantifyVarId;
quantifyVarId = array_fetch(int, quantifyVarMddIdArray, i);
assert(st_is_member(imageSupportTable, (char *)(long)quantifyVarId) == 0);
}
st_free_table(imageSupportTable);
array_free(imageSupportArray);
return 1;
}
Here is the caller graph for this function:
| void Img_AbstractTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| array_t * | abstractVars, | ||
| mdd_t * | abstractCube, | ||
| Img_DirectionType | directionType | ||
| ) |
Function********************************************************************
Synopsis [Abstracts out given variables from transition relation.]
Description [Abstracts out given variables from transition relation. abstractVars should be an array of bdd variables.]
SideEffects []
Definition at line 1420 of file imgUtil.c.
{
switch (imageInfo->methodType) {
case Img_Monolithic_c:
ImgAbstractTransitionRelationMono(imageInfo, abstractVars,
abstractCube, imageInfo->printMinimizeStatus);
break;
case Img_Tfm_c:
case Img_Hybrid_c:
ImgAbstractTransitionFunction(imageInfo, abstractVars,
abstractCube, directionType,
imageInfo->printMinimizeStatus);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
ImgAbstractTransitionRelationIwls95(imageInfo, abstractVars,
abstractCube, directionType,
imageInfo->printMinimizeStatus);
break;
default:
fail("** img error : Unexpected type when abstracting transition relation");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Img_AddDontCareToImage | ( | mdd_t * | image, |
| mdd_t * | constraint, | ||
| Img_MinimizeType | method | ||
| ) |
Function********************************************************************
Synopsis [Adds a dont care set to the given image.]
Description [Adds a dont care set to the given image.]
SideEffects []
Definition at line 1327 of file imgUtil.c.
{
return(Img_MinimizeImage(image, constraint, Img_Restrict_c, method));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Img_ApproximateImage | ( | mdd_manager * | mgr, |
| mdd_t * | image, | ||
| bdd_approx_dir_t | approxDir, | ||
| bdd_approx_type_t | approxMethod, | ||
| int | approxThreshold, | ||
| double | approxQuality, | ||
| double | approxQualityBias, | ||
| mdd_t * | bias | ||
| ) |
Function********************************************************************
Synopsis [Approximate image.]
Description [Approximate image.]
SideEffects []
Definition at line 1593 of file imgUtil.c.
{
double quality;
double qualityBias;
int nvars = mdd_get_number_of_bdd_support(mgr, image);
mdd_t *approxImage;
if (approxQuality != 0.0)
quality = approxQuality;
else
quality = 1.0; /* default */
/* based on approximation method specified, compute subset or superset */
switch (approxMethod) {
case BDD_APPROX_HB:
approxImage = bdd_approx_hb(image, approxDir, nvars, approxThreshold);
break;
case BDD_APPROX_SP:
approxImage = bdd_approx_sp(image, approxDir, nvars, approxThreshold, 0);
break;
case BDD_APPROX_UA:
approxImage = bdd_approx_ua(image, approxDir, nvars, approxThreshold, 0,
quality);
break;
case BDD_APPROX_RUA:
approxImage = bdd_approx_remap_ua(image, approxDir, nvars, approxThreshold,
quality);
break;
case BDD_APPROX_BIASED_RUA:
if (approxQualityBias != 0.0)
qualityBias = approxQualityBias;
else
qualityBias = 0.5; /* default */
approxImage = bdd_approx_biased_rua(image, approxDir, bias, nvars,
approxThreshold, quality, qualityBias);
break;
case BDD_APPROX_COMP:
approxImage = bdd_approx_compress(image, approxDir, nvars, approxThreshold);
break;
default:
assert(0);
approxImage = NIL(mdd_t);
break;
}
return(approxImage);
}
Here is the caller graph for this function:
| int Img_ApproximateTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| bdd_approx_dir_t | approxDir, | ||
| bdd_approx_type_t | approxMethod, | ||
| int | approxThreshold, | ||
| double | approxQuality, | ||
| double | approxQualityBias, | ||
| Img_DirectionType | directionType, | ||
| mdd_t * | bias | ||
| ) |
Function********************************************************************
Synopsis [Approximate transition relation.]
Description [Approximate transition relation.]
SideEffects []
Definition at line 1522 of file imgUtil.c.
{
int unchanged = 0;
mdd_manager *mgr =
Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
switch (imageInfo->methodType) {
case Img_Monolithic_c:
unchanged = ImgApproximateTransitionRelationMono(mgr, imageInfo,
approxDir, approxMethod,
approxThreshold,
approxQuality,
approxQualityBias, bias);
break;
case Img_Tfm_c:
case Img_Hybrid_c:
unchanged = ImgApproximateTransitionFunction(mgr,
imageInfo->methodData,
approxDir, approxMethod,
approxThreshold,
approxQuality,
approxQualityBias,
directionType, bias);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
if (directionType == Img_Forward_c || directionType == Img_Both_c) {
unchanged = ImgApproximateTransitionRelationIwls95(mgr,
imageInfo->methodData,
approxDir, approxMethod,
approxThreshold,
approxQuality,
approxQualityBias,
Img_Forward_c, bias);
}
if (directionType == Img_Backward_c || directionType == Img_Both_c) {
unchanged += ImgApproximateTransitionRelationIwls95(mgr,
imageInfo->methodData,
approxDir, approxMethod,
approxThreshold,
approxQuality,
approxQualityBias,
Img_Backward_c, bias);
}
break;
default:
fail(
"** img error : Unexpected type when approximating transition relation");
}
return(unchanged);
}
Here is the call graph for this function:
| mdd_t* Img_ComposeIntermediateNodes | ( | graph_t * | partition, |
| mdd_t * | node, | ||
| array_t * | psVars, | ||
| array_t * | nsVars, | ||
| array_t * | inputVars | ||
| ) |
Function********************************************************************
Synopsis [Replace partitioned transition relation.]
Description [Replace partitioned transition relation.]
SideEffects []
Definition at line 1826 of file imgUtil.c.
{
mdd_manager *mgr = Part_PartitionReadMddManager(partition);
array_t *supportList;
st_table *supportTable = st_init_table(st_numcmp, st_numhash);
int i, j;
int existIntermediateVars;
int mddId;
vertex_t *vertex;
array_t *varBddFunctionArray, *varArray;
mdd_t *var, *func, *tmpMdd;
mdd_t *composedNode;
Mvf_Function_t *mvf;
if (psVars) {
for (i = 0; i < array_n(psVars); i++) {
mddId = array_fetch(int, psVars, i);
st_insert(supportTable, (char *)(long)mddId, NULL);
}
}
if (nsVars) {
for (i = 0; i < array_n(nsVars); i++) {
mddId = array_fetch(int, nsVars, i);
st_insert(supportTable, (char *)(long)mddId, NULL);
}
}
if (inputVars) {
for (i = 0; i < array_n(inputVars); i++) {
mddId = array_fetch(int, inputVars, i);
st_insert(supportTable, (char *)(long)mddId, NULL);
}
}
composedNode = mdd_dup(node);
existIntermediateVars = 1;
while (existIntermediateVars) {
existIntermediateVars = 0;
supportList = mdd_get_support(mgr, composedNode);
for (i = 0; i < array_n(supportList); i++) {
mddId = array_fetch(int, supportList, i);
if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
vertex = Part_PartitionFindVertexByMddId(partition, mddId);
mvf = Part_VertexReadFunction(vertex);
varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mgr, mddId, mvf);
varArray = mdd_id_to_bdd_array(mgr, mddId);
assert(array_n(varBddFunctionArray) == array_n(varArray));
for (j = 0; j < array_n(varBddFunctionArray); j++) {
var = array_fetch(mdd_t *, varArray, j);
func = array_fetch(mdd_t *, varBddFunctionArray, j);
tmpMdd = composedNode;
composedNode = bdd_compose(composedNode, var, func);
mdd_free(tmpMdd);
mdd_free(var);
mdd_free(func);
}
array_free(varBddFunctionArray);
array_free(varArray);
existIntermediateVars = 1;
}
}
array_free(supportList);
}
st_free_table(supportTable);
return(composedNode);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_DupTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| Img_DirectionType | directionType | ||
| ) |
Function********************************************************************
Synopsis [Duplicates the transition relation for backup.]
Description [Duplicates the transition relation for backup. Copies transition relation as well as quantification schedule for temporary use.]
SideEffects []
Definition at line 1458 of file imgUtil.c.
{
switch (imageInfo->methodType) {
case Img_Monolithic_c:
ImgDuplicateTransitionRelationMono(imageInfo);
break;
case Img_Tfm_c:
case Img_Hybrid_c:
ImgDuplicateTransitionFunction(imageInfo, directionType);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
ImgDuplicateTransitionRelationIwls95(imageInfo, directionType);
break;
default:
fail("** img error: Unexpected type when duplicating transition relation");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_End | ( | void | ) |
| int Img_GetNumberOfImageComputation | ( | Img_DirectionType | imgDir | ) |
Function********************************************************************
Synopsis [Returns number of image/preimage computation.]
Description [Returns number of image/preimage computation.]
SideEffects []
Definition at line 1701 of file imgUtil.c.
{
if (imgDir == Img_Forward_c)
return(nImgComps);
else if (imgDir == Img_Backward_c)
return(nPreComps);
else
return(nImgComps + nPreComps);
}
Here is the caller graph for this function:
| array_t* Img_GetPartitionedTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| Img_DirectionType | directionType | ||
| ) |
Function********************************************************************
Synopsis [Returns current partitioned transition relation.]
Description [Returns current partitioned transition relation.]
SideEffects []
Definition at line 1722 of file imgUtil.c.
{
array_t *relationArray;
switch (imageInfo->methodType) {
case Img_Monolithic_c:
relationArray = (array_t *)imageInfo->methodData;
break;
case Img_Tfm_c:
case Img_Hybrid_c:
relationArray = ImgGetTransitionFunction(imageInfo->methodData,
directionType);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
relationArray = ImgGetTransitionRelationIwls95(imageInfo->methodData,
directionType);
break;
default:
fail("** img error: Unexpected image method type.\n");
}
return(relationArray);
}
Here is the call graph for this function:
| Img_MinimizeType Img_GuidedSearchReadOverApproxMinimizeMethod | ( | void | ) |
Function********************************************************************
Synopsis [Returns the guided search minimize method of overapproximating the transition relation.]
Description [Returns the guided search minimize method of overapproximating the transition relation. Default is OrNot.]
SideEffects []
Definition at line 2016 of file imgUtil.c.
{
char *flagValue;
Img_MinimizeType minimizeMethod = Img_OrNot_c;
flagValue = Cmd_FlagReadByName("guided_search_overapprox_minimize_method");
if (flagValue != NIL(char)) {
if (strcmp(flagValue, "ornot") == 0) {
minimizeMethod = Img_OrNot_c;
} else if (strcmp(flagValue, "squeeze") == 0) {
minimizeMethod = Img_Squeeze_c;
} else {
fprintf(vis_stderr,
"** img error : invalid value %s for guided_search_overapprox_minimize_method. ***\n",
flagValue);
fprintf(vis_stderr,
"** img error : Reverting to default method : OrNot\n");
}
}
return(minimizeMethod);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Img_MinimizeType Img_GuidedSearchReadUnderApproxMinimizeMethod | ( | void | ) |
Function********************************************************************
Synopsis [Returns the guided search minimize method of underapproximating the transition relation.]
Description [Returns the guided search minimize method of underapproximating the transition relation. Default is And.]
SideEffects []
Definition at line 1982 of file imgUtil.c.
{
char *flagValue;
Img_MinimizeType minimizeMethod = Img_And_c;
flagValue = Cmd_FlagReadByName("guided_search_underapprox_minimize_method");
if (flagValue != NIL(char)) {
if (strcmp(flagValue, "constrain") == 0) {
minimizeMethod = Img_Constrain_c;
} else if (strcmp(flagValue, "and") == 0) {
minimizeMethod = Img_And_c;
} else {
fprintf(vis_stderr,
"** img error : invalid value %s for guided_search_underapprox_minimize_method. ***\n",
flagValue);
fprintf(vis_stderr,
"** img error : Reverting to default minimize method : And\n");
}
}
return(minimizeMethod);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_ImageAllowPartialImage | ( | Img_ImageInfo_t * | info, |
| boolean | value | ||
| ) |
Function********************************************************************
Synopsis [Sets the flag to allow the next image computation to return a subset of the actual image.]
Description [Sets the flag to allow the next image computation to return a subset of the actual image. Default is to not allow partial image computations. This flag is reset at the end of every image/preimage computation i.e., has to be specified before every image/preimage computation if partial image is desired. ]
SideEffects [Flag is reset at the end of every image/preimage computation.]
SeeAlso [Img_ImageWasPartialImage]
Definition at line 498 of file imgUtil.c.
{
if (info->methodType == Img_Iwls95_c || info->methodType == Img_Mlp_c) {
ImgImageAllowPartialImageIwls95(info->methodData, value);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_ImageConstrainAndClusterTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| Img_DirectionType | direction, | ||
| mdd_t * | constrain, | ||
| Img_MinimizeType | minimizeMethod, | ||
| boolean | underApprox, | ||
| boolean | cleanUp, | ||
| boolean | forceReorder, | ||
| int | printStatus | ||
| ) |
Function********************************************************************
Synopsis [Constrains/adds dont-cares to the bit relations with the given constraint and creates a new transtion relation.]
Description [Constrains/adds dont-cares to the bit relations with the given constraint and creates a new transition relation in the direction indicated. This procedure will incur the cost of creating the bit relations if they dont already exist. An over/under approximation of the transition relation may be created according to the underApprox flag. The flag is TRUE for underapproximations and FALSE for over approximation. An underapproximation of the transition relation will be in the interval [T.C, T] and an overapproximation of the transition relation will be in the interval [T, T+ C']. THe method used in minimization is set in Img_GuidedSearchReadUnderApproxMinimizeMethod and Img_GuidedSearchReadOverApproxMinimizeMethod. The cleanup flag cleans up the data (e.g., bit relations) stored for applying constraints repeatedly. ]
SideEffects [Current transition relation and quantification schedule are freed. Bit relations are freed if indicated by the cleanUp flag.]
SeeAlso [Img_GuidedSearchReadUnderApproxMinimizeMethod Img_GuidedSearchReadOverApproxMinimizeMethod]
Definition at line 1923 of file imgUtil.c.
{
switch (imageInfo->methodType) {
case Img_Monolithic_c:
ImgImageConstrainAndClusterTransitionRelationMono(imageInfo,
constrain,
minimizeMethod,
underApprox,
cleanUp,
forceReorder,
printStatus);
break;
case Img_Tfm_c:
case Img_Hybrid_c:
ImgImageConstrainAndClusterTransitionRelationTfm(imageInfo,
direction,
constrain,
minimizeMethod,
underApprox,
cleanUp,
forceReorder,
printStatus);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(imageInfo,
direction,
constrain,
minimizeMethod,
underApprox,
cleanUp,
forceReorder,
printStatus);
break;
default:
fail("** img error: Unexpected image method type.\n");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Img_ImageInfoComputeBwd | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | fromLowerBound, | ||
| mdd_t * | fromUpperBound, | ||
| array_t * | toCareSetArray | ||
| ) |
Function********************************************************************
Synopsis [Computes the backward image of a set.]
Description [Computes the backward image of a set, under the function vector in imageInfo, using the image computation method specified in imageInfo. The set for which the backward image is computed is some set containing fromLowerBound and contained in fromUpperBound. The exact set used is chosen to simplify the computation. ToCareSet specifies those backward image points of interest; any points not in this set may or may not belong to the returned set. The MDDs fromLowerBound and fromUpperBound are defined over the range variables. The MDD toCareSet and the returned MDD are defined over the domain variables. If fromLowerBound is zero, then zero will be returned.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoFree Img_ImageInfoComputeBwdWithDomainVars]
Definition at line 823 of file imgUtil.c.
{
mdd_t *image;
if (mdd_is_tautology(fromLowerBound, 0)){
mdd_manager *mddManager =
Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
return (mdd_zero(mddManager));
}
image = ((*imageInfo->imageComputeBwdProc) (&(imageInfo->functionData),
imageInfo,
fromLowerBound,
fromUpperBound,
toCareSetArray));
nPreComps++;
#ifndef NDEBUG
assert(CheckImageValidity(
Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork),
image,
imageInfo->functionData.rangeVars,
imageInfo->functionData.quantifyVars));
#endif
return image;
}
Here is the call graph for this function:
| mdd_t* Img_ImageInfoComputeBwdWithDomainVars | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | fromLowerBound, | ||
| mdd_t * | fromUpperBound, | ||
| mdd_t * | toCareSet | ||
| ) |
Function********************************************************************
Synopsis [Computes the backward image of a set expressed in terms of domain variables.]
Description [Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care set, as opposed to ComputeBwd, which takes a care-set array.]
SideEffects []
SeeAlso [Img_ImageInfoComputeBwd]
Definition at line 784 of file imgUtil.c.
{
array_t *toCareSetArray;
mdd_t *preImage;
toCareSetArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
preImage = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
fromLowerBound, fromUpperBound, toCareSetArray);
array_free(toCareSetArray);
return(preImage);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Img_ImageInfoComputeEXWithDomainVars | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | fromLowerBound, | ||
| mdd_t * | fromUpperBound, | ||
| array_t * | toCareSetArray | ||
| ) |
Function********************************************************************
Synopsis [Computes the backward image of a set expressed in terms of domain variables.]
Description [Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSetArray are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care-set array, as opposed to Img_ImageInfoComputeBwdWithDomainVars, which takes a care set.]
SideEffects []
SeeAlso [Img_ImageInfoComputeBwd]
Definition at line 747 of file imgUtil.c.
{
mdd_t *image;
if (mdd_is_tautology(fromLowerBound, 0)){
mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
return (mdd_zero(mddManager));
}
image = ((*imageInfo->imageComputeBwdWithDomainVarsProc)
(&(imageInfo->functionData), imageInfo,
fromLowerBound, fromUpperBound, toCareSetArray));
nPreComps++;
return image;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Img_ImageInfoComputeFwd | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | fromLowerBound, | ||
| mdd_t * | fromUpperBound, | ||
| array_t * | toCareSetArray | ||
| ) |
Function********************************************************************
Synopsis [Computes the forward image of a set.]
Description [Computes the forward image of a set, under the function vector in imageInfo, using the image computation method specified in imageInfo. The set for which the forward image is computed is some set containing fromLowerBound and contained in fromUpperBound. The exact set used is chosen to simplify the computation. ToCareSet specifies those forward image points of interest; any points not in this set may or may not belong to the returned set. The MDDs fromLowerBound and fromUpperBound are defined over the domain variables. The MDD toCareSet and the returned MDD are defined over the range variables. If fromLowerBound is zero, then zero will be returned. (Takes care states as an array.)]
SideEffects []
SeeAlso [Img_ImageInfoInitialize Img_ImageInfoComputeBwd Img_ImageInfoFree Img_ImageInfoComputeFwdWithDomainVars]
Definition at line 659 of file imgUtil.c.
{
mdd_t *image;
if (mdd_is_tautology(fromLowerBound, 0)){
mdd_manager *mddManager = Part_PartitionReadMddManager(
imageInfo->functionData.mddNetwork);
return (mdd_zero(mddManager));
}
image = ((*imageInfo->imageComputeFwdProc) (&(imageInfo->functionData),
imageInfo,
fromLowerBound,
fromUpperBound,
toCareSetArray));
nImgComps++;
#ifndef NDEBUG
assert(CheckImageValidity(
Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork),
image,
imageInfo->functionData.domainVars,
imageInfo->functionData.quantifyVars));
#endif
return image;
}
Here is the call graph for this function:
| mdd_t* Img_ImageInfoComputeFwdWithDomainVars | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | fromLowerBound, | ||
| mdd_t * | fromUpperBound, | ||
| mdd_t * | toCareSet | ||
| ) |
Function********************************************************************
Synopsis [Computes the forward image of a set and expresses it in terms of domain variables.]
Description [Computes the forward image of a set and expresses it in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeFwd for more information. (Takes care states as a set.)]
SideEffects []
SeeAlso [Img_ImageInfoComputeFwd]
Definition at line 619 of file imgUtil.c.
{
array_t *toCareSetArray;
mdd_t *image;
toCareSetArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
image = Img_ImageInfoComputeImageWithDomainVars(imageInfo, fromLowerBound,
fromUpperBound, toCareSetArray);
array_free(toCareSetArray);
return(image);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Img_ImageInfoComputeImageWithDomainVars | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | fromLowerBound, | ||
| mdd_t * | fromUpperBound, | ||
| array_t * | toCareSetArray | ||
| ) |
Function********************************************************************
Synopsis [Computes the forward image of a set and expresses it in terms of domain variables.]
Description [Computes the forward image of a set and expresses it in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeFwd for more information. (Takes care set as an array.)]
SideEffects []
SeeAlso [Img_ImageInfoComputeFwd]
Definition at line 563 of file imgUtil.c.
{
mdd_t *image;
mdd_manager *mddManager;
long peakMem;
int peakLiveNode;
if (mdd_is_tautology(fromLowerBound, 0)){
mddManager = Part_PartitionReadMddManager(
imageInfo->functionData.mddNetwork);
return (mdd_zero(mddManager));
}
image = ((*imageInfo->imageComputeFwdWithDomainVarsProc)
(&(imageInfo->functionData), imageInfo,
fromLowerBound, fromUpperBound, toCareSetArray));
nImgComps++;
if (imageInfo->verbosity >= 2 && bdd_get_package_name() == CUDD) {
mddManager = Part_PartitionReadMddManager(
imageInfo->functionData.mddNetwork);
peakMem = bdd_read_peak_memory(mddManager);
peakLiveNode = bdd_read_peak_live_node(mddManager);
fprintf(vis_stdout, "** img info: current peak memory = %ld\n", peakMem);
fprintf(vis_stdout, "** img info: current peak live nodes = %d\n",
peakLiveNode);
}
#ifndef NDEBUG
assert(CheckImageValidity(
Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork),
image,
imageInfo->functionData.rangeVars,
imageInfo->functionData.quantifyVars));
#endif
return(image);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Img_ImageInfoComputePreImageWithDomainVars | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | fromLowerBound, | ||
| mdd_t * | fromUpperBound, | ||
| array_t * | toCareSetArray | ||
| ) |
Function********************************************************************
Synopsis [Computes the backward image of a set expressed in terms of domain variables.]
Description [Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSetArray are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care-set array, as opposed to Img_ImageInfoComputeBwdWithDomainVars, which takes a care set.]
SideEffects []
SeeAlso [Img_ImageInfoComputeBwd]
Definition at line 705 of file imgUtil.c.
{
mdd_t *image;
if (mdd_is_tautology(fromLowerBound, 0)){
mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
return (mdd_zero(mddManager));
}
image = ((*imageInfo->imageComputeBwdWithDomainVarsProc)
(&(imageInfo->functionData), imageInfo,
fromLowerBound, fromUpperBound, toCareSetArray));
nPreComps++;
#ifndef NDEBUG
assert(CheckImageValidity(
Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork),
image,
imageInfo->functionData.rangeVars,
imageInfo->functionData.quantifyVars));
#endif
return image;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_ImageInfoFree | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [Frees the memory associated with imageInfo.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd]
Definition at line 862 of file imgUtil.c.
{
(*imageInfo->imageFreeProc) (imageInfo->methodData);
if (imageInfo->functionData.domainBddVars)
mdd_array_free(imageInfo->functionData.domainBddVars);
if (imageInfo->functionData.rangeBddVars)
mdd_array_free(imageInfo->functionData.rangeBddVars);
if (imageInfo->functionData.quantifyBddVars)
mdd_array_free(imageInfo->functionData.quantifyBddVars);
if (imageInfo->functionData.permutD2R)
FREE(imageInfo->functionData.permutD2R);
if (imageInfo->functionData.permutR2D)
FREE(imageInfo->functionData.permutR2D);
if (imageInfo->savedRelation)
mdd_array_free((array_t *) imageInfo->savedRelation);
FREE(imageInfo);
}
Here is the caller graph for this function:
| void Img_ImageInfoFreeFAFW | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [Frees the memory associated with imageInfo.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd]
Definition at line 891 of file imgUtil.c.
{
if (imageInfo->functionData.quantifyVars)
mdd_array_free(imageInfo->functionData.quantifyVars);
if (imageInfo->functionData.quantifyCube)
mdd_free(imageInfo->functionData.quantifyCube);
}
Here is the caller graph for this function:
| Img_ImageInfo_t* Img_ImageInfoInitialize | ( | Img_ImageInfo_t * | imageInfo, |
| graph_t * | mddNetwork, | ||
| array_t * | roots, | ||
| array_t * | domainVars, | ||
| array_t * | rangeVars, | ||
| array_t * | quantifyVars, | ||
| mdd_t * | domainCube, | ||
| mdd_t * | rangeCube, | ||
| mdd_t * | quantifyCube, | ||
| Ntk_Network_t * | network, | ||
| Img_MethodType | methodType, | ||
| Img_DirectionType | directionType, | ||
| int | FAFWFlag, | ||
| mdd_t * | Winning | ||
| ) |
Function********************************************************************
Synopsis [Initializes an imageInfo structure for the given method and direction.]
Description [Initializes an imageInfo structure. MethodType specifies which image computation method to use. If methodType is Img_Default_c, then if the user-settable flag "image_method" has been set, then this method is used, otherwise some default is used. DirectionType specifies which types of image computations will be performed (forward, backward, or both). Method-specific initialization takes into account the value of relevant parameters in the global flag table.
MddNetwork is a graph representing the functions to be used. Each vertex of the graph contains a multi-valued function (MVF) and an MDD id. The MVF gives the function of the vertex in terms of the MDD ids of the immediate fanins of the vertex.
Roots is an array of char* specifying the vertices of the graph which represent those functions for which we want to compute the image (it must not be empty); for example, for an FSM, roots represent the next state functions. DomainVars is an array of mddIds; for an FSM, these are the present state variables. Subsets of the domain are defined over these variables. RangeVars is an array of mddIds over which the range is expressed; for an FSM, these are the next state variables. This array must be in one-to-one correspondence with the array of roots. QuantifyVars is an array of mddIds, representing variables to be quantified from results of backward images; for an FSM, these are the input variables. This array may be empty. No copies are made of any of the input parameters, and thus it is the application's responsibility to free this data *after* the returned Img_ImageInfo_t is freed.]
Comment [To add a new method, see the instructions at the top of imgInt.h.]
SideEffects []
SeeAlso [Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd Img_ImageInfoFree]
Definition at line 201 of file imgUtil.c.
{
char *flagValue;
int verbosity;
mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork);
int updateFlag = 0;
assert(array_n(roots) != 0);
/* If it does not exist, create a new one and initialize fields appropriately
*/
if (imageInfo == NIL(Img_ImageInfo_t)) {
imageInfo = ALLOC(Img_ImageInfo_t, 1);
memset(imageInfo, 0, sizeof(Img_ImageInfo_t));
imageInfo->directionType = directionType;
if (Cmd_FlagReadByName("linear_optimize"))
imageInfo->linearOptimize = Opt_NS;
/*
* Initialization of the function structure inside ImageInfo .
* Since no duplication is needed, this process is not encapsulated
* inside a static procedure.
*/
imageInfo->functionData.FAFWFlag = FAFWFlag;
imageInfo->functionData.Winning = Winning;
imageInfo->functionData.mddNetwork = mddNetwork;
imageInfo->functionData.roots = roots;
imageInfo->functionData.domainVars = domainVars;
imageInfo->functionData.rangeVars = rangeVars;
imageInfo->functionData.quantifyVars = quantifyVars;
imageInfo->functionData.domainCube = domainCube;
imageInfo->functionData.rangeCube = rangeCube;
imageInfo->functionData.quantifyCube = quantifyCube;
imageInfo->functionData.domainBddVars = mdd_id_array_to_bdd_array(
mddManager, domainVars);
imageInfo->functionData.rangeBddVars = mdd_id_array_to_bdd_array(
mddManager, rangeVars);
imageInfo->functionData.quantifyBddVars = mdd_id_array_to_bdd_array(
mddManager, quantifyVars);
if (bdd_get_package_name() == CUDD) {
int i, nVars, idD, idR;
mdd_t *varD, *varR;
nVars = bdd_num_vars(mddManager);
imageInfo->functionData.permutD2R = ALLOC(int, sizeof(int) * nVars);
imageInfo->functionData.permutR2D = ALLOC(int, sizeof(int) * nVars);
for (i = 0; i < nVars; i++) {
imageInfo->functionData.permutD2R[i] = i;
imageInfo->functionData.permutR2D[i] = i;
}
nVars = array_n(imageInfo->functionData.rangeBddVars);
for (i = 0; i < nVars; i++) {
varD = array_fetch(bdd_t *, imageInfo->functionData.domainBddVars, i);
varR = array_fetch(bdd_t *, imageInfo->functionData.rangeBddVars, i);
idD = (int)bdd_top_var_id(varD);
idR = (int)bdd_top_var_id(varR);
imageInfo->functionData.permutD2R[idD] = idR;
imageInfo->functionData.permutR2D[idR] = idD;
}
} else {
imageInfo->functionData.permutD2R = NIL(int);
imageInfo->functionData.permutR2D = NIL(int);
}
if (domainCube)
imageInfo->functionData.createVarCubesFlag = 1;
imageInfo->functionData.network = network;
imageInfo->methodData = NIL(void);
updateFlag = 1;
}
/*
* If methodType is default, use user-specified method if set.
*/
if (methodType == Img_Default_c)
methodType = Img_UserSpecifiedMethod();
/* If image_method changes, we need to free existing method data and
* to update proper function calls.
*/
if (imageInfo->methodData) {
if (imageInfo->methodType != methodType) {
(*imageInfo->imageFreeProc)(imageInfo->methodData);
imageInfo->methodData = NIL(void);
updateFlag = 1;
}
}
if (updateFlag) {
imageInfo->methodType = methodType;
switch (methodType) {
case Img_Monolithic_c:
imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdMono;
imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdMono;
imageInfo->imageComputeFwdWithDomainVarsProc =
ImgImageInfoComputeFwdWithDomainVarsMono;
imageInfo->imageComputeBwdWithDomainVarsProc =
ImgImageInfoComputeBwdWithDomainVarsMono;
imageInfo->imageFreeProc = ImgImageInfoFreeMono;
imageInfo->imagePrintMethodParamsProc =
ImgImageInfoPrintMethodParamsMono;
break;
case Img_Tfm_c:
case Img_Hybrid_c:
imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdTfm;
imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdTfm;
imageInfo->imageComputeFwdWithDomainVarsProc =
ImgImageInfoComputeFwdWithDomainVarsTfm;
imageInfo->imageComputeBwdWithDomainVarsProc =
ImgImageInfoComputeBwdWithDomainVarsTfm;
imageInfo->imageFreeProc = ImgImageInfoFreeTfm;
imageInfo->imagePrintMethodParamsProc =
ImgImageInfoPrintMethodParamsTfm;
break;
case Img_Linear_Range_c:
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdIwls95;
imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdIwls95;
imageInfo->imageComputeFwdWithDomainVarsProc =
ImgImageInfoComputeFwdWithDomainVarsIwls95;
imageInfo->imageComputeBwdWithDomainVarsProc =
ImgImageInfoComputeBwdWithDomainVarsIwls95;
imageInfo->imageFreeProc = ImgImageInfoFreeIwls95;
imageInfo->imagePrintMethodParamsProc =
ImgImageInfoPrintMethodParamsIwls95;
break;
default:
fail("** img error: Unexpected type when updating image method");
}
imageInfo->fwdTrMinimizedFlag = FALSE;
imageInfo->bwdTrMinimizedFlag = FALSE;
imageInfo->printMinimizeStatus = 0;
imageInfo->savedRelation = NIL(void);
flagValue = Cmd_FlagReadByName("image_verbosity");
if (flagValue != NIL(char)) {
verbosity = atoi(flagValue);
imageInfo->verbosity = verbosity;
if (verbosity == 1)
imageInfo->printMinimizeStatus = 1;
else if (verbosity > 1)
imageInfo->printMinimizeStatus = 2;
}
}
/*
* Perform method-specific initialization of methodData.
*/
switch (imageInfo->methodType) {
case Img_Monolithic_c:
imageInfo->methodData =
ImgImageInfoInitializeMono(imageInfo->methodData,
&(imageInfo->functionData),
directionType);
break;
case Img_Tfm_c:
case Img_Hybrid_c:
imageInfo->methodData =
ImgImageInfoInitializeTfm(imageInfo->methodData,
&(imageInfo->functionData),
directionType,
imageInfo->methodType);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
case Img_Linear_Range_c:
imageInfo->methodData =
ImgImageInfoInitializeIwls95(imageInfo->methodData,
&(imageInfo->functionData),
directionType,
imageInfo->methodType);
break;
default:
fail("IMG Error : Unexpected type when initalizing image method");
}
return imageInfo;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Img_MethodType Img_ImageInfoObtainMethodType | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [Returns the method type of an imageInfo.]
Description [Returns the method type of an imageInfo.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize]
Definition at line 958 of file imgUtil.c.
{
return(imageInfo->methodType);
}
Here is the caller graph for this function:
| char* Img_ImageInfoObtainMethodTypeAsString | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [Returns a string giving the method type of an imageInfo.]
Description [Returns a string giving the method type of an imageInfo. It is the user's responsibility to free this string.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize]
Definition at line 912 of file imgUtil.c.
{
char *methodString;
Img_MethodType methodType = imageInfo->methodType;
switch (methodType) {
case Img_Monolithic_c:
methodString = util_strsav("monolithic");
break;
case Img_Tfm_c:
methodString = util_strsav("tfm");
break;
case Img_Hybrid_c:
methodString = util_strsav("hybrid");
break;
case Img_Iwls95_c:
methodString = util_strsav("iwls95");
break;
case Img_Mlp_c:
methodString = util_strsav("mlp");
break;
case Img_Linear_c:
methodString = util_strsav("linear");
break;
case Img_Default_c:
methodString = util_strsav("default");
break;
default:
fail("IMG Error : Unexpected type when initalizing image method");
}
return methodString;
}
Here is the caller graph for this function:
| Img_OptimizeType Img_ImageInfoObtainOptimizeType | ( | Img_ImageInfo_t * | imageInfo | ) |
AutomaticEnd
Function********************************************************************
Synopsis [Returns the method type of an imageInfo.]
Description [Returns the method type of an imageInfo.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize]
Definition at line 975 of file imgUtil.c.
{
return(imageInfo->linearOptimize);
}
Here is the caller graph for this function:
| void Img_ImageInfoPrintMethodParams | ( | Img_ImageInfo_t * | imageInfo, |
| FILE * | fp | ||
| ) |
Function********************************************************************
Synopsis [Prints information about the image technique currently used.]
Description [Prints information about the image technique currently used.]
SideEffects [None.]
Definition at line 1058 of file imgUtil.c.
{
(*imageInfo->imagePrintMethodParamsProc)(imageInfo->methodData, fp);
}
Here is the caller graph for this function:
| void Img_ImageInfoResetLinearComputeRange | ( | Img_ImageInfo_t * | imageInfo | ) |
| void Img_ImageInfoResetUseOptimizedRelationFlag | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [reset optimization relation flag .]
Description [reset optimization relation flag .]
SideEffects []
SeeAlso [Img_ImageInfoInitialize]
Definition at line 1009 of file imgUtil.c.
{
imageInfo->useOptimizedRelationFlag = 0;
}
Here is the caller graph for this function:
| void Img_ImageInfoSetLinearComputeRange | ( | Img_ImageInfo_t * | imageInfo | ) |
| void Img_ImageInfoSetUseOptimizedRelationFlag | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [set optimization relation flag .]
Description [set optimization relation flag .]
SideEffects []
SeeAlso [Img_ImageInfoInitialize]
Definition at line 992 of file imgUtil.c.
{
imageInfo->useOptimizedRelationFlag = 1;
}
Here is the caller graph for this function:
| void Img_ImageInfoUpdateVariables | ( | Img_ImageInfo_t * | imageInfo, |
| graph_t * | mddNetwork, | ||
| array_t * | domainVars, | ||
| array_t * | quantifyVars, | ||
| mdd_t * | domainCube, | ||
| mdd_t * | quantifyCube | ||
| ) |
Function********************************************************************
Synopsis [Updates present state and primary input variables.]
Description [Updates present state and primary input variables. This function is called after calling ImageInfoInitialize for a subFsm.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize]
Definition at line 457 of file imgUtil.c.
{
mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork);
imageInfo->functionData.domainVars = domainVars;
imageInfo->functionData.quantifyVars = quantifyVars;
imageInfo->functionData.domainCube = domainCube;
imageInfo->functionData.quantifyCube = quantifyCube;
mdd_array_free(imageInfo->functionData.domainBddVars);
imageInfo->functionData.domainBddVars = mdd_id_array_to_bdd_array(
mddManager, domainVars);
mdd_array_free(imageInfo->functionData.quantifyBddVars);
imageInfo->functionData.quantifyBddVars = mdd_id_array_to_bdd_array(
mddManager, quantifyVars);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_ImagePrintPartialImageOptions | ( | void | ) |
Function********************************************************************
Synopsis [Prints partial image options.]
Description [Prints partial image options.]
SideEffects []
Definition at line 517 of file imgUtil.c.
{
ImgPrintPartialImageOptions();
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean Img_ImageWasPartial | ( | Img_ImageInfo_t * | info | ) |
Function********************************************************************
Synopsis [Queries whether the last image computation was partial.]
Description [Queries whether the last image computation was partial. Reset before every image/preimage computation i.e., this information is valid for only the previous image/preimage computation.]
SideEffects [Reset before every image/preimage computation.]
SeeAlso [Img_ImageAllowPartialImage]
Definition at line 539 of file imgUtil.c.
{
if (info->methodType == Img_Iwls95_c || info->methodType == Img_Mlp_c)
return (ImgImageWasPartialIwls95(info->methodData));
else
return FALSE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_Init | ( | void | ) |
| int Img_IsPartitionedTransitionRelation | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [Returns 1 if partitioned transition relation is used.]
Description [Returns 1 if partitioned transition relation is used.]
SideEffects []
Definition at line 1659 of file imgUtil.c.
{
if (imageInfo->methodType == Img_Iwls95_c ||
imageInfo->methodType == Img_Mlp_c ||
imageInfo->methodType == Img_Linear_c)
return(1);
else if (imageInfo->methodType == Img_Hybrid_c)
return(ImgIsPartitionedTransitionRelationTfm(imageInfo));
else
return(0);
}
Here is the call graph for this function:
| int Img_IsQuantifyArraySame | ( | Img_ImageInfo_t * | imageInfo, |
| array_t * | quantifyArray | ||
| ) |
Function********************************************************************
Synopsis [Check the given address of array+t is same as the functionData.quantifyArray.]
Description [This function is for remove memory leakage.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize]
Definition at line 433 of file imgUtil.c.
{
if(imageInfo->functionData.quantifyVars == quantifyArray)
return (1);
else
return(0);
}
Here is the caller graph for this function:
| int Img_IsQuantifyCubeSame | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | quantifyCube | ||
| ) |
Function********************************************************************
Synopsis [Check the given address of mdd_t is same as the functionData.quantifyCube.]
Description [This function is for remove memory leakage.]
SideEffects []
SeeAlso [Img_ImageInfoInitialize]
Definition at line 411 of file imgUtil.c.
{
if(imageInfo->functionData.quantifyCube == quantifyCube)
return (1);
else
return(0);
}
Here is the caller graph for this function:
| mdd_t* Img_MinimizeImage | ( | mdd_t * | image, |
| mdd_t * | constraint, | ||
| Img_MinimizeType | method, | ||
| boolean | underapprox | ||
| ) |
Function********************************************************************
Synopsis [Minimizes an image with given constraint.]
Description [Minimizes an image with given constraint. This function can be used to minimize any BDDs.
If underapprox is 1, the the bdds are underapproximated. If it is 0, they are overapproximated, and the minimizeMethod has to be either ornot or squeeze. ]
SideEffects []
Definition at line 1254 of file imgUtil.c.
{
mdd_t *newImage;
mdd_t *l, *u;
if (method == Img_DefaultMinimizeMethod_c)
method = Img_ReadMinimizeMethod();
if(underapprox){
switch (method) {
case Img_Restrict_c :
newImage = bdd_minimize(image, constraint);
break;
case Img_Constrain_c :
newImage = bdd_cofactor(image, constraint);
break;
case Img_Compact_c :
newImage = bdd_compact(image, constraint);
break;
case Img_Squeeze_c :
l = bdd_and(image, constraint, 1, 1);
u = bdd_or(image, constraint, 1, 0);
newImage = bdd_squeeze(l, u);
if (bdd_size(newImage) >= bdd_size(image)) {
bdd_free(newImage);
newImage = bdd_dup(image);
}
mdd_free(l);
mdd_free(u);
break;
case Img_And_c :
newImage = bdd_and(image, constraint, 1, 1);
break;
default :
fail("** img error : Unexpected type when minimizing an image");
}
}else{ /* if underapprox */
switch (method) {
case Img_Squeeze_c :
l = image;
u = bdd_or(image, constraint, 1, 0);
newImage = bdd_squeeze(l, u);
if (bdd_size(newImage) >= bdd_size(image)) {
bdd_free(newImage);
newImage = bdd_dup(image);
}
mdd_free(u);
break;
case Img_OrNot_c :
newImage = bdd_or(image, constraint, 1, 0);
break;
default :
fail("** img error: Unexpected type when adding dont-cares to an image");
}
}/* if underapprox */
return(newImage);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Img_MinimizeImageArray | ( | mdd_t * | image, |
| array_t * | constraintArray, | ||
| Img_MinimizeType | method, | ||
| boolean | underapprox | ||
| ) |
Function********************************************************************
Synopsis [Minimizes a single bdd with a set of constraint.]
Description [Minimizes a bdd with given set of constraints. Underapproximates if underapprox is true, otherwise overapproximated (in which case method has to be ornot or squeeze).]
SideEffects [Img_MinimizeImage]
Definition at line 1349 of file imgUtil.c.
{
int i;
mdd_t *newImage, *tmpImage;
mdd_t *constraint;
if (method == Img_DefaultMinimizeMethod_c)
method = Img_ReadMinimizeMethod();
newImage = mdd_dup(image);
arrayForEachItem(mdd_t *, constraintArray, i, constraint) {
tmpImage = newImage;
newImage = Img_MinimizeImage(tmpImage, constraint, method, underapprox);
mdd_free(tmpImage);
}
return(newImage);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_MinimizeTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| array_t * | constrainArray, | ||
| Img_MinimizeType | minimizeMethod, | ||
| Img_DirectionType | directionType, | ||
| boolean | reorderIwls95Clusters | ||
| ) |
Function********************************************************************
Synopsis [Minimizes transition relation with given constraint if it hasn't been minimized already.]
Description [Minimizes transition relation with given constraint if it hasn't been minimized already (does nothing otherwise). The constraint is expressed as an array of conjuncts of BDDs, The transition relation is minimized with each one of the conjuncts.
The boolean reorderIwls95Clusters is only relevant to the iwls95 image method. It causes the clusters to be ordered again after minimization.
The conjuncts have to be in terms of present-state variables or inputs. Next-state variables are not allowed.
For the hybrid and tfm methods, for image, we can only minimize wrt a set that includes any possible argument. For preimage, the result is only correct for as far as it lies within the set that the TR is minimized with. That means that reachability info can be usefully applied here.
For the other methods, we can also minimize wrt different sets. The edges in the TR that are outgoing from states not in this set may then get removed.]
SideEffects []
Definition at line 1175 of file imgUtil.c.
{
if (minimizeMethod == Img_DefaultMinimizeMethod_c)
minimizeMethod = Img_ReadMinimizeMethod();
switch (imageInfo->methodType) {
case Img_Monolithic_c:
if (imageInfo->fwdTrMinimizedFlag)
break;
ImgMinimizeTransitionRelationMono(imageInfo, constrainArray,
minimizeMethod, imageInfo->printMinimizeStatus);
imageInfo->fwdTrMinimizedFlag = TRUE;
break;
case Img_Tfm_c:
case Img_Hybrid_c:
if (imageInfo->fwdTrMinimizedFlag)
break;
ImgMinimizeTransitionFunction(imageInfo->methodData, constrainArray,
minimizeMethod, directionType,
imageInfo->printMinimizeStatus);
if (directionType == Img_Forward_c || directionType == Img_Both_c)
imageInfo->fwdTrMinimizedFlag = TRUE;
if (directionType == Img_Backward_c || directionType == Img_Both_c)
imageInfo->bwdTrMinimizedFlag = TRUE;
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
if (directionType == Img_Forward_c || directionType == Img_Both_c) {
if (imageInfo->fwdTrMinimizedFlag == FALSE) {
ImgMinimizeTransitionRelationIwls95(imageInfo->methodData,
&(imageInfo->functionData),
constrainArray, minimizeMethod,
Img_Forward_c,
reorderIwls95Clusters,
imageInfo->printMinimizeStatus);
imageInfo->fwdTrMinimizedFlag = TRUE;
}
}
if (directionType == Img_Backward_c || directionType == Img_Both_c) {
if (imageInfo->bwdTrMinimizedFlag == FALSE) {
ImgMinimizeTransitionRelationIwls95(imageInfo->methodData,
&(imageInfo->functionData),
constrainArray, minimizeMethod,
Img_Backward_c,
reorderIwls95Clusters,
imageInfo->printMinimizeStatus);
imageInfo->bwdTrMinimizedFlag = TRUE;
}
}
break;
default:
fail("** img error: Unexpected type when minimizing transition relation");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Img_MinimizeType Img_ReadMinimizeMethod | ( | void | ) |
Function********************************************************************
Synopsis [Returns current method of minimizing transition relation.]
Description [Returns current method of minimizing transition relation. Default is restrict.]
SideEffects []
Definition at line 1093 of file imgUtil.c.
{
int value;
char *flagValue;
Img_MinimizeType minimizeMethod = Img_Restrict_c;
flagValue = Cmd_FlagReadByName("image_minimize_method");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &value);
switch (value) {
case 0 :
minimizeMethod = Img_Restrict_c;
break;
case 1 :
minimizeMethod = Img_Constrain_c;
break;
case 2 :
if (bdd_get_package_name() != CUDD) {
fprintf(vis_stderr, "** img error : Compact in image_minimize_method ");
fprintf(vis_stderr, "is currently supported only by CUDD. ***\n");
fprintf(vis_stderr,
"** img error : Reverting to default minimize method : restrict\n");
break;
}
minimizeMethod = Img_Compact_c;
break;
case 3 :
if (bdd_get_package_name() != CUDD) {
fprintf(vis_stderr, "** img error : Squeeze in image_minimize_method ");
fprintf(vis_stderr, "is currently supported only by CUDD. ***\n");
fprintf(vis_stderr,
"** img error : Reverting to default minimize method : restrict\n");
break;
}
minimizeMethod = Img_Squeeze_c;
break;
case 4 :
minimizeMethod = Img_And_c;
break;
default :
fprintf(vis_stderr,
"** img error : invalid value %s for image_minimize_method[0-4]. ***\n",
flagValue);
fprintf(vis_stderr,
"** img error : Reverting to default minimize method : restrict\n");
break;
}
}
return(minimizeMethod);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Img_ReadPrintMinimizeStatus | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [Reads the flag whether to print the status of minimizing transition relation.]
Description [Reads the flag whether to print the status of minimizing transition relation.]
SideEffects []
Definition at line 1404 of file imgUtil.c.
{
return(imageInfo->printMinimizeStatus);
}
Here is the caller graph for this function:
| void Img_ReplaceIthPartitionedTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| int | i, | ||
| mdd_t * | relation, | ||
| Img_DirectionType | directionType | ||
| ) |
Function********************************************************************
Synopsis [Replace ith partitioned transition relation.]
Description [Replace ith partitioned transition relation.]
SideEffects []
Definition at line 1760 of file imgUtil.c.
{
switch (imageInfo->methodType) {
case Img_Monolithic_c:
break;
case Img_Tfm_c:
case Img_Hybrid_c:
ImgReplaceIthTransitionFunction(imageInfo->methodData, i, relation,
directionType);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
ImgReplaceIthPartitionedTransitionRelationIwls95(imageInfo->methodData,
i, relation, directionType);
break;
default:
fail("** img error: Unexpected image method type.\n");
}
}
Here is the call graph for this function:
| void Img_ReplacePartitionedTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| array_t * | relationArray, | ||
| Img_DirectionType | directionType | ||
| ) |
Function********************************************************************
Synopsis [Replace partitioned transition relation.]
Description [Replace partitioned transition relation.]
SideEffects []
Definition at line 1793 of file imgUtil.c.
{
switch (imageInfo->methodType) {
case Img_Monolithic_c:
break;
case Img_Tfm_c:
case Img_Hybrid_c:
ImgUpdateTransitionFunction(imageInfo->methodData, relationArray,
directionType);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
ImgUpdateTransitionRelationIwls95(imageInfo->methodData,
relationArray, directionType);
break;
default:
fail("** img error: Unexpected image method type.\n");
}
}
Here is the call graph for this function:
| void Img_ResetNumberOfImageComputation | ( | Img_DirectionType | imgDir | ) |
Function********************************************************************
Synopsis [Resets number of image/preimage computation.]
Description [Resets number of image/preimage computation.]
SideEffects []
Definition at line 1682 of file imgUtil.c.
{
if (imgDir == Img_Forward_c || imgDir == Img_Both_c)
nImgComps = 0;
if (imgDir == Img_Backward_c || imgDir == Img_Both_c)
nPreComps = 0;
}
Here is the caller graph for this function:
| void Img_ResetTrMinimizedFlag | ( | Img_ImageInfo_t * | imageInfo, |
| Img_DirectionType | directionType | ||
| ) |
Function********************************************************************
Synopsis [Resets the flag that transition relation is minimized.]
Description [Resets the flag that transition relation is minimized.]
SideEffects []
Definition at line 1073 of file imgUtil.c.
{
if (directionType == Img_Forward_c || directionType == Img_Both_c)
imageInfo->fwdTrMinimizedFlag = FALSE;
if (directionType == Img_Backward_c || directionType == Img_Both_c)
imageInfo->bwdTrMinimizedFlag = FALSE;
}
Here is the caller graph for this function:
| void Img_RestoreTransitionRelation | ( | Img_ImageInfo_t * | imageInfo, |
| Img_DirectionType | directionType | ||
| ) |
Function********************************************************************
Synopsis [Restores original transition relation from saved.]
Description [Restores original transition relation from saved.]
SideEffects []
Definition at line 1489 of file imgUtil.c.
{
switch (imageInfo->methodType) {
case Img_Monolithic_c:
ImgRestoreTransitionRelationMono(imageInfo, directionType);
break;
case Img_Tfm_c:
case Img_Hybrid_c:
ImgRestoreTransitionFunction(imageInfo, directionType);
break;
case Img_Iwls95_c:
case Img_Mlp_c:
case Img_Linear_c:
ImgRestoreTransitionRelationIwls95(imageInfo, directionType);
break;
default:
fail("** img error : Unexpected type when backup transition relation");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Img_SetPrintMinimizeStatus | ( | Img_ImageInfo_t * | imageInfo, |
| int | status | ||
| ) |
Function********************************************************************
Synopsis [Sets the flag whether to print the status of minimizing transition relation.]
Description [Sets the flag whether to print the status of minimizing transition relation.]
SideEffects []
Definition at line 1383 of file imgUtil.c.
{
if (status < 0 || status > 2)
(void)fprintf(vis_stderr,
"** img error: invalid value[%d] for status.\n", status);
else
imageInfo->printMinimizeStatus = status;
}
Here is the caller graph for this function:
| mdd_t* Img_Substitute | ( | Img_ImageInfo_t * | imageInfo, |
| mdd_t * | f, | ||
| Img_SubstituteDir | dir | ||
| ) |
Function********************************************************************
Synopsis [Substitutes variables between domain and range.]
Description [Substitutes variables between domain and range.]
SideEffects []
Definition at line 2049 of file imgUtil.c.
{
mdd_t *new_;
new_ = ImgSubstitute(f, &(imageInfo->functionData), dir);
return(new_);
}
Here is the call graph for this function:
| Img_MethodType Img_UserSpecifiedMethod | ( | void | ) |
Function********************************************************************
Synopsis [Return the image method preferred by the user.]
Description [Returns the method selected by Img_ImageInfoInitialize if Img_Default_c is passed in. Note that this may change if the user changes the definition of the image_method set flag.]
SideEffects []
SeeAlso [Img_ImageInfoIninitialize]
Definition at line 135 of file imgUtil.c.
{
char *userSpecifiedMethod;
userSpecifiedMethod = Cmd_FlagReadByName("image_method");
if (userSpecifiedMethod == NIL(char))
return IMGDEFAULT_METHOD;
if (strcmp(userSpecifiedMethod, "monolithic") == 0)
return Img_Monolithic_c;
if (strcmp(userSpecifiedMethod, "tfm") == 0)
return Img_Tfm_c;
if (strcmp(userSpecifiedMethod, "hybrid") == 0)
return Img_Hybrid_c;
if (strcmp(userSpecifiedMethod, "iwls95") == 0)
return Img_Iwls95_c;
if (strcmp(userSpecifiedMethod, "mlp") == 0)
return Img_Mlp_c;
fprintf(vis_stderr, "** img error: Unrecognized image_method %s",
userSpecifiedMethod);
fprintf(vis_stderr, "using default method.\n");
return IMGDEFAULT_METHOD;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int ImgArrayBddArrayCheckValidity | ( | array_t * | arrayBddArray | ) |
Function********************************************************************
Synopsis [This function checks the validity of an array of array of BDD nodes.]
SideEffects []
SeeAlso [ImgBddCheckValidity]
Definition at line 2405 of file imgUtil.c.
{
int i;
for(i=0; i<array_n(arrayBddArray); i++) {
ImgBddArrayCheckValidity(array_fetch(array_t*, arrayBddArray, i));
}
return 1;
}
Here is the call graph for this function:
| int ImgBddArrayCheckValidity | ( | array_t * | bddArray | ) |
Function********************************************************************
Synopsis [This function checks the validity of array of BDD nodes.]
SideEffects []
SeeAlso [ImgBddCheckValidity]
Definition at line 2425 of file imgUtil.c.
{
int i;
for(i=0; i<array_n(bddArray); i++) {
ImgBddCheckValidity(array_fetch(bdd_t*, bddArray, i));
}
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int ImgBddCheckValidity | ( | bdd_t * | bdd | ) |
Function********************************************************************
Synopsis [This function checks the validity of a BDD.]
Description [[This function checks the validity of a BDD. Three checks are done: 1. The BDD should not be freed. "free" field should be 0. 2. The node pointer of the BDD should be a valid pointer. 3. The manager pointer of the BDD should be a valid pointer. The assumption for 2 and 3 is that, the value of a valid pointer should be > 0xf.]
SideEffects []
Definition at line 2450 of file imgUtil.c.
{
#ifndef NDEBUG
int i;
#endif
assert(bdd_get_free(bdd) == 0); /* Bdd should not have been freed */
assert(((unsigned long)bdd_get_node(bdd, &i)) & ~0xf); /* Valid node pointer */
assert(((unsigned long)bdd_get_manager(bdd)) & ~0xf); /* Valid manager pointer */
return 1;
}
Here is the caller graph for this function:
| int ImgCheckToCareSetArrayChanged | ( | array_t * | toCareSetArray1, |
| array_t * | toCareSetArray2 | ||
| ) |
Function********************************************************************
Synopsis [Checks whether toCareSetArray changed.]
Description [Checks whether toCareSetArray changed.]
SideEffects []
Definition at line 2493 of file imgUtil.c.
{
int i, size1, size2;
mdd_t *careSet1, *careSet2;
size1 = array_n(toCareSetArray1);
size2 = array_n(toCareSetArray2);
if (size1 != size2)
return(1);
for (i = 0; i < size1; i++) {
careSet1 = array_fetch(mdd_t *, toCareSetArray1, i);
careSet2 = array_fetch(mdd_t *, toCareSetArray2, i);
if (bdd_equal(careSet1, careSet2) == 0)
return(1);
}
return(0);
}
| ImgPartialImageOption_t* ImgGetPartialImageOptions | ( | void | ) |
Function********************************************************************
Synopsis [Get partial image options.]
Description [Get partial image options.]
SideEffects []
Definition at line 2298 of file imgUtil.c.
{
ImgPartialImageOption_t *options;
char *qualityString;
char *partialImageThresholdString, *partialImageApproxString, *partialImageSizeString;
char *partialImageMethodString, *clippingDepthString;
options = ALLOC(ImgPartialImageOption_t , 1);
if (options == NIL(ImgPartialImageOption_t)) return NIL(ImgPartialImageOption_t);
/* initialize to default values; */
options->nvars = 0;
options->partialImageMethod = Img_PIApprox_c;
options->partialImageThreshold = 200000;
options->partialImageSize = 100000;
options->partialImageApproxMethod = BDD_APPROX_RUA;
options->quality = 1.0;
options->qualityBias = 0.5;
options->clippingDepthFrac = IMG_PI_CLIP_DEPTH;
/* what kind of approximation to apply to the image */
partialImageMethodString = Cmd_FlagReadByName("hd_partial_image_method");
if (partialImageMethodString != NIL(char)) {
if (strcmp(partialImageMethodString, "approx") == 0) {
options->partialImageMethod = Img_PIApprox_c;
} else if (strcmp(partialImageMethodString, "clipping") == 0) {
options->partialImageMethod = Img_PIClipping_c;
}
}
/* threshold to trigger partial image computation */
partialImageThresholdString = Cmd_FlagReadByName("hd_partial_image_threshold");
if (partialImageThresholdString != NIL(char)) {
options->partialImageThreshold = strtol(partialImageThresholdString, NULL, 10);
if (options->partialImageThreshold < 0) {
options->partialImageThreshold = 200000;
}
}
/* intended size of partial image */
partialImageSizeString = Cmd_FlagReadByName("hd_partial_image_size");
if (partialImageSizeString != NIL(char)) {
options->partialImageSize = strtol(partialImageSizeString, NULL, 10);
if (options->partialImageSize < 0) {
options->partialImageSize = 100000;
}
}
/* which approximation method to apply */
partialImageApproxString = Cmd_FlagReadByName("hd_partial_image_approx");
if (partialImageApproxString != NIL(char)) {
if (strcmp(partialImageApproxString, "heavy_branch") == 0) {
options->partialImageApproxMethod = BDD_APPROX_HB;
} else if (strcmp(partialImageApproxString, "short_paths") == 0) {
options->partialImageApproxMethod = BDD_APPROX_SP;
} else if (strcmp(partialImageApproxString, "under_approx") == 0) {
options->partialImageApproxMethod = BDD_APPROX_UA;
} else if (strcmp(partialImageApproxString, "remap_ua") == 0) {
options->partialImageApproxMethod = BDD_APPROX_RUA;
} else if (strcmp(partialImageApproxString, "compress") == 0) {
options->partialImageApproxMethod = BDD_APPROX_COMP;
} else if (strcmp(partialImageApproxString, "biased_rua") == 0) {
options->partialImageApproxMethod = BDD_APPROX_BIASED_RUA;
}
}
/* quality factor for remap_ua and under_approx methods */
qualityString = Cmd_FlagReadByName("hd_partial_image_approx_quality");
if (qualityString != NIL(char)) {
options->quality = strtod(qualityString, NULL);
if (options->quality < 0.0) {
options->quality = 1.0;
}
}
/* quality factor for remap_ua and under_approx methods */
qualityString = Cmd_FlagReadByName("hd_partial_image_approx_bias_quality");
if (qualityString != NIL(char)) {
options->qualityBias = strtod(qualityString, NULL);
if (options->qualityBias < 0.0) {
options->qualityBias = 0.5;
}
}
/* fraction of depth of Bdd to clip at. */
clippingDepthString = Cmd_FlagReadByName("hd_partial_image_clipping_depth");
if (clippingDepthString != NIL(char)) {
options->clippingDepthFrac = strtod(clippingDepthString, NULL);
if ((options->clippingDepthFrac > 1.0) ||
(options->clippingDepthFrac < 0.0)) {
options->clippingDepthFrac = IMG_PI_CLIP_DEPTH;
}
}
return (options);
} /* end of ImgGetPartialImageOptions */
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* ImgMinimizeImageArrayWithCareSetArray | ( | array_t * | imageArray, |
| array_t * | careSetArray, | ||
| Img_MinimizeType | minimizeMethod, | ||
| boolean | underapprox, | ||
| boolean | printInfo, | ||
| Img_DirectionType | dir | ||
| ) |
Function********************************************************************
Synopsis [Minimize array of bdds wrt a set of constraints]
Description [Compute a new array, such that every element corresponds to an element of imageArray minimized with all elements of careSetArray successively, using minimizeMethod. This function can be used for any array of bdds.
If underapprox is 1, the the bdds are underapproximated. If it is 0, they are overapproximated, and the minimizeMethod has to be either ornot or squeeze.]
SideEffects []
SeeAlso[Img_MinimizeImage ImgMinimizeImageArrayWithCareSetArrayInSitu]
Definition at line 2081 of file imgUtil.c.
{
array_t *result; /* of mdd_t * */
result = mdd_array_duplicate(imageArray);
ImgMinimizeImageArrayWithCareSetArrayInSitu(result, careSetArray,
minimizeMethod, underapprox,
printInfo, dir);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void ImgMinimizeImageArrayWithCareSetArrayInSitu | ( | array_t * | imageArray, |
| array_t * | careSetArray, | ||
| Img_MinimizeType | minimizeMethod, | ||
| boolean | underapprox, | ||
| boolean | printInfo, | ||
| Img_DirectionType | dir | ||
| ) |
Function********************************************************************
Synopsis [Minimize array of bdds wrt a set of constraints]
Description [Compute a new array, such that every element corresponds to an element of imageArray minimized with all elements of careSetArray successively, using minimizeMethod. This function can be used for any array of bdds.
If underapprox is 1, the the bdds are underapproximated. If it is 0, they are overapproximated, and the minimizeMethod has to be either ornot or squeeze.
In-situ variant of ImgMinimizeImageArrayWithCareSetArray. Probably saves space. ]
SideEffects []
SeeAlso[Img_MinimizeImage,ImgMinimizeImageArrayWithCareSetArray]
Definition at line 2121 of file imgUtil.c.
{
int i;
mdd_t *cluster = NIL(mdd_t);
long constrainSize, initialTotalSize;
char *dirname = NIL(char);
if (minimizeMethod == Img_DefaultMinimizeMethod_c)
minimizeMethod = Img_ReadMinimizeMethod();
if(printInfo){
constrainSize = mdd_size_multiple(careSetArray);
initialTotalSize = mdd_size_multiple(imageArray);
assert(dir != Img_Both_c);
if(dir == Img_Forward_c)
dirname = "fwd";
else
dirname = "bwd";
} else { /* to remove uninitialized variable warnings */
constrainSize = 0;
initialTotalSize = 0;
}
arrayForEachItem(mdd_t *, imageArray, i, cluster){
mdd_t *minimized;
minimized = Img_MinimizeImageArray(cluster, careSetArray,
minimizeMethod, underapprox);
array_insert(mdd_t *, imageArray, i, minimized);
if(printInfo)
(void) fprintf(vis_stdout,
"IMG Info: minimized %s relation %d | %ld => %d in component %d.\n",
dirname, mdd_size(cluster), constrainSize,
mdd_size(minimized), i);
mdd_free(cluster);
}
if(printInfo)
(void) fprintf(vis_stdout,
"IMG Info: minimized %s relation %ld | %ld => %ld with %d components.\n",
dirname, initialTotalSize, constrainSize,
mdd_size_multiple(imageArray), array_n(imageArray));
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void ImgPrintPartialImageOptions | ( | void | ) |
Function********************************************************************
Synopsis [Prints Partial Image options.]
Description [Prints Partial Image options.]
SideEffects []
Definition at line 2250 of file imgUtil.c.
{
ImgPartialImageOption_t *PIoption;
char *dummy;
PIoption = ImgGetPartialImageOptions();
dummy = ALLOC(char, 25);
switch (PIoption->partialImageMethod) {
case Img_PIApprox_c: sprintf(dummy, "%s", "approx");break;
case Img_PIClipping_c: sprintf(dummy, "%s", "clipping");break;
default: sprintf(dummy, "%s", "approx");break;
}
fprintf(vis_stdout, "HD: Partial Image number of variables = %d\n", PIoption->nvars);
fprintf(vis_stdout, "HD: Partial Image Method = %s\n", dummy);
fprintf(vis_stdout, "HD: Partial Image Threshold = %d\n", PIoption->partialImageThreshold);
fprintf(vis_stdout, "HD: Partial Image Size = %d\n", PIoption->partialImageSize);
switch (PIoption->partialImageApproxMethod) {
case BDD_APPROX_HB: sprintf(dummy, "%s", "heavy_branch"); break;
case BDD_APPROX_SP: sprintf(dummy, "%s", "short_paths"); break;
case BDD_APPROX_UA: sprintf(dummy, "%s", "under_approx"); break;
case BDD_APPROX_RUA: sprintf(dummy, "%s", "remap_ua"); break;
case BDD_APPROX_COMP: sprintf(dummy, "%s", "compress"); break;
default: sprintf(dummy, "%s", "remap_ua"); break;
}
fprintf(vis_stdout, "HD: Partial Image Approximation Method = %s\n", dummy);
fprintf(vis_stdout, "HD: Partial Image Approximation quality factor = %g\n", PIoption->quality);
fprintf(vis_stdout, "HD: Partial Image Approximation Bias quality factor = %g\n", PIoption->qualityBias);
fprintf(vis_stdout, "HD: Partial Image Clipping factor = %g\n", PIoption->clippingDepthFrac);
FREE(dummy);
FREE(PIoption);
return;
} /* end of ImgPrintPartialImageOptions */
Here is the call graph for this function:
Here is the caller graph for this function:
| void ImgPrintVarIdTable | ( | st_table * | table | ) |
Function********************************************************************
Synopsis [Prints the content of a table containing integers.]
Description [Prints the content of a table containing integers.]
SideEffects []
Definition at line 2472 of file imgUtil.c.
{
st_generator *stgen;
long varId;
st_foreach_item(table, stgen, &varId, NULL){
(void) fprintf(vis_stdout, "%d ", (int) varId);
}
(void) fprintf(vis_stdout, "\n");
}
| mdd_t* ImgSubstitute | ( | mdd_t * | f, |
| ImgFunctionData_t * | functionData, | ||
| Img_SubstituteDir | dir | ||
| ) |
Function********************************************************************
Synopsis [Substitutes variables between domain and range.]
Description [Substitutes variables between domain and range.]
SideEffects []
Definition at line 2184 of file imgUtil.c.
{
mdd_t *new_;
if (bdd_get_package_name() == CUDD) {
if (dir == Img_D2R_c)
new_ = bdd_substitute_with_permut(f, functionData->permutD2R);
else
new_ = bdd_substitute_with_permut(f, functionData->permutR2D);
} else {
if (dir == Img_D2R_c) {
new_ = bdd_substitute(f, functionData->domainBddVars,
functionData->rangeBddVars);
} else {
new_ = bdd_substitute(f, functionData->rangeBddVars,
functionData->domainBddVars);
}
}
return(new_);
}
Here is the caller graph for this function:
| array_t* ImgSubstituteArray | ( | array_t * | f_array, |
| ImgFunctionData_t * | functionData, | ||
| Img_SubstituteDir | dir | ||
| ) |
Function********************************************************************
Synopsis [Substitutes variables between domain and range.]
Description [Substitutes variables between domain and range.]
SideEffects []
Definition at line 2215 of file imgUtil.c.
{
array_t *new_array;
if (bdd_get_package_name() == CUDD) {
if (dir == Img_D2R_c) {
new_array = bdd_substitute_array_with_permut(f_array,
functionData->permutD2R);
} else {
new_array = bdd_substitute_array_with_permut(f_array,
functionData->permutR2D);
}
} else {
if (dir == Img_D2R_c) {
new_array = bdd_substitute_array(f_array, functionData->domainBddVars,
functionData->rangeBddVars);
} else {
new_array = bdd_substitute_array(f_array, functionData->rangeBddVars,
functionData->domainBddVars);
}
}
return(new_array);
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: imgUtil.c,v 1.74 2005/05/14 21:08:32 jinh Exp $" [static] |
CFile***********************************************************************
FileName [imgUtil.c]
PackageName [img]
Synopsis [High-level routines to perform image computations.]
Description [This file provides the exported interface to the method-specific image computation routines.
Minimization of the transition relation can be done in three ways (for Iwls95, not so sure about monolithic and hybrid) (RB):
-
You can call MinimizeTR. This way, you'll loose the old TR, though it could potentially reconstruct it from the bit relations. This is a good option for (overapproximate) reachability info, since the TR will remain valid.
-
You can call the triplet Img_DupTransitionRelation to copy the TR, Img_MinimizeTransitionRelation to minimize the TR, and Img_RestoreTransitionRelation to discard the minimized TR and to restore the original.
-
Finally, if you just want to minimize the TR for a single step, you can pass the care set to the (pre)image computation routine. This does unfortunately (and queerly) not work for image, but only for preimage. If you pas a care set, the TR gets minimized, and the minimized relation is kept and reused until you pass a different care set. Hence, minimizaiton is not done at every preimage computation, but only if you change the care set.
]
Author [Rajeev Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon, Kavita Ravi]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. 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 CALIFORNIA 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 CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA 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 CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
