Data Fields
array_t *	bitRelationArray
array_t *	quantifyVarMddIdArray
array_t *	fwdOptClusteredRelationArray
array_t *	fwdClusteredRelationArray
array_t *	fwdOriClusteredRelationArray
array_t *	bwdClusteredRelationArray
array_t *	bwdOriClusteredRelationArray
array_t *	bwdClusteredCofactoredRelationArray
array_t *	careSetArray
array_t *	fwdOptArraySmoothVarBddArray
array_t *	fwdArraySmoothVarBddArray
array_t *	bwdArraySmoothVarBddArray
array_t *	fwdOptSmoothVarCubeArray
array_t *	fwdSmoothVarCubeArray
array_t *	bwdSmoothVarCubeArray
boolean	allowPartialImage
boolean	wasPartialImage
ImgPartialImageOption_t *	PIoption
array_t *	savedArraySmoothVarBddArray
array_t *	savedSmoothVarCubeArray
Img_MethodType	method
ImgTrmOption_t *	option
int	eliminateDepend
int	nFoundDependVars
float	averageFoundDependVars
int	nPrevEliminatedFwd
int	linearComputeRange
boolean	lazySiftFlag

Detailed Description

Struct**********************************************************************

Synopsis [This structure stores the information needed for iterative image computation by IWLS'95 method.]

Description [A step of image computation is computed by taking the product of "From" set with the BDD's of fwdClusteredRelationArray in order. "fwdArraySmoothVarBddArray[i]" is an array of Bdd variables, which represents the set of variables which can be quantified out once fwdClusteredRelationArray[i] is multiplied in the product. Similar analysis holds good for bwdClusteredRelationArray.

The "option" struct contains option values for computing the above mentioned arrays and also controls the verbosity.

The bit relation array contains the transition relation in a bit relation form.

The quantifyVarMddIdArray contains functionData->quantifyVars and any intermediate variables that need to be quantified.

The *SmoothVarCubeArrays hold the same information as the ArraySmoothVarBddArrays, but in the form of an array of cubes, one cube for each entry of *ArraySmoothVarBddArrays, because the quantification functions expect a cube.

AllowPartialImage is an option for high-density analysis, if it is true, image is allowed to return a subset instead of the correct result. If it does so, it will set wasPartialImage. The PIOptions field keeps the options for partial image computation. (See the definition of the type)

The bwdClusteredCofactoredRelationArray is the clusteredCofactoredRelationArray minimized wrt careSetArray. Minimization only takes place when the careSetArray that is passed is changed. They can both be NIL, which means that they need to be recomputed.

RB What are savedArray*, method, eliminateDepend, nFoundDependVars, averageFOundDependVars, nPrev*, and lazySiftFlag????]

Definition at line 127 of file imgIwls95.c.