Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

imgIwls95.c @ 93

Last change on this file since 93 was 14, checked in by cecile, 13 years ago
vis2.3
File size: 220.2 KB

Line
1	/CFile*********************************************************************
2
3	FileName [imgIwls95.c]
4
5	PackageName [img]
6
7	Synopsis [Routines for image computation using component transition
8	relation approach described in the proceedings of IWLS'95,
9	(henceforth referred to Iwls95 technique).]
10
11	Description [<p>The initialization process performs following steps:
12	<UL>
13	<LI> Create the relation of the roots at the bit level
14	in terms of the quantify and domain variables.
15	<LI> Order the bit level relations.
16	<LI> Group the relations of bits together, making a cluster
17	whenever the BDD size reaches a threshold.
18	<LI> For each cluster, quantify out the quantify variables which
19	are local to that particular cluster.
20	<LI> Order the clusters using the algorithm given in
21	"Efficient BDD Algorithms for FSM Synthesis and
22	Verification", by R. K. Ranjan et. al. in the proceedings of
23	IWLS'95{1}.
24	<LI> The orders of the clusters for forward and backward image are
25	calculated and stored. Also stored is the schedule of
26	variables for early quantification.
27	</UL>
28	For forward and backward image computation the corresponding
29	routines are called with appropriate ordering of clusters and
30	early quantification schedule. <p>
31	Note that, a cubic implementation of the above algorithm is
32	straightforward. However, to obtain quadratic complexity requires
33	significant amount of book-keeping. This is the reason for the complexity
34	of the code in this file.]
35
36	SeeAlso []
37
38	Author [Rajeev K. Ranjan, In-Ho Moon, Kavita Ravi]
39
40	Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California.
41	All rights reserved.
42
43	Permission is hereby granted, without written agreement and without license
44	or royalty fees, to use, copy, modify, and distribute this software and its
45	documentation for any purpose, provided that the above copyright notice and
46	the following two paragraphs appear in all copies of this software.
47
48	IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
49	DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
50	OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
51	CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
52
53	THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
54	INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
55	FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN
56	"AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
57	MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
58
59	******************************************************************************/
60	#include "imgInt.h"
61	#include "fsm.h"
62
63	static char rcsid[] UNUSED = "$Id: imgIwls95.c,v 1.127 2005/05/18 18:11:57 jinh Exp $";
64
65	/---------------------------------------------------------------------------/
66	/* Constant declarations */
67	/---------------------------------------------------------------------------/
68	#define domainVar_c 0
69	#define rangeVar_c 1
70	#define quantifyVar_c 2
71	#define IMG_IWLS95_DEBUG
72
73	/---------------------------------------------------------------------------/
74	/* Type declarations */
75	/---------------------------------------------------------------------------/
76
77	typedef struct Iwls95InfoStruct Iwls95Info_t;
78	typedef struct CtrInfoStruct CtrInfo_t;
79	typedef struct VarInfoStruct VarInfo_t;
80	typedef struct CtrItemStruct CtrItem_t;
81	typedef struct VarItemStruct VarItem_t;
82
83	/---------------------------------------------------------------------------/
84	/* Structure declarations */
85	/---------------------------------------------------------------------------/
86	/Struct********************************************************************
87
88	Synopsis [This structure stores the information needed for iterative image
89	computation by IWLS'95 method.]
90
91	Description [A step of image computation is computed by taking the product of
92	"From" set with the BDD's of fwdClusteredRelationArray in order.
93	"fwdArraySmoothVarBddArray[i]" is an array of Bdd variables, which represents
94	the set of variables which can be quantified out once
95	fwdClusteredRelationArray[i] is multiplied in the product. Similar analysis
96	holds good for bwdClusteredRelationArray.
97
98	<p>The "option" struct contains option values for computing the above
99	mentioned arrays and also controls the verbosity.
100
101	<p>The bit relation array contains the transition relation in a bit relation
102	form.
103
104	<p>The quantifyVarMddIdArray contains functionData->quantifyVars and any
105	intermediate variables that need to be quantified.
106
107	<p> The *SmoothVarCubeArrays hold the same information as the
108	*ArraySmoothVarBddArrays, but in the form of an array of cubes, one cube for
109	each entry of *ArraySmoothVarBddArrays, because the quantification functions
110	expect a cube.
111
112	<p>AllowPartialImage is an option for high-density analysis, if it is true,
113	image is allowed to return a subset instead of the correct result. If it
114	does so, it will set wasPartialImage. The PIOptions field keeps the options
115	for partial image computation. (See the definition of the type)
116
117	<p> The bwdClusteredCofactoredRelationArray is the
118	clusteredCofactoredRelationArray minimized wrt careSetArray. Minimization
119	only takes place when the careSetArray that is passed is changed. They can
120	both be NIL, which means that they need to be recomputed.
121
122	<p> RB What are savedArray*, method, eliminateDepend, nFoundDependVars,
123	averageFOundDependVars, nPrev*, and lazySiftFlag????]
124
125	******************************************************************************/
126
127	struct Iwls95InfoStruct {
128	array_t *bitRelationArray;
129
130	array_t *quantifyVarMddIdArray;
131
132	array_t *fwdOptClusteredRelationArray;
133	array_t *fwdClusteredRelationArray;
134	array_t *fwdOriClusteredRelationArray;
135	array_t *bwdClusteredRelationArray;
136	array_t *bwdOriClusteredRelationArray;
137	array_t *bwdClusteredCofactoredRelationArray;
138	array_t *careSetArray;
139
140	array_t *fwdOptArraySmoothVarBddArray;
141	array_t *fwdArraySmoothVarBddArray;
142	array_t *bwdArraySmoothVarBddArray;
143	array_t *fwdOptSmoothVarCubeArray;
144	array_t *fwdSmoothVarCubeArray;
145	array_t *bwdSmoothVarCubeArray;
146
147	boolean allowPartialImage;
148	boolean wasPartialImage;
149	ImgPartialImageOption_t *PIoption;
150
151	array_t *savedArraySmoothVarBddArray;
152	array_t *savedSmoothVarCubeArray;
153
154	Img_MethodType method;
155	ImgTrmOption_t *option;
156
157	int eliminateDepend;
158	/* 0 : do not perform this
159	1 : eliminates dependent variables from
160	constraint and modifies function vector by
161	composition at every image computation.
162	2 : once the number of eliminated variables
163	becomes zero, do not perform.
164	*/
165	int nFoundDependVars;
166	float averageFoundDependVars;
167
168	int nPrevEliminatedFwd;
169	int linearComputeRange;
170
171	boolean lazySiftFlag;
172	};
173
174
175	/Struct********************************************************************
176
177	Synopsis [This structure contains the information about a particular
178	cluster.]
179
180	Description [Corresponding to each cluster one ctrInfoStruct is created, The
181	various fields of this structure contain the information for
182	ordering the clusters for image computation
183	purposes. "varItemList" is the linked list of "varItemStruct"
184	corresponding to all the support variables of the cluster.]
185
186	******************************************************************************/
187	struct CtrInfoStruct {
188	int ctrId; /* Unique id of the cluster */
189	int numLocalSmoothVars; /*
190	* Number of smooth variables in the support of the
191	* cluster which can be quantified out if the cluster
192	* is multiplied in the current product.
193	*/
194	int numSmoothVars; /* Number of smooth variables in the support */
195	int numIntroducedVars; /*
196	* Number of range variables introduced if the cluster
197	* is multiplied in the current product.
198	*/
199	int maxSmoothVarIndex; /* Max. index of a smooth variable in the support */
200	int rankMaxSmoothVarIndex; /* Rank of maximum index amongst all ctr's */
201	lsList varItemList; /* List of varItemStruct of the support variables */
202	lsHandle ctrInfoListHandle; /*
203	* Handle to the list of info struct of ctr's
204	* which are yet to be ordered.
205	*/
206	};
207
208
209
210	/Struct********************************************************************
211
212	Synopsis [This structure contains information about a particular variable
213	(domain, range or quantify).]
214
215	Description [Corresponding to each variable a structure is created. Like the
216	varItemList field of ctrInfoStruct, ctrItemList contains the
217	list of ctrInfoStruct corresponding to various clusters which
218	depend on this variable.]
219
220	******************************************************************************/
221
222	struct VarInfoStruct {
223	int bddId; /* BDD id of the variable */
224	int numCtr; /* Number of components which depend on this variable. */
225	int varType; /* Domain, range or quantify variable ?*/
226	lsList ctrItemList; /* List of ctrItemStruct corresponding to the clusters
227	that depend on it */
228	};
229
230
231
232	/Struct********************************************************************
233
234	Synopsis [This structure is the wrapper around a particular variable which
235	is in the support of a particular cluster.]
236
237	Description [Every cluster has a linked list of varItemStruct's. Each of
238	these structs is a wrapper around varInfo. The "ctrItemStruct"
239	corresponding to the cluster itself is present in ctrItemList,
240	the linked list of varInfo. "ctrItemHandle" is the handle to
241	the ctrItemStruct in "ctrItemList" of varInfo.]
242
243	******************************************************************************/
244	struct VarItemStruct {
245	VarInfo_t varInfo; / The pointer to the corresponding variable info
246	* structure */
247	lsHandle ctrItemHandle; /*
248	* The list handle to the ctrItemStruct
249	* corresponding to the ctrInfo (the one which
250	* contains this varItem in the varItemList) in the
251	* ctrItemList field of the varInfo.
252	*/
253	};
254
255
256	/Struct********************************************************************
257
258	Synopsis [This structure is the wrapper around a particular ctr which
259	depend on a particular variable.]
260
261	Description [Every variable has a linked list of ctrItemStruct's. Each of
262	these structs is a wrapper around ctrInfo. The "varItemStruct"
263	corresponding to the variable itself is present in varItemList,
264	the linked list of ctrInfo. "varItemHandle" is the handle to
265	the varItemStruct in "varItemList" of ctrInfo.]
266
267	******************************************************************************/
268	struct CtrItemStruct {
269	CtrInfo_t ctrInfo; / Pointer to the corresponding cluster
270	* info structure. */
271	lsHandle varItemHandle; /*
272	* The list handle to the varItemStruct
273	* corresponding to the varInfo (the one which
274	* contains this ctrItem in the ctrItemList) in the
275	* varItemList field of the ctrInfo.
276	*/
277	};
278
279
280
281	/---------------------------------------------------------------------------/
282	/* Variable declarations */
283	/---------------------------------------------------------------------------/
284
285	static double *signatures;
286
287	/---------------------------------------------------------------------------/
288	/* Macro declarations */
289	/---------------------------------------------------------------------------/
290
291
292	/AutomaticStart***********************************************************/
293
294	/---------------------------------------------------------------------------/
295	/* Static function prototypes */
296	/---------------------------------------------------------------------------/
297
298	static void ResetClusteredCofactoredRelationArray(mdd_manager mddManager, Iwls95Info_t info);
299	static void FreeClusteredCofactoredRelationArray(Iwls95Info_t *info);
300	static ImgTrmOption_t * TrmGetOptions(void);
301	static void CreateBitRelationArray(Iwls95Info_t info, ImgFunctionData_t functionData);
302	static void FreeBitRelationArray(Iwls95Info_t *info);
303	static void OrderClusterOrder(mdd_manager mddManager, array_t relationArray, array_t fromVarBddArray, array_t toVarBddArray, array_t quantifyVarBddArray, array_t orderedClusteredRelationArrayPtr, array_t smoothVarBddArrayPtr, ImgTrmOption_t option, boolean freeRelationArray);
304	static array_t * CreateClusters(bdd_manager bddManager, array_t relationArray, ImgTrmOption_t *option);
305	static void OrderRelationArray(mdd_manager mddManager, array_t relationArray, array_t domainVarBddArray, array_t quantifyVarBddArray, array_t rangeVarBddArray, ImgTrmOption_t option, array_t orderedRelationArrayPtr, array_t arraySmoothVarBddArrayPtr);
306	static array_t * RelationArraySmoothLocalVars(array_t relationArray, array_t ctrInfoArray, array_t varInfoArray, st_table bddIdToBddTable);
307	static void OrderRelationArrayAux(array_t relationArray, lsList remainingCtrInfoList, array_t ctrInfoArray, array_t varInfoArray, int sortedMaxIndexVector, int numSmoothVarsRemaining, int numIntroducedVarsRemaining, st_table bddIdToBddTable, ImgTrmOption_t option, array_t domainAndQuantifyVarBddArray, array_t orderedRelationArrayPtr, array_t arraySmoothVarBddArrayPtr, array_t arrayDomainQuantifyVarsWithZeroNumCtr);
308	static array_t * UpdateInfoArrays(CtrInfo_t ctrInfo, st_table bddIdToBddTable, int numSmoothVarsRemainingPtr, int numIntroducedVarsRemainingPtr);
309	static float CalculateBenefit(CtrInfo_t ctrInfo, int maxNumLocalSmoothVars, int maxNumSmoothVars, int maxIndex, int maxNumIntroducedVars, ImgTrmOption_t option);
310	static void PrintOption(Img_MethodType method, ImgTrmOption_t option, FILE fp);
311	static Iwls95Info_t * Iwls95InfoStructAlloc(Img_MethodType method);
312	static CtrInfo_t * CtrInfoStructAlloc(void);
313	static void CtrInfoStructFree(CtrInfo_t *ctrInfo);
314	static VarInfo_t * VarInfoStructAlloc(void);
315	static void VarInfoStructFree(VarInfo_t *varInfo);
316	static void CtrItemStructFree(CtrItem_t *ctrItem);
317	static void VarItemStructFree(VarItem_t *varItem);
318	static int CtrInfoMaxIndexCompare(const void * p1, const void * p2);
319	static void PrintCtrInfoStruct(CtrInfo_t *ctrInfo);
320	static void PrintVarInfoStruct(VarInfo_t *varInfo);
321	static int CheckQuantificationSchedule(array_t relationArray, array_t arraySmoothVarBddArray);
322	static int CheckCtrInfoArray(array_t *ctrInfoArray, int numDomainVars, int numQuantifyVars, int numRangeVars);
323	static int CheckCtrInfo(CtrInfo_t *ctrInfo, int numDomainVars, int numQuantifyVars, int numRangeVars);
324	static int CheckVarInfoArray(array_t *varInfoArray, int numRelation);
325	static array_t * BddArrayDup(array_t *bddArray);
326	static array_t * BddArrayArrayDup(array_t *bddArray);
327	static mdd_t * BddLinearAndSmooth(mdd_manager mddManager, bdd_t fromSet, array_t relationArray, array_t arraySmoothVarBddArray, array_t smoothVarCubeArray, int verbosity, ImgPartialImageOption_t PIoption, boolean *partial, boolean lazySiftFlag);
328	static void HashIdToBddTable(st_table table, array_t idArray, array_t *bddArray);
329	static void PrintSmoothIntroducedCount(array_t clusterArray, array_t arraySmoothVarBddArrayPtr, array_t psBddIdArray, array_t *nsBddIdArray);
330	static void PrintBddIdFromBddArray(array_t *bddArray);
331	static void PrintBddIdTable(st_table *idTable);
332	static void PartitionTraverseRecursively(mdd_manager mddManager, vertex_t vertex, int mddId, st_table vertexTable, array_t relationArray, st_table domainQuantifyVarMddIdTable, array_t quantifyVarMddIdArray);
333	static void PrintPartitionRecursively(vertex_t vertex, st_table vertexTable, int indent);
334	static bdd_t * RecomputeImageIfNecessary(ImgFunctionData_t functionData, mdd_manager mddManager, bdd_t domainSubset, array_t relationArray, array_t arraySmoothVarBddArray, array_t smoothVarCubeArray, int verbosity, ImgPartialImageOption_t PIoption, array_t toCareSetArray, boolean *partial, boolean lazySiftFlag);
335	static bdd_t * ComputeSubsetOfIntermediateProduct(bdd_t product, ImgPartialImageOption_t PIoption);
336	static bdd_t * ComputeClippedAndAbstract(bdd_t product, bdd_t relation, array_t smoothVarBddArray, int nvars, int clippingDepth, boolean partial, int verbosity);
337	static array_t * CopyArrayBddArray(array_t *arrayBddArray);
338	static void PrintPartitionedTransitionRelation(mdd_manager mddManager, Iwls95Info_t info, Img_DirectionType directionType);
339	static void ReorderPartitionedTransitionRelation(Iwls95Info_t info, ImgFunctionData_t functionData, Img_DirectionType directionType);
340	static void UpdateQuantificationSchedule(Iwls95Info_t info, ImgFunctionData_t functionData, Img_DirectionType directionType);
341	static array_t * MakeSmoothVarCubeArray(mdd_manager mddManager, array_t arraySmoothVarBddArray);
342	static mdd_t * TrmEliminateDependVars(Img_ImageInfo_t imageInfo, array_t relationArray, mdd_t states, mdd_t *dependRelations);
343	static int TrmSignatureCompare(int ptrX, int ptrY);
344	static void SetupLazySifting(mdd_manager mddManager, array_t bddRelationArray, array_t domainVarBddArray, array_t quantifyVarBddArray, array_t *rangeVarBddArray, int verbosity);
345	static int MddSizeCompare(const void ptr1, const void ptr2);
346	/AutomaticEnd*************************************************************/
347
348
349	/---------------------------------------------------------------------------/
350	/* Definition of exported functions */
351	/---------------------------------------------------------------------------/
352
353
354	/Function******************************************************************
355
356	Synopsis [Returns the result after existentially quantifying a
357	set of variables after taking the product of the array of relations.]
358
359	Description ["relationArray" is an array of mdd's which need to be
360	multiplied and the variables in the "smoothVarMddIdArray" need to
361	be quantified out from the product. "introducedVarMddIdArray" is the
362	array of mddIds of the variables (other than the variables to be
363	quantified out) in the support of the relations. This array is used
364	to compute the product order such that the number of new variables
365	introduced in the product is minimized. However passing an empty
366	array or an array of mddIds of partial support will not result in any
367	error (some optimality will be lost though). The computation consists of 2
368	phases. In phase 1, an ordering of the relations and a schedule of
369	quantifying variables is found (based on IWLS95) heuristic. In phase
370	2, the relations are multiplied in order and the quantifying
371	variables are quantified according to the schedule.]
372
373	SideEffects [None]
374
375	******************************************************************************/
376	mdd_t*
377	Img_MultiwayLinearAndSmooth(mdd_manager mddManager, array_t relationArray,
378	array_t *smoothVarMddIdArray,
379	array_t *introducedVarMddIdArray,
380	Img_MethodType method,
381	Img_DirectionType direction)
382	{
383	mdd_t *product;
384	array_t *smoothVarBddArray = mdd_id_array_to_bdd_array(mddManager,
385	smoothVarMddIdArray);
386	array_t *introducedVarBddArray = mdd_id_array_to_bdd_array(mddManager,
387	introducedVarMddIdArray);
388
389	product = ImgMultiwayLinearAndSmooth(mddManager, relationArray,
390	smoothVarBddArray, introducedVarBddArray,
391	method, direction, NIL(ImgTrmOption_t));
392
393	mdd_array_free(introducedVarBddArray);
394	mdd_array_free(smoothVarBddArray);
395	return product;
396	}
397
398
399	/Function******************************************************************
400
401	Synopsis [Prints info of the partitioned transition relation.]
402
403	Description [Prints info of the partitioned transition relation.]
404
405	SideEffects []
406
407	******************************************************************************/
408	void
409	Img_PrintPartitionedTransitionRelation(mdd_manager *mddManager,
410	Img_ImageInfo_t *imageInfo,
411	Img_DirectionType directionType)
412	{
413	Iwls95Info_t info = (Iwls95Info_t ) imageInfo->methodData;
414
415	if (imageInfo->methodType != Img_Iwls95_c &&
416	imageInfo->methodType != Img_Mlp_c &&
417	imageInfo->methodType != Img_Linear_c)
418	return;
419
420	PrintPartitionedTransitionRelation(mddManager, info, directionType);
421	}
422
423
424	/Function******************************************************************
425
426	Synopsis [Reorder partitioned transition relation.]
427
428	Description [Reorder partitioned transition relation.]
429
430	SideEffects []
431
432	******************************************************************************/
433	void
434	Img_ReorderPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo,
435	Img_DirectionType directionType)
436	{
437	if (imageInfo->methodType != Img_Iwls95_c &&
438	imageInfo->methodType != Img_Mlp_c &&
439	imageInfo->methodType != Img_Linear_c)
440	return;
441
442	ReorderPartitionedTransitionRelation((Iwls95Info_t *)imageInfo->methodData,
443	&(imageInfo->functionData),
444	directionType);
445	}
446
447
448	/Function******************************************************************
449
450	Synopsis [Updates quantification schedule.]
451
452	Description [Updates quantification schedule.]
453
454	SideEffects []
455
456	******************************************************************************/
457	void
458	Img_UpdateQuantificationSchedule(Img_ImageInfo_t *imageInfo,
459	Img_DirectionType directionType)
460	{
461	if (imageInfo->methodType != Img_Iwls95_c)
462	return;
463
464	UpdateQuantificationSchedule((Iwls95Info_t *)imageInfo->methodData,
465	&(imageInfo->functionData), directionType);
466	}
467
468
469	/Function******************************************************************
470
471	Synopsis [Clusters relation array and returns quantification schedule.]
472
473	Description [Clusters relation array and returns quantification schedule.]
474
475	SideEffects []
476
477	******************************************************************************/
478	void
479	Img_ClusterRelationArray(mdd_manager *mddManager,
480	Img_MethodType method,
481	Img_DirectionType direction,
482	array_t *relationArray,
483	array_t *domainVarMddIdArray,
484	array_t *rangeVarMddIdArray,
485	array_t *quantifyVarMddIdArray,
486	array_t **clusteredRelationArray,
487	array_t **arraySmoothVarBddArray,
488	array_t **smoothVarCubeArray,
489	boolean freeRelationArray)
490	{
491	array_t *domainVarBddArray;
492	array_t *quantifyVarBddArray;
493	array_t *rangeVarBddArray;
494	ImgTrmOption_t *option;
495
496	option = TrmGetOptions();
497	domainVarBddArray = mdd_id_array_to_bdd_array(mddManager,
498	domainVarMddIdArray);
499	rangeVarBddArray = mdd_id_array_to_bdd_array(mddManager,
500	rangeVarMddIdArray);
501	quantifyVarBddArray = mdd_id_array_to_bdd_array(mddManager,
502	quantifyVarMddIdArray);
503
504	*clusteredRelationArray = ImgClusterRelationArray(mddManager,
505	NIL(ImgFunctionData_t),
506	method,
507	direction,
508	option,
509	relationArray,
510	domainVarBddArray,
511	quantifyVarBddArray,
512	rangeVarBddArray,
513	arraySmoothVarBddArray,
514	smoothVarCubeArray,
515	freeRelationArray);
516
517	ImgFreeTrmOptions(option);
518	mdd_array_free(domainVarBddArray);
519	mdd_array_free(rangeVarBddArray);
520	mdd_array_free(quantifyVarBddArray);
521	}
522
523
524	/---------------------------------------------------------------------------/
525	/* Definition of internal functions */
526	/---------------------------------------------------------------------------/
527
528
529	/Function******************************************************************
530
531	Synopsis [Returns the result after existentially quantifying a
532	set of variables after taking the product of the array of relations.]
533
534	Description ["relationArray" is an array of mdd's which need to be
535	multiplied and the variables in the "smoothVarBddArray" need to
536	be quantified out from the product. "introducedVarBddArray" is the
537	array of the bdd variables (other than the variables to be
538	quantified out) in the support of the relations. This array is used
539	to compute the product order such that the number of new variables
540	introduced in the product is minimized. However passing an empty
541	array or an array of mddIds of partial support will not result in any
542	error (some optimality will be lost though). The computation consists of 2
543	phases. In phase 1, an ordering of the relations and a schedule of
544	quantifying variables is found (based on IWLS95) heuristic. In phase
545	2, the relations are multiplied in order and the quantifying
546	variables are quantified according to the schedule.]
547
548	SideEffects [None]
549
550	******************************************************************************/
551	mdd_t*
552	ImgMultiwayLinearAndSmooth(mdd_manager *mddManager,
553	array_t *relationArray,
554	array_t *smoothVarBddArray,
555	array_t *introducedVarBddArray,
556	Img_MethodType method,
557	Img_DirectionType direction,
558	ImgTrmOption_t *option)
559	{
560	mdd_t *product;
561	array_t domainVarBddArray = array_alloc(bdd_t, 0);
562
563	product = ImgMultiwayLinearAndSmoothWithFrom(mddManager, relationArray,
564	NIL(mdd_t),
565	smoothVarBddArray,
566	domainVarBddArray,
567	introducedVarBddArray,
568	method, direction, option);
569
570	array_free(domainVarBddArray);
571	return product;
572	}
573
574
575	/Function******************************************************************
576
577	Synopsis [Returns the result after existentially quantifying a
578	set of variables after taking the product of the array of relations.]
579
580	Description ["relationArray" is an array of mdd's which need to be
581	multiplied and the variables in the "smoothVarBddArray" need to
582	be quantified out from the product. "introducedVarBddArray" is the
583	array of the bdd variables (other than the variables to be
584	quantified out) in the support of the relations. This array is used
585	to compute the product order such that the number of new variables
586	introduced in the product is minimized. However passing an empty
587	array or an array of mddIds of partial support will not result in any
588	error (some optimality will be lost though). The computation consists of 2
589	phases. In phase 1, an ordering of the relations and a schedule of
590	quantifying variables is found (based on IWLS95) heuristic. In phase
591	2, the relations are multiplied in order and the quantifying
592	variables are quantified according to the schedule. If "from" is not nil,
593	we first order "relationArray" and make quantification schedule, then
594	we multiply with "from". In this case, "domainVarBddArray" should contain
595	the state variables to be quantified out. If "from" is nil, then
596	"domainVarBddArray" should be an empty array.]
597
598	SideEffects [None]
599
600	******************************************************************************/
601	mdd_t*
602	ImgMultiwayLinearAndSmoothWithFrom(mdd_manager *mddManager,
603	array_t *relationArray,
604	mdd_t *from,
605	array_t *smoothVarBddArray,
606	array_t *domainVarBddArray,
607	array_t *introducedVarBddArray,
608	Img_MethodType method,
609	Img_DirectionType direction,
610	ImgTrmOption_t *option)
611	{
612	mdd_t *product;
613	boolean partial = FALSE;
614	array_t *orderedRelationArray = NIL(array_t);
615	array_t *arraySmoothVarBddArray = NIL(array_t);
616	int freeOptionFlag;
617	int lazySiftFlag = bdd_is_lazy_sift(mddManager);
618
619	if (!option) {
620	option = TrmGetOptions();
621	freeOptionFlag = 1;
622	} else
623	freeOptionFlag = 0;
624
625	if (method == Img_Iwls95_c) {
626	OrderRelationArray(mddManager, relationArray, domainVarBddArray,
627	smoothVarBddArray, introducedVarBddArray, option,
628	&orderedRelationArray, &arraySmoothVarBddArray);
629	} else if (method == Img_Mlp_c) {
630	if (direction == Img_Forward_c) {
631	/*
632	* domainVarBddArray : PS
633	* introducedVarBddArray : NS
634	*/
635	if (option->mlpMultiway && from == NIL(mdd_t)) {
636	product = ImgMlpMultiwayAndSmooth(mddManager, NIL(ImgFunctionData_t),
637	relationArray, domainVarBddArray,
638	smoothVarBddArray,
639	introducedVarBddArray, direction,
640	option);
641	array_free(domainVarBddArray);
642	if (freeOptionFlag)
643	ImgFreeTrmOptions(option);
644	return product;
645	} else {
646	ImgMlpOrderRelationArray(mddManager, relationArray, domainVarBddArray,
647	smoothVarBddArray, introducedVarBddArray,
648	direction, &orderedRelationArray,
649	&arraySmoothVarBddArray, option);
650	}
651	} else { /* direction == Img_Backward_c */
652	/*
653	* domainVarBddArray : NS
654	* introducedVarBddArray : PS
655	*/
656	if (option->mlpPreSwapStateVars) {
657	if (option->mlpMultiway && from == NIL(mdd_t)) {
658	product = ImgMlpMultiwayAndSmooth(mddManager, NIL(ImgFunctionData_t),
659	relationArray,
660	domainVarBddArray,
661	smoothVarBddArray,
662	introducedVarBddArray,
663	Img_Forward_c, option);
664	array_free(domainVarBddArray);
665	if (freeOptionFlag)
666	ImgFreeTrmOptions(option);
667	return product;
668	} else {
669	ImgMlpOrderRelationArray(mddManager, relationArray,
670	domainVarBddArray, smoothVarBddArray,
671	introducedVarBddArray,
672	Img_Forward_c, &orderedRelationArray,
673	&arraySmoothVarBddArray, option);
674	}
675	} else {
676	if (option->mlpMultiway && from == NIL(mdd_t)) {
677	product = ImgMlpMultiwayAndSmooth(mddManager, NIL(ImgFunctionData_t),
678	relationArray, domainVarBddArray,
679	smoothVarBddArray,
680	introducedVarBddArray,
681	Img_Backward_c, option);
682	array_free(domainVarBddArray);
683	if (freeOptionFlag)
684	ImgFreeTrmOptions(option);
685	return product;
686	} else {
687	ImgMlpOrderRelationArray(mddManager, relationArray,
688	domainVarBddArray, smoothVarBddArray,
689	introducedVarBddArray,
690	Img_Backward_c, &orderedRelationArray,
691	&arraySmoothVarBddArray, option);
692	}
693	}
694	}
695	} else
696	assert(0);
697
698	product = BddLinearAndSmooth(mddManager, from,
699	orderedRelationArray,
700	arraySmoothVarBddArray,
701	NIL(array_t),
702	option->verbosity,
703	NULL, &partial, lazySiftFlag);
704
705	if (freeOptionFlag)
706	ImgFreeTrmOptions(option);
707	mdd_array_free(orderedRelationArray);
708	mdd_array_array_free(arraySmoothVarBddArray);
709	return product;
710	}
711
712
713	/Function******************************************************************
714
715	Synopsis [Returns a BDD after taking the product of fromSet with the
716	BDDs in the relationArray and quantifying out the variables using
717	the schedule given in the arraySmoothVarBddArray.]
718
719	Description [The product is taken from the left, i.e., fromSet is
720	multiplied with relationArray[0]. The array of variables given by
721	arraySmoothVarBddArray[i] are quantified when the relationArray[i]
722	is multiplied in the product.]
723
724	SideEffects [None]
725
726	******************************************************************************/
727	mdd_t*
728	ImgBddLinearAndSmooth(mdd_manager *mddManager,
729	mdd_t *from,
730	array_t *relationArray,
731	array_t *arraySmoothVarBddArray,
732	array_t *smoothVarCubeArray,
733	int verbosity)
734	{
735	mdd_t *product;
736	boolean partial = FALSE;
737	int lazySiftFlag = bdd_is_lazy_sift(mddManager);
738
739	product = BddLinearAndSmooth(mddManager, from,
740	relationArray,
741	arraySmoothVarBddArray,
742	smoothVarCubeArray,
743	verbosity,
744	NULL, &partial, lazySiftFlag);
745
746	return product;
747	}
748
749
750	/Function******************************************************************
751
752	Synopsis [Clusters relation array and makes quantification schedule.]
753
754	Description [Orders and clusters relation array and makes quantification
755	schedule. (Order/Cluster/Order.)]
756
757	SideEffects []
758
759	******************************************************************************/
760	array_t *
761	ImgClusterRelationArray(mdd_manager *mddManager,
762	ImgFunctionData_t *functionData,
763	Img_MethodType method,
764	Img_DirectionType direction,
765	ImgTrmOption_t *option,
766	array_t *relationArray,
767	array_t *domainVarBddArray,
768	array_t *quantifyVarBddArray,
769	array_t *rangeVarBddArray,
770	array_t **arraySmoothVarBddArray,
771	array_t **smoothVarCubeArray,
772	boolean freeRelationArray)
773	{
774	array_t *orderedRelationArray;
775	array_t *clusteredRelationArray;
776	int freeOptionFlag;
777	long initialTime, finalTime;
778
779	if (!option) {
780	option = TrmGetOptions();
781	freeOptionFlag = 1;
782	} else
783	freeOptionFlag = 0;
784
785	if (option->verbosity >= 2)
786	initialTime = util_cpu_time();
787	else /* to remove uninitialized variables warning */
788	initialTime = 0;
789
790	if (method == Img_Iwls95_c) {
791	assert(direction != Img_Both_c);
792	if (direction == Img_Forward_c) {
793	OrderClusterOrder(mddManager, relationArray, domainVarBddArray,
794	rangeVarBddArray, quantifyVarBddArray,
795	&orderedRelationArray, arraySmoothVarBddArray,
796	option, freeRelationArray);
797	} else {
798	assert(direction == Img_Backward_c);
799	OrderClusterOrder(mddManager, relationArray, rangeVarBddArray,
800	domainVarBddArray, quantifyVarBddArray,
801	&orderedRelationArray, arraySmoothVarBddArray,
802	option, freeRelationArray);
803
804	}
805	if (freeOptionFlag)
806	ImgFreeTrmOptions(option);
807
808	if (smoothVarCubeArray) {
809	if (functionData->createVarCubesFlag) {
810	*smoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
811	*arraySmoothVarBddArray);
812	} else
813	*smoothVarCubeArray = NIL(array_t);
814	}
815	if (option->verbosity >= 2) {
816	finalTime = util_cpu_time();
817	fprintf(vis_stdout, "time for clustering with IWLS95 = %10g\n",
818	(double)(finalTime - initialTime) / 1000.0);
819	}
820	return(orderedRelationArray);
821	} else if (method == Img_Mlp_c) {
822	if ((direction == Img_Forward_c && option->mlpReorder == 2) \|\|
823	(direction == Img_Backward_c && option->mlpPreReorder == 2)) {
824	if (direction == Img_Forward_c)
825	option->mlpReorder = 0;
826	else
827	option->mlpPreReorder = 0;
828	ImgMlpClusterRelationArray(mddManager, functionData, relationArray,
829	domainVarBddArray, quantifyVarBddArray, rangeVarBddArray,
830	direction, &clusteredRelationArray, NIL(array_t *), option);
831	if (direction == Img_Forward_c)
832	option->mlpReorder = 2;
833	else
834	option->mlpPreReorder = 2;
835	ImgMlpOrderRelationArray(mddManager, clusteredRelationArray,
836	domainVarBddArray, quantifyVarBddArray, rangeVarBddArray,
837	direction, &orderedRelationArray, arraySmoothVarBddArray,
838	option);
839	mdd_array_free(clusteredRelationArray);
840	} else if ((direction == Img_Forward_c && option->mlpReorder == 3) \|\|
841	(direction == Img_Backward_c && option->mlpPreReorder == 3)) {
842	if (direction == Img_Forward_c)
843	option->mlpReorder = 0;
844	else
845	option->mlpPreReorder = 0;
846	ImgMlpClusterRelationArray(mddManager, functionData, relationArray,
847	domainVarBddArray, quantifyVarBddArray, rangeVarBddArray,
848	direction, &clusteredRelationArray, NIL(array_t *), option);
849	if (direction == Img_Forward_c)
850	option->mlpReorder = 3;
851	else
852	option->mlpPreReorder = 3;
853	OrderRelationArray(mddManager, clusteredRelationArray,
854	domainVarBddArray, quantifyVarBddArray,
855	rangeVarBddArray, option,
856	&orderedRelationArray, arraySmoothVarBddArray);
857	mdd_array_free(clusteredRelationArray);
858	} else {
859	ImgMlpClusterRelationArray(mddManager, functionData, relationArray,
860	domainVarBddArray, quantifyVarBddArray, rangeVarBddArray,
861	direction, &orderedRelationArray, arraySmoothVarBddArray,
862	option);
863	}
864	if (freeOptionFlag)
865	ImgFreeTrmOptions(option);
866	if (smoothVarCubeArray) {
867	if (functionData->createVarCubesFlag) {
868	*smoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
869	*arraySmoothVarBddArray);
870	} else
871	*smoothVarCubeArray = NIL(array_t);
872	}
873	if (option->verbosity >= 2) {
874	finalTime = util_cpu_time();
875	fprintf(vis_stdout, "time for clustering with MLP = %10g\n",
876	(double)(finalTime - initialTime) / 1000.0);
877	}
878	return(orderedRelationArray);
879	} else
880	assert(0);
881	return NIL(array_t); /* we should never get here */
882	}
883
884
885	/Function******************************************************************
886
887	Synopsis [Returns quantification schedule for a given relation array.]
888
889	Description [Returns quantification schedule for a given relation array.]
890
891	SideEffects []
892
893	******************************************************************************/
894	array_t *
895	ImgGetQuantificationSchedule(mdd_manager *mddManager,
896	ImgFunctionData_t *functionData,
897	Img_MethodType method,
898	Img_DirectionType direction,
899	ImgTrmOption_t *option,
900	array_t *relationArray,
901	array_t *smoothVarBddArray,
902	array_t *domainVarBddArray,
903	array_t *introducedVarBddArray,
904	boolean withClustering,
905	array_t **orderedRelationArrayPtr)
906	{
907	array_t *orderedRelationArray = NIL(array_t);
908	array_t *clusteredRelationArray;
909	array_t *arraySmoothVarBddArray = NIL(array_t);
910	int freeOptionFlag;
911
912	if (!option) {
913	option = TrmGetOptions();
914	freeOptionFlag = 1;
915	} else
916	freeOptionFlag = 0;
917
918	if (method == Img_Iwls95_c) {
919	if (withClustering) {
920	OrderRelationArray(mddManager, relationArray, domainVarBddArray,
921	smoothVarBddArray, introducedVarBddArray, option,
922	&orderedRelationArray, NIL(array_t *));
923
924	clusteredRelationArray = CreateClusters(mddManager, orderedRelationArray,
925	option);
926	mdd_array_free(orderedRelationArray);
927
928	OrderRelationArray(mddManager, clusteredRelationArray, domainVarBddArray,
929	smoothVarBddArray, introducedVarBddArray, option,
930	&orderedRelationArray, &arraySmoothVarBddArray);
931	mdd_array_free(clusteredRelationArray);
932	} else {
933	OrderRelationArray(mddManager, relationArray, domainVarBddArray,
934	smoothVarBddArray, introducedVarBddArray, option,
935	&orderedRelationArray, &arraySmoothVarBddArray);
936	}
937	} else if (method == Img_Mlp_c) {
938	if (withClustering) {
939	ImgMlpClusterRelationArray(mddManager, functionData, relationArray,
940	domainVarBddArray, smoothVarBddArray, introducedVarBddArray,
941	direction, &orderedRelationArray, &arraySmoothVarBddArray,
942	option);
943	} else {
944	ImgMlpOrderRelationArray(mddManager, relationArray, domainVarBddArray,
945	smoothVarBddArray, introducedVarBddArray, direction,
946	&orderedRelationArray, &arraySmoothVarBddArray,
947	option);
948	}
949	} else
950	assert(0);
951
952	if (freeOptionFlag)
953	ImgFreeTrmOptions(option);
954	if (orderedRelationArrayPtr)
955	*orderedRelationArrayPtr = orderedRelationArray;
956	else
957	mdd_array_free(orderedRelationArray);
958	return(arraySmoothVarBddArray);
959	}
960
961
962	/Function******************************************************************
963
964	Synopsis [Allocates an option structure for transition relation method.]
965
966	Description [Allocates an option structure for transition relation method.]
967
968	SideEffects []
969
970	******************************************************************************/
971	ImgTrmOption_t *
972	ImgGetTrmOptions(void)
973	{
974	ImgTrmOption_t *option;
975
976	option = TrmGetOptions();
977	return(option);
978	}
979
980
981	/Function******************************************************************
982
983	Synopsis [Frees the option structure for transition relation method.]
984
985	Description [Frees the option structure for transition relation method.]
986
987	SideEffects []
988
989	******************************************************************************/
990	void
991	ImgFreeTrmOptions(ImgTrmOption_t *option)
992	{
993	if (option->readCluster)
994	FREE(option->readCluster);
995	if (option->writeCluster)
996	FREE(option->writeCluster);
997	if (option->writeDepMatrix)
998	FREE(option->writeDepMatrix);
999	FREE(option);
1000	}
1001
1002
1003	/Function******************************************************************
1004
1005	Synopsis [Turn off option to apply linear based image computation by comsidering range of state variables]
1006
1007	Description [ Turn off option to apply linear based image computation by comsidering range of state variables.]
1008
1009	SideEffects []
1010
1011	SeeAlso [ImgImageInfoFreeIwls95]
1012	******************************************************************************/
1013
1014	void
1015	ImgResetMethodDataLinearComputeRange(void *methodData)
1016	{
1017	Iwls95Info_t info = (Iwls95Info_t ) methodData;
1018	info->linearComputeRange = 0;
1019	}
1020
1021	/Function******************************************************************
1022
1023	Synopsis [Turn on option to apply linear based image computation by comsidering range of state variables]
1024
1025	Description [ Turn on option to apply linear based image computation by comsidering range of state variables.]
1026
1027	SideEffects []
1028
1029	SeeAlso []
1030	******************************************************************************/
1031	void
1032	ImgSetMethodDataLinearComputeRange(void *methodData)
1033	{
1034	Iwls95Info_t info = (Iwls95Info_t ) methodData;
1035	info->linearComputeRange = 1;
1036	}
1037
1038	/Function******************************************************************
1039
1040	Synopsis [Get unreachable states]
1041
1042	Description [Return unreachable states]
1043
1044	SideEffects []
1045
1046	SeeAlso []
1047	******************************************************************************/
1048	mdd_t *
1049	Img_ImageGetUnreachableStates(Img_ImageInfo_t * imageInfo)
1050	{
1051	array_t *relationArray;
1052	mdd_t *states;
1053	Iwls95Info_t info = (Iwls95Info_t ) imageInfo->methodData;
1054
1055	relationArray = info->fwdOptClusteredRelationArray;
1056	states = array_fetch(mdd_t *, relationArray, 0);
1057	states = ImgSubstitute(states, &(imageInfo->functionData), Img_R2D_c);
1058	return(states);
1059	}
1060
1061
1062	/Function******************************************************************
1063
1064	Synopsis [Initializes an image data structure for image
1065	computation using the Iwls95 technique.]
1066
1067	Description [This process consists of following steps.
1068	1. The transition functions are built.
1069	2. An array of bit level relations are built using the function
1070	mdd_fn_array_to_bdd_rel_array.
1071	3. The relations are clustered using the threshold value.
1072	4. The clustered relations are ordered.]
1073
1074	SideEffects []
1075
1076	SeeAlso [ImgImageInfoFreeIwls95]
1077	******************************************************************************/
1078
1079
1080	void *
1081	ImgImageInfoInitializeIwls95(void *methodData,
1082	ImgFunctionData_t *functionData,
1083	Img_DirectionType directionType,
1084	Img_MethodType method)
1085	{
1086	array_t *fwdClusteredRelationArray;
1087	array_t *bwdClusteredRelationArray;
1088	Iwls95Info_t info = (Iwls95Info_t ) methodData;
1089	Ntk_Network_t *network;
1090	Ntk_Node_t *node;
1091	char *flagValue;
1092	int i, mddId ;
1093
1094	if (info &&
1095	(((info->fwdClusteredRelationArray) &&
1096	(info->bwdClusteredRelationArray)) \|\|
1097	((directionType == Img_Forward_c) &&
1098	(info->fwdClusteredRelationArray)) \|\|
1099	((directionType == Img_Backward_c) &&
1100	(info->bwdClusteredRelationArray)))) {
1101	/* Nothing needs to be done. Return */
1102	return (void *) info;
1103	}
1104	else{
1105	array_t rangeVarBddArray, domainVarBddArray, *quantifyVarBddArray;
1106	array_t *newQuantifyVarMddIdArray;
1107	array_t *clusteredRelationArray;
1108	FILE fin, fout;
1109	array_t bddRelationArray, quantifyVarMddIdArray;
1110	mdd_manager *mddManager = Part_PartitionReadMddManager(functionData->mddNetwork);
1111
1112	if (info == NIL(Iwls95Info_t)) {
1113	info = Iwls95InfoStructAlloc(method);
1114	}
1115	CreateBitRelationArray(info, functionData);
1116
1117	/ if FAFWFlag then remove PI from quantifyVarMddIdArray /
1118	bddRelationArray = info->bitRelationArray;
1119	quantifyVarMddIdArray = info->quantifyVarMddIdArray;
1120	if(functionData->FAFWFlag) {
1121	network = functionData->network;
1122	newQuantifyVarMddIdArray = array_alloc(int, 0);
1123	for(i=0; i<array_n(quantifyVarMddIdArray); i++) {
1124	mddId = array_fetch(int, quantifyVarMddIdArray, i);
1125	node = Ntk_NetworkFindNodeByMddId(network, mddId);
1126	if(!Ntk_NodeTestIsInput(node)) {
1127	array_insert_last(int, newQuantifyVarMddIdArray, mddId);
1128	}
1129	}
1130	array_free(quantifyVarMddIdArray);
1131	quantifyVarMddIdArray = newQuantifyVarMddIdArray;
1132	info->quantifyVarMddIdArray = newQuantifyVarMddIdArray;
1133	}
1134
1135	info->bitRelationArray = NIL(array_t);
1136	info->quantifyVarMddIdArray = NIL(array_t);
1137
1138	rangeVarBddArray = functionData->rangeBddVars;
1139	domainVarBddArray = functionData->domainBddVars;
1140	quantifyVarBddArray = mdd_id_array_to_bdd_array(mddManager,
1141	quantifyVarMddIdArray);
1142
1143	array_free(quantifyVarMddIdArray);
1144
1145	if (((directionType == Img_Forward_c) \|\|
1146	(directionType == Img_Both_c)) &&
1147	(info->fwdClusteredRelationArray == NIL(array_t))) {
1148	if (info->option->readCluster) {
1149	if (info->option->readReorderCluster) {
1150	fin = fopen(info->option->readCluster, "r");
1151	ImgMlpReadClusterFile(fin, mddManager,
1152	functionData, bddRelationArray,
1153	domainVarBddArray, rangeVarBddArray,
1154	quantifyVarBddArray, Img_Forward_c,
1155	&clusteredRelationArray, NIL(array_t *),
1156	info->option);
1157	fclose(fin);
1158	if (method == Img_Iwls95_c) {
1159	OrderRelationArray(mddManager, clusteredRelationArray,
1160	domainVarBddArray, quantifyVarBddArray,
1161	rangeVarBddArray, info->option,
1162	&info->fwdClusteredRelationArray,
1163	&info->fwdArraySmoothVarBddArray);
1164	} else if (method == Img_Mlp_c) {
1165	ImgMlpOrderRelationArray(mddManager, clusteredRelationArray,
1166	domainVarBddArray, quantifyVarBddArray,
1167	rangeVarBddArray, Img_Forward_c,
1168	&info->fwdClusteredRelationArray,
1169	&info->fwdArraySmoothVarBddArray,
1170	info->option);
1171	} else
1172	assert(0);
1173	mdd_array_free(clusteredRelationArray);
1174	} else {
1175	fin = fopen(info->option->readCluster, "r");
1176	ImgMlpReadClusterFile(fin, mddManager,
1177	functionData, bddRelationArray,
1178	domainVarBddArray, rangeVarBddArray,
1179	quantifyVarBddArray, Img_Forward_c,
1180	&info->fwdClusteredRelationArray,
1181	&info->fwdArraySmoothVarBddArray,
1182	info->option);
1183	fclose(fin);
1184	}
1185	} else if (method == Img_Iwls95_c) {
1186	/*
1187	* Since clusters are formed by multiplying the latches starting
1188	* from one end we need to order the latches using some heuristics
1189	* first. Right now, we order the latches using the same heuristic
1190	* as the one used for ordering the clusters for early quantifiction.
1191	* However, since we are not interested in the quantification
1192	* schedule at this stage, we will pass a NIL(array_t*) as the last
1193	* argument.
1194	*/
1195	OrderClusterOrder(mddManager, bddRelationArray, domainVarBddArray,
1196	rangeVarBddArray, quantifyVarBddArray,
1197	&info->fwdClusteredRelationArray,
1198	&info->fwdArraySmoothVarBddArray,
1199	info->option, 0);
1200	} else if (method == Img_Mlp_c) {
1201	if (info->option->mlpReorder == 2) {
1202	info->option->mlpReorder = 0;
1203	ImgMlpClusterRelationArray(mddManager, functionData,
1204	bddRelationArray, domainVarBddArray,
1205	quantifyVarBddArray, rangeVarBddArray,
1206	Img_Forward_c, &clusteredRelationArray,
1207	NIL(array_t *), info->option);
1208	info->option->mlpReorder = 2;
1209	ImgMlpOrderRelationArray(mddManager, clusteredRelationArray,
1210	domainVarBddArray, quantifyVarBddArray,
1211	rangeVarBddArray, Img_Forward_c,
1212	&info->fwdClusteredRelationArray,
1213	&info->fwdArraySmoothVarBddArray, info->option);
1214	mdd_array_free(clusteredRelationArray);
1215	} else if (info->option->mlpReorder == 3) {
1216	info->option->mlpReorder = 0;
1217	ImgMlpClusterRelationArray(mddManager, functionData,
1218	bddRelationArray, domainVarBddArray,
1219	quantifyVarBddArray, rangeVarBddArray,
1220	Img_Forward_c, &clusteredRelationArray,
1221	NIL(array_t *), info->option);
1222	info->option->mlpReorder = 3;
1223	OrderRelationArray(mddManager, clusteredRelationArray,
1224	domainVarBddArray, quantifyVarBddArray,
1225	rangeVarBddArray, info->option,
1226	&info->fwdClusteredRelationArray,
1227	&info->fwdArraySmoothVarBddArray);
1228	mdd_array_free(clusteredRelationArray);
1229	} else {
1230	ImgMlpClusterRelationArray(mddManager, functionData,
1231	bddRelationArray, domainVarBddArray,
1232	quantifyVarBddArray, rangeVarBddArray,
1233	Img_Forward_c, &info->fwdClusteredRelationArray,
1234	&info->fwdArraySmoothVarBddArray, info->option);
1235	}
1236	} else if (method == Img_Linear_c \|\| method == Img_Linear_Range_c) {
1237	if(method == Img_Linear_Range_c) {
1238	info->option->linearComputeRange = 1;
1239	method = Img_Linear_c;
1240	}
1241	ImgLinearClusterRelationArray(mddManager, functionData,
1242	bddRelationArray,
1243	Img_Forward_c,
1244	&info->fwdClusteredRelationArray,
1245	&info->fwdArraySmoothVarBddArray,
1246	&info->fwdOptClusteredRelationArray,
1247	&info->fwdOptArraySmoothVarBddArray,
1248	info->option);
1249	} else
1250	assert(0);
1251
1252	if (info->option->verbosity > 2)
1253	PrintPartitionedTransitionRelation(mddManager, info, Img_Forward_c);
1254	if(method == Img_Linear_c)
1255	ImgPrintPartitionedTransitionRelation(mddManager,
1256	info->fwdOptClusteredRelationArray ,
1257	info->fwdOptArraySmoothVarBddArray);
1258
1259	if (info->option->printDepMatrix \|\| info->option->writeDepMatrix) {
1260	if (info->option->writeDepMatrix) {
1261	fout = fopen(info->option->writeDepMatrix, "w");
1262	if (!fout) {
1263	fprintf(vis_stderr, "** img error: can't open file [%s]\n",
1264	info->option->writeDepMatrix);
1265	}
1266	} else
1267	fout = NIL(FILE);
1268	ImgMlpPrintDependenceMatrix(mddManager,
1269	info->fwdClusteredRelationArray,
1270	domainVarBddArray, quantifyVarBddArray, rangeVarBddArray,
1271	Img_Forward_c, info->option->printDepMatrix, fout,
1272	info->option);
1273	if (fout)
1274	fclose(fout);
1275	}
1276	if (info->option->writeCluster) {
1277	fout = fopen(info->option->writeCluster, "w");
1278	ImgMlpWriteClusterFile(fout, mddManager,
1279	info->fwdClusteredRelationArray,
1280	domainVarBddArray, rangeVarBddArray);
1281	fclose(fout);
1282	}
1283
1284	if (functionData->createVarCubesFlag && info->fwdArraySmoothVarBddArray)
1285	info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
1286	info->fwdArraySmoothVarBddArray);
1287	else
1288	info->fwdSmoothVarCubeArray = NIL(array_t);
1289
1290	if (functionData->createVarCubesFlag && info->fwdOptArraySmoothVarBddArray)
1291	info->fwdOptSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
1292	info->fwdOptArraySmoothVarBddArray);
1293	else
1294	info->fwdOptSmoothVarCubeArray = NIL(array_t);
1295
1296	#ifndef NDEBUG
1297	if(info->fwdClusteredRelationArray)
1298	assert(CheckQuantificationSchedule(info->fwdClusteredRelationArray,
1299	info->fwdArraySmoothVarBddArray));
1300	if(info->fwdOptClusteredRelationArray)
1301	assert(CheckQuantificationSchedule(info->fwdOptClusteredRelationArray,
1302	info->fwdOptArraySmoothVarBddArray));
1303	#endif
1304	}
1305
1306	if (((directionType == Img_Backward_c) \|\|
1307	(directionType == Img_Both_c)) &&
1308	(info->bwdClusteredRelationArray == NIL(array_t))) {
1309	if (info->option->readCluster) {
1310	if (info->option->readReorderCluster) {
1311	fin = fopen(info->option->readCluster, "r");
1312	ImgMlpReadClusterFile(fin, mddManager,
1313	functionData, bddRelationArray,
1314	domainVarBddArray, rangeVarBddArray,
1315	quantifyVarBddArray, Img_Backward_c,
1316	&clusteredRelationArray, NIL(array_t *),
1317	info->option);
1318	fclose(fin);
1319	if (method == Img_Iwls95_c) {
1320	OrderRelationArray(mddManager, clusteredRelationArray,
1321	rangeVarBddArray, quantifyVarBddArray,
1322	domainVarBddArray, info->option,
1323	&info->bwdClusteredRelationArray,
1324	&info->bwdArraySmoothVarBddArray);
1325	} else if (method == Img_Mlp_c) {
1326	ImgMlpOrderRelationArray(mddManager, clusteredRelationArray,
1327	domainVarBddArray, quantifyVarBddArray,
1328	rangeVarBddArray, Img_Backward_c,
1329	&info->bwdClusteredRelationArray,
1330	&info->bwdArraySmoothVarBddArray,
1331	info->option);
1332	} else
1333	assert(0);
1334	mdd_array_free(clusteredRelationArray);
1335	} else {
1336	fin = fopen(info->option->readCluster, "r");
1337	ImgMlpReadClusterFile(fin, mddManager,
1338	functionData, bddRelationArray,
1339	domainVarBddArray, rangeVarBddArray,
1340	quantifyVarBddArray, Img_Backward_c,
1341	&info->bwdClusteredRelationArray,
1342	&info->bwdArraySmoothVarBddArray,
1343	info->option);
1344	fclose(fin);
1345	}
1346	} else if (method == Img_Iwls95_c) {
1347	/*
1348	* Since clusters are formed by multiplying the latches starting
1349	* from one end we need to order the latches using some heuristics
1350	* first. Right now, we order the latches using the same heuristic
1351	* as the one used for ordering the clusters for early quantifiction.
1352	* However, since we are not interested in the quantification
1353	* schedule at this stage, we will pass a NIL(array_t*) as the last
1354	* argument.
1355	*/
1356	OrderClusterOrder(mddManager, bddRelationArray, rangeVarBddArray,
1357	domainVarBddArray, quantifyVarBddArray,
1358	&info->bwdClusteredRelationArray,
1359	&info->bwdArraySmoothVarBddArray,
1360	info->option, 0);
1361	} else if (method == Img_Mlp_c) {
1362	if (info->option->mlpPreReorder == 2) {
1363	info->option->mlpPreReorder = 0;
1364	ImgMlpClusterRelationArray(mddManager, functionData,
1365	bddRelationArray, domainVarBddArray,
1366	quantifyVarBddArray, rangeVarBddArray,
1367	Img_Backward_c, &clusteredRelationArray,
1368	NIL(array_t *), info->option);
1369	info->option->mlpPreReorder = 2;
1370	ImgMlpOrderRelationArray(mddManager, clusteredRelationArray,
1371	domainVarBddArray, quantifyVarBddArray,
1372	rangeVarBddArray, Img_Backward_c,
1373	&info->bwdClusteredRelationArray,
1374	&info->bwdArraySmoothVarBddArray, info->option);
1375	mdd_array_free(clusteredRelationArray);
1376	} else if (info->option->mlpPreReorder == 3) {
1377	info->option->mlpPreReorder = 0;
1378	ImgMlpClusterRelationArray(mddManager, functionData,
1379	bddRelationArray, domainVarBddArray,
1380	quantifyVarBddArray, rangeVarBddArray,
1381	Img_Backward_c, &clusteredRelationArray,
1382	NIL(array_t *), info->option);
1383	info->option->mlpPreReorder = 3;
1384	OrderRelationArray(mddManager, clusteredRelationArray,
1385	domainVarBddArray, quantifyVarBddArray,
1386	rangeVarBddArray, info->option,
1387	&info->bwdClusteredRelationArray,
1388	&info->bwdArraySmoothVarBddArray);
1389	mdd_array_free(clusteredRelationArray);
1390	} else {
1391	ImgMlpClusterRelationArray(mddManager, functionData,
1392	bddRelationArray, domainVarBddArray,
1393	quantifyVarBddArray, rangeVarBddArray,
1394	Img_Backward_c, &info->bwdClusteredRelationArray,
1395	&info->bwdArraySmoothVarBddArray, info->option);
1396	}
1397	} else
1398	assert(0);
1399
1400	info->careSetArray = NIL(array_t);
1401	info->bwdClusteredCofactoredRelationArray = NIL(array_t);
1402
1403	if (info->option->verbosity > 2)
1404	PrintPartitionedTransitionRelation(mddManager, info, Img_Backward_c);
1405
1406	if (info->option->printDepMatrix \|\| info->option->writeDepMatrix) {
1407	if (info->option->writeDepMatrix) {
1408	fout = fopen(info->option->writeDepMatrix, "w");
1409	if (!fout) {
1410	fprintf(vis_stderr, "** img error: can't open file [%s]\n",
1411	info->option->writeDepMatrix);
1412	}
1413	} else
1414	fout = NIL(FILE);
1415	ImgMlpPrintDependenceMatrix(mddManager,
1416	info->bwdClusteredRelationArray,
1417	domainVarBddArray, quantifyVarBddArray, rangeVarBddArray,
1418	Img_Backward_c, info->option->printDepMatrix, fout,
1419	info->option);
1420
1421	if (fout)
1422	fclose(fout);
1423	}
1424	if (info->option->writeCluster) {
1425	fout = fopen(info->option->writeCluster, "w");
1426	ImgMlpWriteClusterFile(fout, mddManager,
1427	info->bwdClusteredRelationArray,
1428	domainVarBddArray, rangeVarBddArray);
1429	fclose(fout);
1430	}
1431
1432	if (functionData->createVarCubesFlag)
1433	info->bwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
1434	info->bwdArraySmoothVarBddArray);
1435	else
1436	info->bwdSmoothVarCubeArray = NIL(array_t);
1437
1438	#ifndef NDEBUG
1439	assert(CheckQuantificationSchedule(info->bwdClusteredRelationArray,
1440	info->bwdArraySmoothVarBddArray));
1441	#endif
1442	}
1443
1444
1445	info->lazySiftFlag = bdd_is_lazy_sift(mddManager);
1446	if (info->lazySiftFlag) {
1447	SetupLazySifting(mddManager, bddRelationArray, domainVarBddArray,
1448	quantifyVarBddArray, rangeVarBddArray,
1449	info->option->verbosity);
1450	}
1451
1452	/* Free the bddRelationArray */
1453	mdd_array_free(bddRelationArray);
1454
1455	if ((info->option)->verbosity > 0) {
1456	fwdClusteredRelationArray = info->fwdClusteredRelationArray;
1457	bwdClusteredRelationArray = info->bwdClusteredRelationArray;
1458	if (method == Img_Iwls95_c)
1459	fprintf(vis_stdout,"Computing Image Using IWLS95 technique.\n");
1460	else if (method == Img_Mlp_c)
1461	fprintf(vis_stdout,"Computing Image Using MLP technique.\n");
1462	else if (method == Img_Linear_c) {
1463	fprintf(vis_stdout,"Computing Image Using LINEAR technique.\n");
1464	fwdClusteredRelationArray = info->fwdOptClusteredRelationArray;
1465	/bwdClusteredRelationArray = info->bwdOptClusteredRelationArray;/
1466	}
1467	else
1468	assert(0);
1469	fprintf(vis_stdout,"Total # of domain binary variables = %3d\n",
1470	array_n(domainVarBddArray));
1471	fprintf(vis_stdout,"Total # of range binary variables = %3d\n",
1472	array_n(rangeVarBddArray));
1473	fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n",
1474	array_n(quantifyVarBddArray));
1475	if ((directionType == Img_Forward_c) \|\| (directionType ==
1476	Img_Both_c)) {
1477	fprintf(vis_stdout, "Shared size of transition relation for forward image computation is %10ld BDD nodes (%-4d components)\n",
1478	bdd_size_multiple(fwdClusteredRelationArray),
1479	array_n(fwdClusteredRelationArray));
1480	}
1481	if ((directionType == Img_Backward_c) \|\| (directionType == Img_Both_c)) {
1482	fprintf(vis_stdout, "Shared size of transition relation for backward image computation is %10ld BDD nodes (%-4d components)\n",
1483	bdd_size_multiple(bwdClusteredRelationArray),
1484	array_n(bwdClusteredRelationArray));
1485	}
1486	}
1487
1488	/* Update nvars field in partial image options structure with
1489	total number of variables. */
1490	if (info->PIoption != NULL) {
1491	(info->PIoption)->nvars = array_n(domainVarBddArray) +
1492	array_n(quantifyVarBddArray) +
1493	array_n(rangeVarBddArray);
1494	}
1495	/* Free the Bdd arrays */
1496	mdd_array_free(quantifyVarBddArray);
1497
1498	flagValue = Cmd_FlagReadByName("image_eliminate_depend_vars");
1499	if (flagValue == NIL(char))
1500	info->eliminateDepend = 0; /* the default value */
1501	else
1502	info->eliminateDepend = atoi(flagValue);
1503	if (info->eliminateDepend && bdd_get_package_name() != CUDD) {
1504	fprintf(vis_stderr,
1505	"** trm error : image_eliminate_depend_vars is available for only CUDD.\n");
1506	info->eliminateDepend = 0;
1507	}
1508	info->nPrevEliminatedFwd = -1;
1509
1510	return (void *)info;
1511	}
1512	}
1513
1514
1515	/Function******************************************************************
1516
1517	Synopsis [Computes the forward image of a set of states.]
1518
1519	Description [Computes the forward image of a set of states. If
1520	partial image requested and the first image computed doesn't
1521	intersect toCareSet, then recompute image. ASSUME that toCareSet is
1522	in terms of functionData->domainVars.]
1523
1524	SideEffects [ IMPORTANT NOTE: image may be in terms of domain
1525	variables even when the reverse is expected IF partial images are
1526	allowed. The clean way would be to convert toCareset in terms of
1527	functionData->rangeVars but it may end up being quite inefficient.]
1528
1529	SeeAlso [ImgImageInfoComputeFwdWithDomainVarsIwls95]
1530
1531	******************************************************************************/
1532	mdd_t *
1533	ImgImageInfoComputeFwdIwls95(ImgFunctionData_t *functionData,
1534	Img_ImageInfo_t *imageInfo,
1535	mdd_t *fromLowerBound,
1536	mdd_t *fromUpperBound,
1537	array_t *toCareSetArray)
1538	{
1539	mdd_t image, domainSubset, *newFrom;
1540	mdd_manager *mddManager;
1541	boolean partial;
1542	Iwls95Info_t info = (Iwls95Info_t )imageInfo->methodData;
1543	int eliminateDepend;
1544	Img_OptimizeType optDir;
1545	array_t *fwdOriClusteredRelationArray;
1546	array_t *fwdOriArraySmoothVarBddArray;
1547	array_t *fwdOriSmoothVarCubeArray;
1548	array_t *fwdClusteredRelationArray;
1549	Relation_t *head;
1550	int bOptimize;
1551	boolean farSideImageIsEnabled;
1552	char *userSpecifiedMethod;
1553
1554	mddManager = Part_PartitionReadMddManager(functionData->mddNetwork);
1555
1556	if(imageInfo->methodType == Img_Linear_c) {
1557	if(info->fwdClusteredRelationArray == 0 \|\|
1558	imageInfo->useOptimizedRelationFlag) {
1559	fwdOriClusteredRelationArray = info->fwdOptClusteredRelationArray;
1560	fwdOriArraySmoothVarBddArray = info->fwdOptArraySmoothVarBddArray;
1561	fwdOriSmoothVarCubeArray = info->fwdOptSmoothVarCubeArray;
1562	}
1563	else {
1564	fwdOriClusteredRelationArray = info->fwdClusteredRelationArray;
1565	fwdOriArraySmoothVarBddArray = info->fwdArraySmoothVarBddArray;
1566	fwdOriSmoothVarCubeArray = info->fwdSmoothVarCubeArray;
1567	}
1568	}
1569	else {
1570	fwdOriClusteredRelationArray = info->fwdClusteredRelationArray;
1571	fwdOriArraySmoothVarBddArray = info->fwdArraySmoothVarBddArray;
1572	fwdOriSmoothVarCubeArray = info->fwdSmoothVarCubeArray;
1573	}
1574
1575	if (fwdOriClusteredRelationArray == NIL(array_t)) {
1576	fprintf(vis_stderr, "** img error: The data structure has not been ");
1577	fprintf(vis_stderr, "initialized for forward image computation\n");
1578	return NIL(mdd_t);
1579	}
1580
1581	if (info->eliminateDepend == 1 \|\|
1582	(info->eliminateDepend == 2 && info->nPrevEliminatedFwd > 0)) {
1583	eliminateDepend = 1;
1584	} else
1585	eliminateDepend = 0;
1586
1587	domainSubset = bdd_between(fromLowerBound, fromUpperBound);
1588
1589	if (eliminateDepend) {
1590	fwdClusteredRelationArray = mdd_array_duplicate(fwdOriClusteredRelationArray);
1591	newFrom = TrmEliminateDependVars(imageInfo, fwdClusteredRelationArray,
1592	domainSubset, NIL(mdd_t *));
1593	mdd_free(domainSubset);
1594	domainSubset = newFrom;
1595	} else
1596	fwdClusteredRelationArray = fwdOriClusteredRelationArray;
1597
1598	/* Record if partial images are allowed. */
1599	partial = info->allowPartialImage;
1600	info->wasPartialImage = FALSE;
1601
1602	/* bias field is used to bias the intermediate results towards care states */
1603	if ((info->PIoption)->partialImageApproxMethod == BDD_APPROX_BIASED_RUA) {
1604	/* assume that this array has only one mdd */
1605	mdd_t toCareSet = array_fetch(mdd_t , toCareSetArray, 0);
1606	(info->PIoption)->bias = mdd_dup(toCareSet);
1607	}
1608
1609	/* when the "compositional far side image approach" is selected, and
1610	* there are more than one transition relation clusters,
1611	* over-approximate images (w.r.t individual TR clusters) will be
1612	* used to minimize the transition relation.
1613	*/
1614	farSideImageIsEnabled = FALSE;
1615	userSpecifiedMethod = Cmd_FlagReadByName("image_farside_method");
1616	if (userSpecifiedMethod != NIL(char)) {
1617	if (!strcmp(userSpecifiedMethod, "1"))
1618	farSideImageIsEnabled = TRUE;
1619	}
1620
1621	if (!farSideImageIsEnabled \|\| array_n(fwdClusteredRelationArray) < 2) {
1622
1623	image = BddLinearAndSmooth(mddManager, domainSubset,
1624	fwdClusteredRelationArray,
1625	fwdOriArraySmoothVarBddArray,
1626	fwdOriSmoothVarCubeArray,
1627	(info->option)->verbosity,
1628	info->PIoption, &partial, info->lazySiftFlag);
1629
1630	}else {
1631
1632	array_t *fwdFarArraySmoothVarBddArray = fwdOriArraySmoothVarBddArray;
1633	array_t *fwdFarSmoothVarCubeArray = fwdOriSmoothVarCubeArray;
1634	array_t *fwdFarClusteredRelationArray = mdd_array_duplicate(fwdClusteredRelationArray);
1635	array_t upperBoundImages = array_alloc(mdd_t , 0);
1636	st_table domainSupportVarTable, trClusterSupportVarTable;
1637	mdd_t trCluster, newDomainset, newTRcluster, upperBoundImage;
1638	mdd_t holdMdd, tmpMdd;
1639	array_t *tempArray;
1640	int beforeSize, afterSize, middleSize;
1641	int size1, size2, size3;
1642	boolean flag1, flag2;
1643	int i,j, k;
1644	long bddId;
1645
1646	/* compute a series of over-approximate images based on individual
1647	* TR clusters
1648	*/
1649	domainSupportVarTable = st_init_table(st_ptrcmp, st_ptrhash);
1650	tempArray = mdd_get_bdd_support_ids(mddManager, domainSubset);
1651	arrayForEachItem(int, tempArray, j, bddId) {
1652	st_insert(domainSupportVarTable, (char )bddId, (char )0);
1653	}
1654	array_free(tempArray);
1655
1656	beforeSize = afterSize = middleSize =0;
1657	arrayForEachItem(mdd_t *, fwdFarClusteredRelationArray, i, trCluster) {
1658	array_t preQuantifiedVarsInDomainset = array_alloc(mdd_t , 0);
1659	array_t preQuantifiedVarsInTRcluster = array_alloc(mdd_t , 0);
1660	array_t quantifiedVarsInProduct = array_alloc(mdd_t , 0);
1661
1662	/* some variables can be quantified before taking the conjunction */
1663	trClusterSupportVarTable = st_init_table(st_ptrcmp, st_ptrhash);
1664	tempArray = mdd_get_bdd_support_ids(mddManager, trCluster);
1665	arrayForEachItem(int, tempArray, j, bddId) {
1666	st_insert(trClusterSupportVarTable, (char )bddId, (char )0);
1667	}
1668	array_free(tempArray);
1669	arrayForEachItem(array_t *, fwdFarArraySmoothVarBddArray, j, tempArray) {
1670	arrayForEachItem(mdd_t *, tempArray, k, holdMdd) {
1671	bddId = (int)bdd_top_var_id(holdMdd);
1672	flag1 = st_is_member(domainSupportVarTable, (char *)bddId);
1673	flag2 = st_is_member(trClusterSupportVarTable, (char *)bddId);
1674	if (flag1 && flag2)
1675	array_insert_last(mdd_t *, quantifiedVarsInProduct, holdMdd);
1676	else if (flag1)
1677	array_insert_last(mdd_t *, preQuantifiedVarsInDomainset, holdMdd);
1678	else if (flag2)
1679	array_insert_last(mdd_t *, preQuantifiedVarsInTRcluster, holdMdd);
1680	else
1681	;
1682	}
1683	}
1684	st_free_table(trClusterSupportVarTable);
1685
1686	if (array_n(preQuantifiedVarsInDomainset) == 0)
1687	newDomainset = bdd_dup(domainSubset);
1688	else
1689	newDomainset = bdd_smooth(domainSubset, preQuantifiedVarsInDomainset);
1690	array_free(preQuantifiedVarsInDomainset);
1691
1692	if (array_n(preQuantifiedVarsInTRcluster) == 0)
1693	newTRcluster = bdd_dup(trCluster);
1694	else
1695	newTRcluster = bdd_smooth(trCluster, preQuantifiedVarsInTRcluster);
1696	array_free(preQuantifiedVarsInTRcluster);
1697
1698	/* compute the over-approximated image */
1699	if (array_n(quantifiedVarsInProduct) == 0)
1700	upperBoundImage = bdd_and(newTRcluster, newDomainset, 1, 1);
1701	else
1702	upperBoundImage = bdd_and_smooth(newTRcluster, newDomainset, quantifiedVarsInProduct);
1703	array_free(quantifiedVarsInProduct);
1704	mdd_free(newTRcluster);
1705	mdd_free(newDomainset);
1706
1707	/* minimize the TR cluster with the new upper bound image */
1708	newTRcluster = Img_MinimizeImage(trCluster, upperBoundImage,
1709	Img_DefaultMinimizeMethod_c, TRUE);
1710
1711	size1 = mdd_size(trCluster);
1712	beforeSize += size1;
1713	size2 = mdd_size(upperBoundImage);
1714	middleSize += size2;
1715	size3 = mdd_size(newTRcluster);
1716	afterSize += size3;
1717	if (info->option->verbosity >= 3) {
1718	fprintf(vis_stdout, "farSideImg: minimize TR cluster[%d] %d \|%d => %d\n", i,
1719	size1, size2, size3);
1720	}
1721
1722	if (mdd_equal(newTRcluster, trCluster)) {
1723	mdd_free(newTRcluster);
1724	mdd_free(upperBoundImage);
1725	}else {
1726	mdd_free(trCluster);
1727	array_insert(mdd_t *, fwdFarClusteredRelationArray, i, newTRcluster);
1728	array_insert_last(mdd_t *, upperBoundImages, upperBoundImage);
1729	}
1730	}
1731	st_free_table(domainSupportVarTable);
1732
1733	if (info->option->verbosity >= 2) {
1734	fprintf(vis_stdout, "farSideImg: minimize TR total %d \|%d => %d\n",
1735	beforeSize, middleSize, afterSize);
1736	}
1737
1738	/* compute the image with the simplified transition relation */
1739	image = BddLinearAndSmooth(mddManager, domainSubset,
1740	fwdFarClusteredRelationArray,
1741	fwdFarArraySmoothVarBddArray,
1742	fwdFarSmoothVarCubeArray,
1743	(info->option)->verbosity,
1744	info->PIoption, &partial, info->lazySiftFlag);
1745	mdd_array_free(fwdFarClusteredRelationArray);
1746
1747	/* for performance concerns, the following operations are carried
1748	* out in the domain space
1749	*/
1750	arrayForEachItem(mdd_t *, upperBoundImages, i, holdMdd) {
1751	tmpMdd = ImgSubstitute(holdMdd, functionData, Img_R2D_c);
1752	mdd_free(holdMdd);
1753	array_insert(mdd_t *, upperBoundImages, i, tmpMdd);
1754	}
1755	holdMdd = image;
1756	image = ImgSubstitute(image, functionData,Img_R2D_c);
1757	mdd_free(holdMdd);
1758
1759	/* remove the "bad states" introduced by the TR cluster minimization */
1760	beforeSize = mdd_size(image);
1761	array_sort(upperBoundImages, MddSizeCompare);
1762	arrayForEachItem(mdd_t *, upperBoundImages, i, tmpMdd) {
1763	size1 = mdd_size(image);
1764	size2 = mdd_size(tmpMdd);
1765	holdMdd = image;
1766	image = mdd_and(image, tmpMdd, 1, 1);
1767	mdd_free(tmpMdd);
1768	mdd_free(holdMdd);
1769	size3 = mdd_size(image);
1770
1771	if (info->option->verbosity >= 3) {
1772	fprintf(vis_stdout, "farSideImg: clip image %d \| %d => %d\n",
1773	size1, size2, size3);
1774	}
1775	}
1776	array_free(upperBoundImages);
1777
1778	if (info->option->verbosity >= 2) {
1779	afterSize = mdd_size(image);
1780	fprintf(vis_stdout, "farSideImg: clip image total %d => %d \n",
1781	beforeSize, afterSize);
1782	}
1783
1784	}
1785
1786
1787	/* check that no partial image was computed if not allowed */
1788	assert(!((!info->allowPartialImage) && partial));
1789
1790	/* if partial image computed, and if no new states, recompute
1791	* image with relaxed parameters.
1792	*/
1793	if (partial) {
1794	if (bdd_leq_array(image, toCareSetArray, 1, 0)) {
1795	mdd_free(image);
1796	partial = info->allowPartialImage;
1797	image = RecomputeImageIfNecessary(functionData,
1798	mddManager,
1799	domainSubset,
1800	fwdClusteredRelationArray,
1801	fwdOriArraySmoothVarBddArray,
1802	fwdOriSmoothVarCubeArray,
1803	(info->option)->verbosity,
1804	info->PIoption,
1805	toCareSetArray,
1806	&partial, info->lazySiftFlag);
1807	}
1808	}
1809
1810	if(imageInfo->methodType == Img_Linear_c) {
1811	if(imageInfo->useOptimizedRelationFlag) {
1812	if(info->option->linearOptimize == Opt_NS \|\|
1813	info->option->linearOptimize == Opt_Both)
1814	optDir = Opt_Both;
1815	else
1816	optDir = Opt_CS;
1817
1818	head = ImgLinearRelationInit(mddManager, fwdOriClusteredRelationArray,
1819	functionData->domainBddVars, functionData->rangeBddVars,
1820	functionData->quantifyBddVars, info->option);
1821	bOptimize = ImgLinearOptimizeAll(head, optDir, 0);
1822	if(bOptimize) {
1823	ImgLinearRefineRelation(head);
1824	if(info->fwdClusteredRelationArray == 0 && optDir == Opt_Both) {
1825	info->fwdClusteredRelationArray = fwdOriClusteredRelationArray;
1826	info->fwdArraySmoothVarBddArray =
1827	BddArrayArrayDup(fwdOriArraySmoothVarBddArray);
1828	info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
1829	info->fwdArraySmoothVarBddArray);
1830	}
1831	else {
1832	mdd_array_free(fwdOriClusteredRelationArray);
1833	}
1834	fwdOriClusteredRelationArray = ImgLinearExtractRelationArrayT(head);
1835	info->fwdOptClusteredRelationArray = fwdOriClusteredRelationArray;
1836	}
1837	ImgLinearRelationQuit(head);
1838	}
1839	}
1840
1841	/* free the bias function created. */
1842	if ((info->PIoption)->partialImageApproxMethod == BDD_APPROX_BIASED_RUA) {
1843	mdd_free((info->PIoption)->bias);
1844	(info->PIoption)->bias = NIL(mdd_t);
1845	}
1846	/* indicate whether this image computation was partial or exact. */
1847	info->wasPartialImage = partial;
1848	info->allowPartialImage = FALSE;
1849
1850	if (eliminateDepend)
1851	mdd_array_free(fwdClusteredRelationArray);
1852	mdd_free(domainSubset);
1853
1854	return image;
1855	}
1856
1857	/Function******************************************************************
1858
1859	Synopsis [Computes the forward image of a set of states in terms
1860	of domain variables.]
1861
1862	Description [First the forward image computation function is called
1863	which returns an image on range vars. Later, variable substitution
1864	is used to obtain image on domain vars.]
1865
1866	SideEffects []
1867
1868	SeeAlso [ImgImageInfoComputeFwdIwls95]
1869
1870	******************************************************************************/
1871	mdd_t *
1872	ImgImageInfoComputeFwdWithDomainVarsIwls95(ImgFunctionData_t *functionData,
1873	Img_ImageInfo_t *imageInfo,
1874	mdd_t *fromLowerBound,
1875	mdd_t *fromUpperBound,
1876	array_t *toCareSetArray)
1877	{
1878	int i;
1879	array_t *toCareSetArrayRV = NIL(array_t);
1880	mdd_t toCareSet, toCareSetRV;
1881	mdd_t imageRV, imageDV;
1882	int useToCareSetFlag;
1883	Iwls95Info_t info = (Iwls95Info_t )imageInfo->methodData;
1884
1885	if (toCareSetArray && info->allowPartialImage)
1886	useToCareSetFlag = 1;
1887	else
1888	useToCareSetFlag = 0;
1889
1890	if (useToCareSetFlag) {
1891	toCareSetArrayRV = array_alloc(mdd_t *, 0);
1892	arrayForEachItem(bdd_t *, toCareSetArray, i, toCareSet) {
1893	toCareSetRV = ImgSubstitute(toCareSet, functionData, Img_D2R_c);
1894	array_insert(bdd_t *, toCareSetArrayRV, i, toCareSetRV);
1895	}
1896	}
1897
1898	imageRV = ImgImageInfoComputeFwdIwls95(functionData,
1899	imageInfo,
1900	fromLowerBound,
1901	fromUpperBound,
1902	toCareSetArrayRV);
1903
1904	imageDV = ImgSubstitute(imageRV, functionData, Img_R2D_c);
1905	mdd_free(imageRV);
1906	if (useToCareSetFlag)
1907	mdd_array_free(toCareSetArrayRV);
1908	return imageDV;
1909	}
1910
1911
1912	/Function******************************************************************
1913
1914	Synopsis [Computes the backward image of domainSubset.]
1915
1916	Description [First bdd_cofactor is used to compute the simplified set of
1917	states to compute the image of. Next, this simplified set is multiplied with
1918	the relation arrays given in the bwdClusteredRelationArray in order and the
1919	variables are quantified according to the schedule in
1920	bwdArraySmoothVarBddArray.]
1921
1922	SideEffects []
1923
1924	SeeAlso [ImgImageInfoComputeBwdWithDomainVarsIwls95]
1925
1926	******************************************************************************/
1927	mdd_t *
1928	ImgImageInfoComputeBwdIwls95(ImgFunctionData_t *functionData,
1929	Img_ImageInfo_t *imageInfo,
1930	mdd_t *fromLowerBound,
1931	mdd_t *fromUpperBound,
1932	array_t *toCareSetArray)
1933	{
1934	mdd_t image, domainSubset, *simplifiedImage;
1935	mdd_manager *mddManager;
1936	Iwls95Info_t info = (Iwls95Info_t )imageInfo->methodData;
1937	boolean partial;
1938
1939	if (info->bwdClusteredRelationArray == NIL(array_t)) {
1940	fprintf(vis_stderr, "** img error: The data structure has not been ");
1941	fprintf(vis_stderr, "initialized for backward image computation\n");
1942	return NIL(mdd_t);
1943	}
1944	mddManager = Part_PartitionReadMddManager(functionData->mddNetwork);
1945	domainSubset = bdd_between(fromLowerBound, fromUpperBound);
1946
1947	assert(mddManager != NIL(mdd_manager));
1948
1949	/* Check if we can use the stored simplified relations */
1950	if (info->careSetArray == NIL(array_t) \|\|
1951	!mdd_array_equal(info->careSetArray, toCareSetArray)){
1952	FreeClusteredCofactoredRelationArray(info);
1953	info->careSetArray = mdd_array_duplicate(toCareSetArray);
1954	info->bwdClusteredCofactoredRelationArray =
1955	ImgMinimizeImageArrayWithCareSetArray(info->bwdClusteredRelationArray,
1956	toCareSetArray,
1957	Img_DefaultMinimizeMethod_c, TRUE,
1958	(info->option->verbosity > 0),
1959	Img_Backward_c);
1960	}
1961
1962	/* if the partial images are allowed, compute the care set (or its superset)
1963	* so that partial products can be minimized with respect to it.
1964	*/
1965	partial = info->allowPartialImage;
1966	info->wasPartialImage = FALSE;
1967
1968	/* bias is used to bias the intermediate results towards care states */
1969	if ((info->PIoption)->partialImageApproxMethod == BDD_APPROX_BIASED_RUA) {
1970	/* assume that this array has only one mdd */
1971	mdd_t toCareSet = array_fetch(mdd_t , toCareSetArray, 0);
1972	(info->PIoption)->bias = mdd_dup(toCareSet);
1973	}
1974
1975
1976	image = BddLinearAndSmooth(mddManager, domainSubset,
1977	info->bwdClusteredCofactoredRelationArray,
1978	info->bwdArraySmoothVarBddArray,
1979	info->bwdSmoothVarCubeArray,
1980	(info->option)->verbosity,
1981	info->PIoption, &partial, info->lazySiftFlag);
1982
1983
1984	/* check that no partial image was computed if not allowed */
1985	assert(!((!info->allowPartialImage) && partial));
1986
1987	/* if partial image computed, and if no new states, recompute
1988	* image with relaxed parameters.
1989	*/
1990	if (partial && bdd_leq_array(image, toCareSetArray, 1, 0)) {
1991	bdd_free(image);
1992	partial = info->allowPartialImage;
1993	image = RecomputeImageIfNecessary(functionData,
1994	mddManager,
1995	domainSubset,
1996	info->bwdClusteredRelationArray,
1997	info->bwdArraySmoothVarBddArray,
1998	info->bwdSmoothVarCubeArray,
1999	(info->option)->verbosity,
2000	info->PIoption,
2001	toCareSetArray,
2002	&partial, info->lazySiftFlag);
2003	}
2004
2005	/* free the bias function created. */
2006	if ((info->PIoption)->partialImageApproxMethod == BDD_APPROX_BIASED_RUA) {
2007	mdd_free((info->PIoption)->bias);
2008	(info->PIoption)->bias = NIL(mdd_t);
2009	}
2010	/* indicate whether this image computation was partial or exact. */
2011	info->wasPartialImage = partial;
2012	info->allowPartialImage = FALSE;
2013
2014	mdd_free(domainSubset);
2015	simplifiedImage = bdd_minimize_array(image, toCareSetArray);
2016	bdd_free(image);
2017	return simplifiedImage;
2018	}
2019
2020	/Function******************************************************************
2021
2022	Synopsis [Computes the backward image of a set of states.]
2023
2024	Description [Identical to ImgImageInfoComputeBwdIwls95 except in the
2025	fromLowerBound and fromUpperBound, domainVars are substituted by
2026	rangeVars.]
2027
2028	SideEffects []
2029
2030	SeeAlso [ImgImageInfoComputeBwdIwls95]
2031
2032	******************************************************************************/
2033	mdd_t *
2034	ImgImageInfoComputeBwdWithDomainVarsIwls95(ImgFunctionData_t *functionData,
2035	Img_ImageInfo_t *imageInfo,
2036	mdd_t *fromLowerBound,
2037	mdd_t *fromUpperBound,
2038	array_t *toCareSetArray)
2039	{
2040	mdd_t *fromLowerBoundRV;
2041	mdd_t *fromUpperBoundRV;
2042	mdd_t *image;
2043
2044	fromLowerBoundRV = ImgSubstitute(fromLowerBound, functionData, Img_D2R_c);
2045	if (mdd_equal(fromLowerBound, fromUpperBound))
2046	fromUpperBoundRV = fromLowerBoundRV;
2047	else
2048	fromUpperBoundRV = ImgSubstitute(fromUpperBound, functionData, Img_D2R_c);
2049
2050	image = ImgImageInfoComputeBwdIwls95(functionData,
2051	imageInfo,
2052	fromLowerBoundRV,
2053	fromUpperBoundRV,
2054	toCareSetArray);
2055
2056	mdd_free(fromLowerBoundRV);
2057	if (!mdd_equal(fromLowerBound, fromUpperBound))
2058	mdd_free(fromUpperBoundRV);
2059	return image;
2060	}
2061
2062	/Function******************************************************************
2063
2064	Synopsis [Frees the memory associated with imageInfo.]
2065
2066	Description [Frees the memory associated with imageInfo.]
2067
2068	SideEffects []
2069
2070	SeeAlso [ImgImageInfoInitializeIwls95]
2071
2072	******************************************************************************/
2073	void
2074	ImgImageInfoFreeIwls95(void *methodData)
2075	{
2076	Iwls95Info_t info = (Iwls95Info_t )methodData;
2077
2078	if (info == NIL(Iwls95Info_t)) {
2079	fprintf(vis_stderr, "** img error: Trying to free the NULL image info\n");
2080	return;
2081	}
2082	if (info->bitRelationArray != NIL(array_t)) {
2083	mdd_array_free(info->bitRelationArray);
2084	}
2085	if (info->quantifyVarMddIdArray != NIL(array_t)) {
2086	array_free(info->quantifyVarMddIdArray);
2087	}
2088	if (info->fwdOptClusteredRelationArray != NIL(array_t)) {
2089	mdd_array_free(info->fwdOptClusteredRelationArray);
2090	mdd_array_array_free(info->fwdOptArraySmoothVarBddArray);
2091	}
2092	if (info->fwdOptSmoothVarCubeArray)
2093	mdd_array_free(info->fwdOptSmoothVarCubeArray);
2094	if (info->fwdClusteredRelationArray != NIL(array_t)) {
2095	mdd_array_free(info->fwdClusteredRelationArray);
2096	mdd_array_array_free(info->fwdArraySmoothVarBddArray);
2097	}
2098	if (info->fwdSmoothVarCubeArray)
2099	mdd_array_free(info->fwdSmoothVarCubeArray);
2100	if (info->bwdClusteredRelationArray != NIL(array_t)) {
2101	mdd_array_free(info->bwdClusteredRelationArray);
2102	mdd_array_array_free(info->bwdArraySmoothVarBddArray);
2103	}
2104	if (info->bwdSmoothVarCubeArray)
2105	mdd_array_free(info->bwdSmoothVarCubeArray);
2106	FreeClusteredCofactoredRelationArray(info);
2107
2108	if (info->option != NULL) ImgFreeTrmOptions(info->option);
2109	if (info->PIoption != NULL) FREE(info->PIoption);
2110
2111	if (info->savedArraySmoothVarBddArray != NIL(array_t))
2112	mdd_array_array_free(info->savedArraySmoothVarBddArray);
2113	if (info->savedSmoothVarCubeArray != NIL(array_t))
2114	mdd_array_free(info->savedSmoothVarCubeArray);
2115
2116	FREE(info);
2117	}
2118
2119	/Function******************************************************************
2120
2121	Synopsis [Prints information about the IWLS95 method.]
2122
2123	Description [This function is used to obtain the information about
2124	the parameters used to initialize the imageInfo. If the file pointer
2125	argument is not NULL, the options are printed out. The shared size
2126	of the transition relation is printed out on vis_stdout.]
2127
2128	SideEffects []
2129
2130	******************************************************************************/
2131	void
2132	ImgImageInfoPrintMethodParamsIwls95(void methodData, FILE fp)
2133	{
2134	Iwls95Info_t info = (Iwls95Info_t )methodData;
2135	if (fp == NULL) return;
2136	PrintOption(info->method, info->option, fp);
2137	if (info->fwdClusteredRelationArray != NIL(array_t)) {
2138	(void) fprintf(fp, "Shared size of transition relation for forward image computation is %10ld BDD nodes (%-4d components)\n",
2139	bdd_size_multiple(info->fwdClusteredRelationArray),
2140	array_n(info->fwdClusteredRelationArray));
2141	}
2142	if (info->bwdClusteredRelationArray != NIL(array_t)) {
2143	(void) fprintf(fp, "Shared size of transition relation for backward image computation is %10ld BDD nodes (%-4d components)\n",
2144	bdd_size_multiple(info->bwdClusteredRelationArray),
2145	array_n(info->bwdClusteredRelationArray));
2146	}
2147	}
2148
2149	/Function******************************************************************
2150
2151	Synopsis [Returns the st_table containing the bdd id of the support
2152	variables of the function.]
2153
2154	Description [Returns the st_table containing the bdd id of the support
2155	variables of the function.]
2156
2157	SideEffects []
2158
2159	******************************************************************************/
2160	st_table *
2161	ImgBddGetSupportIdTable(bdd_t *function)
2162	{
2163	st_table *supportTable;
2164	var_set_t *supportVarSet;
2165	int i;
2166
2167	supportTable = st_init_table(st_numcmp, st_numhash);
2168	supportVarSet = bdd_get_support(function);
2169	for(i=0; i<supportVarSet->n_elts; i++) {
2170	if (var_set_get_elt(supportVarSet, i) == 1) {
2171	st_insert(supportTable, (char *)(long) i, NIL(char));
2172	}
2173	}
2174	var_set_free(supportVarSet);
2175	return supportTable;
2176	}
2177
2178	/Function******************************************************************
2179
2180	Synopsis [Checks if the last image/preimage was partial.]
2181
2182	Description [Checks if the last image/preimage was partial. This
2183	flag is valid only for the last image/preimage computation. Reset
2184	before every image/preimage computation. ]
2185
2186	SideEffects [Reset before every image/preimage computation.]
2187
2188	SeeAlso [ImgImageAllowPartialImageIwls95]
2189
2190	******************************************************************************/
2191	boolean
2192	ImgImageWasPartialIwls95(void *methodData)
2193	{
2194	Iwls95Info_t info = (Iwls95Info_t ) methodData;
2195	return (info->wasPartialImage);
2196	}
2197
2198	/Function******************************************************************
2199
2200	Synopsis [Sets the flag to allow partial images.]
2201
2202	Description [Sets the flag to allow partial images. Default is to
2203	not allow partial image computations. This flag is reset at the end
2204	of every image/preimage computation i.e., has to be specified before
2205	every image/preimage computation if partial image is desired. ]
2206
2207	SideEffects [Flag is reset at the end of every image/preimage
2208	computation.]
2209
2210	SeeAlso [ImgImageWasPartialIwls95]
2211
2212	******************************************************************************/
2213	void
2214	ImgImageAllowPartialImageIwls95(void *methodData, boolean value)
2215	{
2216	Iwls95Info_t info = (Iwls95Info_t ) methodData;
2217	info->allowPartialImage = value;
2218	}
2219
2220	/Function******************************************************************
2221
2222	Synopsis [Restores original transition relation from saved.]
2223
2224	Description [Restores original transition relation from saved.]
2225
2226	SideEffects []
2227
2228	SeeAlso[ImgDuplicateTransitionRelationIwls95]
2229	******************************************************************************/
2230	void
2231	ImgRestoreTransitionRelationIwls95(Img_ImageInfo_t *imageInfo,
2232	Img_DirectionType directionType)
2233	{
2234	array_t *relationArray;
2235	Iwls95Info_t iwlsInfo = (Iwls95Info_t ) imageInfo->methodData;
2236	ImgFunctionData_t *functionData = &(imageInfo->functionData);
2237	mdd_manager *mgr = NIL(mdd_manager);
2238
2239	mgr = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
2240
2241	if (directionType == Img_Both_c) {
2242	fprintf(vis_stderr,
2243	"** img error : can't restore fwd and bwd at the same time.\n");
2244	return;
2245	}
2246
2247	relationArray = ImgGetTransitionRelationIwls95(iwlsInfo, directionType);
2248	mdd_array_free(relationArray);
2249	ImgUpdateTransitionRelationIwls95(iwlsInfo,
2250	(array_t *)imageInfo->savedRelation,
2251	directionType);
2252	imageInfo->savedRelation = NIL(void);
2253
2254	assert(iwlsInfo->savedArraySmoothVarBddArray);
2255	if (directionType == Img_Forward_c) {
2256	mdd_array_array_free(iwlsInfo->fwdArraySmoothVarBddArray);
2257	iwlsInfo->fwdArraySmoothVarBddArray = iwlsInfo->savedArraySmoothVarBddArray;
2258	if (functionData->createVarCubesFlag) {
2259	mdd_array_free(iwlsInfo->fwdSmoothVarCubeArray);
2260	iwlsInfo->fwdSmoothVarCubeArray = iwlsInfo->savedSmoothVarCubeArray;
2261	}
2262	} else {
2263	mdd_array_array_free(iwlsInfo->bwdArraySmoothVarBddArray);
2264	iwlsInfo->bwdArraySmoothVarBddArray = iwlsInfo->savedArraySmoothVarBddArray;
2265	if (functionData->createVarCubesFlag) {
2266	mdd_array_free(iwlsInfo->bwdSmoothVarCubeArray);
2267	iwlsInfo->bwdSmoothVarCubeArray = iwlsInfo->savedSmoothVarCubeArray;
2268	}
2269	}
2270	iwlsInfo->savedArraySmoothVarBddArray = NIL(array_t);
2271	iwlsInfo->savedSmoothVarCubeArray = NIL(array_t);
2272
2273	if(directionType == Img_Backward_c \|\| directionType == Img_Both_c)
2274	ResetClusteredCofactoredRelationArray(mgr, iwlsInfo);
2275	}
2276
2277	/Function******************************************************************
2278
2279	Synopsis [Duplicates transition relation.]
2280
2281	Description [Duplicates transition relation. Assumes that the
2282	Transition Relation is an array.]
2283
2284	SideEffects []
2285
2286	SeeAlso[ImgRestoreTransitionRelationIwls95]
2287	******************************************************************************/
2288	void
2289	ImgDuplicateTransitionRelationIwls95(Img_ImageInfo_t *imageInfo,
2290	Img_DirectionType directionType)
2291	{
2292	array_t relationArray, copiedRelationArray;
2293	Iwls95Info_t iwlsInfo = (Iwls95Info_t ) imageInfo->methodData;
2294	ImgFunctionData_t *functionData = &(imageInfo->functionData);
2295
2296	if (directionType == Img_Both_c) {
2297	fprintf(vis_stderr,
2298	"** img error : can't duplicate fwd and bwd at the same time.\n");
2299	return;
2300	}
2301
2302	relationArray = ImgGetTransitionRelationIwls95(iwlsInfo, directionType);
2303	copiedRelationArray = BddArrayDup(relationArray);
2304	assert(!imageInfo->savedRelation);
2305	imageInfo->savedRelation = (void *)relationArray;
2306	ImgUpdateTransitionRelationIwls95(iwlsInfo,
2307	copiedRelationArray, directionType);
2308
2309	assert(!iwlsInfo->savedArraySmoothVarBddArray);
2310	if (directionType == Img_Forward_c) {
2311	iwlsInfo->savedArraySmoothVarBddArray = iwlsInfo->fwdArraySmoothVarBddArray;
2312	iwlsInfo->fwdArraySmoothVarBddArray =
2313	CopyArrayBddArray(iwlsInfo->savedArraySmoothVarBddArray);
2314	if (functionData->createVarCubesFlag) {
2315	iwlsInfo->savedSmoothVarCubeArray = iwlsInfo->fwdSmoothVarCubeArray;
2316	iwlsInfo->fwdSmoothVarCubeArray =
2317	BddArrayDup(iwlsInfo->savedSmoothVarCubeArray);
2318	}
2319	} else {
2320	iwlsInfo->savedArraySmoothVarBddArray = iwlsInfo->bwdArraySmoothVarBddArray;
2321	iwlsInfo->bwdArraySmoothVarBddArray =
2322	CopyArrayBddArray(iwlsInfo->savedArraySmoothVarBddArray);
2323	if (functionData->createVarCubesFlag) {
2324	iwlsInfo->savedSmoothVarCubeArray = iwlsInfo->bwdSmoothVarCubeArray;
2325	iwlsInfo->bwdSmoothVarCubeArray =
2326	BddArrayDup(iwlsInfo->savedSmoothVarCubeArray);
2327	}
2328	}
2329	}
2330
2331
2332	/Function******************************************************************
2333
2334	Synopsis [Minimizes transition relation with given set of constraints.]
2335
2336	Description [Minimizes transition relation with given set of
2337	constraints. This invalidates the bwdclusteredcofactoredrelationarray.
2338
2339	<p>RB: Can Kavita or In-Ho please explain the difference between these four
2340	related functions?? (other three in SeeAlso)
2341
2342	The constraint should be in terms of present-state and input variables only.
2343
2344	This function takes care that the quantification schedule is correct
2345	afterwards. If reorderClusters is true, the clusters are reordered after
2346	minimization.
2347	]
2348
2349	SideEffects []
2350
2351	SeeAlso [ImgMinimizeTransitionRelationIwls95,
2352	ImgApproximateTransitionRelationIwls95, ImgAbstractTransitionRelationIwls95,
2353	Img_MinimizeImage]
2354	******************************************************************************/
2355	void
2356	ImgMinimizeTransitionRelationIwls95(
2357	void *methodData,
2358	ImgFunctionData_t *functionData,
2359	array_t *constrainArray,
2360	Img_MinimizeType minimizeMethod,
2361	Img_DirectionType directionType,
2362	boolean reorderClusters,
2363	int printStatus)
2364	{
2365	Iwls95Info_t info = (Iwls95Info_t )methodData;
2366
2367	if (minimizeMethod == Img_DefaultMinimizeMethod_c)
2368	minimizeMethod = Img_ReadMinimizeMethod();
2369
2370	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c) {
2371	ImgMinimizeImageArrayWithCareSetArrayInSitu(
2372	info->fwdClusteredRelationArray, constrainArray, minimizeMethod, TRUE,
2373	(printStatus == 2), Img_Forward_c);
2374
2375	if(reorderClusters)
2376	ReorderPartitionedTransitionRelation(info, functionData,
2377	Img_Forward_c);
2378	else{
2379	/* any minimization method other than restrict may introduce new
2380	variables, which invalidates the quantification schedule */
2381	assert(minimizeMethod != Img_DefaultMinimizeMethod_c);
2382	if(minimizeMethod != Img_Restrict_c)
2383	UpdateQuantificationSchedule(info, functionData, Img_Forward_c);
2384	}
2385	assert(CheckQuantificationSchedule(info->fwdClusteredRelationArray,
2386	info->fwdArraySmoothVarBddArray));
2387	}
2388
2389	if (directionType == Img_Backward_c \|\| directionType == Img_Both_c) {
2390	ImgMinimizeImageArrayWithCareSetArrayInSitu(
2391	info->bwdClusteredRelationArray, constrainArray, minimizeMethod, TRUE,
2392	(printStatus == 2), Img_Backward_c);
2393
2394	if(reorderClusters)
2395	ReorderPartitionedTransitionRelation(info, functionData,
2396	Img_Backward_c);
2397	/* Minimization can only introduce PS variables, which need not be
2398	quantified out, hence no need to recompute quantification schedule
2399	in backward case. */
2400	assert(CheckQuantificationSchedule(info->bwdClusteredRelationArray,
2401	info->bwdArraySmoothVarBddArray))
2402	}
2403
2404	if(directionType == Img_Backward_c \|\| directionType == Img_Both_c)
2405	FreeClusteredCofactoredRelationArray(info);
2406
2407	return;
2408	}
2409
2410
2411	/Function******************************************************************
2412
2413	Synopsis [Abstracts out given variables from transition relation.]
2414
2415	Description [Abstracts out given variables from transition relation.
2416	abstractVars should be an array of bdd variables. This invalidates the
2417	bwdclusteredcofactoredrelationarray. ]
2418
2419	SideEffects []
2420
2421	SeeAlso [ImgMinimizeTransitionRelationIwls95,
2422	ImgApproximateTransitionRelationIwls95, ImgAbstractTransitionRelationIwls95]
2423
2424	******************************************************************************/
2425	void
2426	ImgAbstractTransitionRelationIwls95(Img_ImageInfo_t *imageInfo,
2427	array_t abstractVars, mdd_t abstractCube,
2428	Img_DirectionType directionType, int printStatus)
2429	{
2430	Iwls95Info_t info = (Iwls95Info_t )imageInfo->methodData;
2431	int i, fwd_size, bwd_size;
2432	bdd_t relation, abstractedRelation;
2433
2434	if (!abstractVars \|\| array_n(abstractVars) == 0)
2435	return;
2436
2437	fwd_size = bwd_size = 0;
2438	if (printStatus) {
2439	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c)
2440	fwd_size = bdd_size_multiple(info->fwdClusteredRelationArray);
2441	if (directionType == Img_Backward_c \|\| directionType == Img_Both_c)
2442	bwd_size = bdd_size_multiple(info->bwdClusteredRelationArray);
2443	}
2444	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c) {
2445	arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) {
2446	if (abstractCube)
2447	abstractedRelation = bdd_smooth_with_cube(relation, abstractCube);
2448	else
2449	abstractedRelation = bdd_smooth(relation, abstractVars);
2450	if (printStatus == 2) {
2451	(void) fprintf(vis_stdout,
2452	"IMG Info: abstracted fwd relation %d => %d in component %d\n",
2453	bdd_size(relation), bdd_size(abstractedRelation), i);
2454	}
2455	mdd_free(relation);
2456	array_insert(bdd_t*, info->fwdClusteredRelationArray, i,
2457	abstractedRelation);
2458	}
2459	}
2460	if (directionType == Img_Backward_c \|\| directionType == Img_Both_c) {
2461	arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) {
2462	if (abstractCube)
2463	abstractedRelation = bdd_smooth_with_cube(relation, abstractCube);
2464	else
2465	abstractedRelation = bdd_smooth(relation, abstractVars);
2466	if (printStatus == 2) {
2467	(void) fprintf(vis_stdout,
2468	"IMG Info: abstracted bwd relation %d => %d in component %d\n",
2469	bdd_size(relation), bdd_size(abstractedRelation), i);
2470	}
2471	mdd_free(relation);
2472	array_insert(bdd_t*, info->bwdClusteredRelationArray, i,
2473	abstractedRelation);
2474	}
2475	}
2476	if (printStatus) {
2477	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c) {
2478	(void) fprintf(vis_stdout,
2479	"IMG Info: abstracted fwd relation [%d => %ld] with %d components\n",
2480	fwd_size,
2481	bdd_size_multiple(info->fwdClusteredRelationArray),
2482	array_n(info->fwdClusteredRelationArray));
2483	}
2484	if (directionType == Img_Backward_c \|\| directionType == Img_Both_c) {
2485	(void) fprintf(vis_stdout,
2486	"IMG Info: abstracted bwd relation [%d => %ld] with %d components\n",
2487	bwd_size,
2488	bdd_size_multiple(info->bwdClusteredRelationArray),
2489	array_n(info->bwdClusteredRelationArray));
2490	}
2491	}
2492
2493	if(directionType == Img_Backward_c \|\| directionType == Img_Both_c)
2494	FreeClusteredCofactoredRelationArray(info);
2495	}
2496
2497
2498	/Function******************************************************************
2499
2500	Synopsis [Approximate transition relation.]
2501
2502	Description [Approximate transition relation. This invalidates the
2503	bwdclusteredcofactoredrelationarray. ]
2504
2505	SideEffects [ImgMinimizeTransitionRelationIwls95,
2506	ImgApproximateTransitionRelationIwls95, ImgAbstractTransitionRelationIwls95,
2507	Img_ApproximateImage]
2508
2509	******************************************************************************/
2510	int
2511	ImgApproximateTransitionRelationIwls95(mdd_manager mgr, void methodData,
2512	bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod,
2513	int approxThreshold, double approxQuality,
2514	double approxQualityBias,
2515	Img_DirectionType directionType, mdd_t *bias)
2516	{
2517	Iwls95Info_t info = (Iwls95Info_t )methodData;
2518	int i;
2519	bdd_t relation, approxRelation;
2520	int unchanged = 0;
2521
2522	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c) {
2523	arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) {
2524	approxRelation = Img_ApproximateImage(mgr, relation,
2525	approxDir, approxMethod,
2526	approxThreshold, approxQuality,
2527	approxQualityBias, bias);
2528	if (bdd_is_tautology(approxRelation, 1)) {
2529	fprintf(vis_stdout,
2530	"** img warning : bdd_one from subsetting in fwd[%d].\n", i);
2531	mdd_free(approxRelation);
2532	unchanged++;
2533	} else if (bdd_is_tautology(approxRelation, 0)) {
2534	fprintf(vis_stdout,
2535	"** img warning : bdd_zero from subsetting in fwd[%d].\n", i);
2536	mdd_free(approxRelation);
2537	unchanged++;
2538	} else if (mdd_equal(approxRelation, relation)) {
2539	mdd_free(approxRelation);
2540	unchanged++;
2541	} else {
2542	mdd_free(relation);
2543	array_insert(bdd_t*, info->fwdClusteredRelationArray, i,
2544	approxRelation);
2545	}
2546	}
2547	}
2548	if (directionType == Img_Backward_c \|\| directionType == Img_Both_c) {
2549	arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) {
2550	approxRelation = Img_ApproximateImage(mgr, relation,
2551	approxDir, approxMethod,
2552	approxThreshold, approxQuality,
2553	approxQualityBias, bias);
2554	if (bdd_is_tautology(approxRelation, 1)) {
2555	fprintf(vis_stdout,
2556	"** img warning : bdd_one from subsetting in bwd[%d].\n", i);
2557	mdd_free(approxRelation);
2558	unchanged++;
2559	} else if (bdd_is_tautology(approxRelation, 0)) {
2560	fprintf(vis_stdout,
2561	"** img warning : bdd_zero from subsetting in bwd[%d].\n", i);
2562	mdd_free(approxRelation);
2563	unchanged++;
2564	} else if (mdd_equal(approxRelation, relation)) {
2565	mdd_free(approxRelation);
2566	unchanged++;
2567	} else {
2568	mdd_free(relation);
2569	array_insert(bdd_t*, info->bwdClusteredRelationArray, i,
2570	approxRelation);
2571	}
2572	}
2573	}
2574
2575	if(directionType == Img_Backward_c \|\| directionType == Img_Both_c)
2576	FreeClusteredCofactoredRelationArray(info);
2577
2578	return(unchanged);
2579	}
2580
2581
2582	/Function******************************************************************
2583
2584	Synopsis [Returns current transition relation.]
2585
2586	Description [Returns current transition relation.]
2587
2588	SideEffects []
2589
2590	******************************************************************************/
2591	array_t *
2592	ImgGetTransitionRelationIwls95(void *methodData,
2593	Img_DirectionType directionType)
2594	{
2595	Iwls95Info_t info = (Iwls95Info_t )methodData;
2596
2597	if (directionType == Img_Forward_c)
2598	return(info->fwdClusteredRelationArray);
2599	else if (directionType == Img_Backward_c)
2600	return(info->bwdClusteredRelationArray);
2601	return(NIL(array_t));
2602	}
2603
2604
2605	/Function******************************************************************
2606
2607	Synopsis [Overwrites transition relation with given.]
2608
2609	Description [Overwrites transition relation with given.]
2610
2611	SideEffects []
2612
2613	******************************************************************************/
2614	void
2615	ImgUpdateTransitionRelationIwls95(void methodData, array_t relationArray,
2616	Img_DirectionType directionType)
2617	{
2618	Iwls95Info_t info = (Iwls95Info_t )methodData;
2619
2620	if (directionType == Img_Forward_c)
2621	info->fwdClusteredRelationArray = relationArray;
2622	else if (directionType == Img_Backward_c)
2623	info->bwdClusteredRelationArray = relationArray;
2624	}
2625
2626
2627	/Function******************************************************************
2628
2629	Synopsis [Replace ith partitioned transition relation.]
2630
2631	Description [Replace ith partitioned transition relation.]
2632
2633	SideEffects []
2634
2635	******************************************************************************/
2636	void
2637	ImgReplaceIthPartitionedTransitionRelationIwls95(void *methodData,
2638	int i, mdd_t *relation, Img_DirectionType directionType)
2639	{
2640	array_t *relationArray;
2641	mdd_t *old;
2642
2643	relationArray = ImgGetTransitionRelationIwls95(methodData, directionType);
2644	if (!relationArray)
2645	return;
2646	old = array_fetch(mdd_t *, relationArray, i);
2647	mdd_free(old);
2648	array_insert(mdd_t *, relationArray, i, relation);
2649	}
2650
2651
2652	/Function******************************************************************
2653
2654	Synopsis [Frees current transition relation and associated
2655	quantification schedule for the given direction.]
2656
2657	Description [Frees current transition relation and associated
2658	quantification schedule for the given direction.]
2659
2660	SideEffects []
2661
2662	******************************************************************************/
2663	void
2664	ImgImageFreeClusteredTransitionRelationIwls95(void *methodData,
2665	Img_DirectionType directionType)
2666	{
2667	Iwls95Info_t info = (Iwls95Info_t )methodData;
2668
2669	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c) {
2670	if (info->fwdClusteredRelationArray != NIL(array_t)) {
2671	mdd_array_free(info->fwdClusteredRelationArray);
2672	info->fwdClusteredRelationArray = NIL(array_t);
2673	}
2674	if (info->fwdArraySmoothVarBddArray != NIL(array_t)) {
2675	mdd_array_array_free(info->fwdArraySmoothVarBddArray);
2676	info->fwdArraySmoothVarBddArray = NIL(array_t);
2677	}
2678	if (info->fwdSmoothVarCubeArray != NIL(array_t)) {
2679	mdd_array_free(info->fwdSmoothVarCubeArray);
2680	info->fwdSmoothVarCubeArray = NIL(array_t);
2681	}
2682	}
2683	if (directionType == Img_Backward_c \|\| directionType == Img_Both_c) {
2684	if (info->bwdClusteredRelationArray != NIL(array_t)) {
2685	mdd_array_free(info->bwdClusteredRelationArray);
2686	info->bwdClusteredRelationArray = NIL(array_t);
2687	}
2688	if (info->bwdArraySmoothVarBddArray != NIL(array_t)) {
2689	mdd_array_array_free(info->bwdArraySmoothVarBddArray);
2690	info->bwdArraySmoothVarBddArray = NIL(array_t);
2691	}
2692	if (info->bwdSmoothVarCubeArray != NIL(array_t)) {
2693	mdd_array_free(info->bwdSmoothVarCubeArray);
2694	info->bwdSmoothVarCubeArray = NIL(array_t);
2695	}
2696	}
2697	}
2698
2699
2700
2701	/Function******************************************************************
2702
2703	Synopsis [Constrains/Adds dont-cares to the bit relation and creates
2704	a new transition relation.]
2705
2706	Description [Constrains/adds dont-cares to the bit relation and creates a new
2707	transition relation. First, the existing transition relation is freed. The
2708	bit relation is created if it isn't stored already. The bit relation is then
2709	copied into the clustered relation field of the given direction. Then, it is
2710	constrained by the given constraint (underapprox) or the complement of the
2711	constraint is added (overapprox) to the bit relation. Then the modified bit
2712	relation is clustered. The underApprox flag indicates whether to create an
2713	over or an underapproximation of the transition relation (TRUE for
2714	underapproximation, FALSE for overapproximation). Although the procedure
2715	Img_MinimizeImage is used, the minimizeMethod flag for underapproximations
2716	should be generated by Img_GuidedSearchReadUnderApproxMinimizeMethod. The
2717	clean up flag indicates freeing of the bit relations. If the forceReorder
2718	flag is set, variable reordering is fired after freeing old relations and
2719	before creating new relations.]
2720
2721	SideEffects [Frees current transition relation and quantification
2722	schedule. Frees bit relations if indicated. ]
2723
2724	SeeAlso [Img_MultiwayLinearAndSmooth ImgImageInfoInitializeMono
2725	Img_MinimizeImage]
2726
2727	******************************************************************************/
2728	void
2729	ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(
2730	Img_ImageInfo_t *imageInfo,
2731	Img_DirectionType direction,
2732	mdd_t *constrain,
2733	Img_MinimizeType minimizeMethod,
2734	boolean underApprox,
2735	boolean cleanUp,
2736	boolean forceReorder,
2737	int printStatus)
2738	{
2739	ImgFunctionData_t *functionData = &(imageInfo->functionData);
2740	Iwls95Info_t info = (Iwls95Info_t )imageInfo->methodData;
2741	array_t *constrainArray;
2742	mdd_manager *mddManager = Part_PartitionReadMddManager(functionData->mddNetwork);
2743	array_t *relationArray = NIL(array_t);
2744	array_t *relationArrayFwd = NIL(array_t);
2745	array_t *relationArrayBwd = NIL(array_t);
2746
2747	assert(imageInfo->methodType == Img_Iwls95_c \|\|
2748	imageInfo->methodType == Img_Mlp_c);
2749
2750	/* free existing relation */
2751	ImgImageFreeClusteredTransitionRelationIwls95(imageInfo->methodData,
2752	direction);
2753	if (forceReorder) bdd_reorder(mddManager);
2754	/* create a bit relation and quantifiable variables (PIs and
2755	intermediate variables) if necessary */
2756	CreateBitRelationArray(info, functionData);
2757
2758	/* make a work copy of the bit array */
2759	relationArray = BddArrayDup(info->bitRelationArray);
2760
2761	if (cleanUp) FreeBitRelationArray(info);
2762
2763	/* apply the constraint to the bit relation */
2764	if (constrain) {
2765	constrainArray = array_alloc(mdd_t *, 1);
2766	array_insert(mdd_t *, constrainArray, 0, constrain);
2767	ImgMinimizeImageArrayWithCareSetArrayInSitu(relationArray,
2768	constrainArray,
2769	minimizeMethod, underApprox,
2770	printStatus, direction);
2771	array_free(constrainArray);
2772	}
2773
2774	if (direction == Img_Forward_c) {
2775	relationArrayFwd = relationArray;
2776	} else if (direction == Img_Backward_c) {
2777	relationArrayBwd = relationArray;
2778	} else if (direction == Img_Both_c) {
2779	relationArrayFwd = relationArray;
2780	relationArrayBwd = BddArrayDup(relationArray);
2781	} else {
2782	assert(0);
2783	}
2784	relationArray = NIL(array_t);
2785
2786	/* return order and recluster the relation */
2787	if (direction == Img_Forward_c \|\| direction == Img_Both_c) {
2788	Img_ClusterRelationArray(mddManager,
2789	imageInfo->methodType,
2790	direction,
2791	relationArrayFwd,
2792	functionData->domainVars,
2793	functionData->rangeVars,
2794	info->quantifyVarMddIdArray,
2795	&info->fwdClusteredRelationArray,
2796	&info->fwdArraySmoothVarBddArray,
2797	NULL,
2798	1);
2799	if (functionData->createVarCubesFlag) {
2800	info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
2801	info->fwdArraySmoothVarBddArray);
2802	}
2803	}
2804
2805	if (direction == Img_Backward_c \|\| direction == Img_Both_c) {
2806	Img_ClusterRelationArray(mddManager,
2807	imageInfo->methodType,
2808	direction,
2809	relationArrayBwd,
2810	functionData->domainVars,
2811	functionData->rangeVars,
2812	info->quantifyVarMddIdArray,
2813	&info->bwdClusteredRelationArray,
2814	&info->bwdArraySmoothVarBddArray,
2815	NULL,
2816	1);
2817	if (functionData->createVarCubesFlag) {
2818	info->bwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
2819	info->bwdArraySmoothVarBddArray);
2820	}
2821	}
2822
2823	if (cleanUp) {
2824	array_free(info->quantifyVarMddIdArray);
2825	info->quantifyVarMddIdArray = NIL(array_t);
2826	}
2827
2828	/* Print information */
2829	if (info->option->verbosity > 0){
2830	fprintf(vis_stdout,"Computing Image Using %s technique.\n",
2831	imageInfo->methodType == Img_Mlp_c ? "MLP" : "IWLS95");
2832	fprintf(vis_stdout,"Total # of domain binary variables = %3d\n",
2833	array_n(functionData->domainBddVars));
2834	fprintf(vis_stdout,"Total # of range binary variables = %3d\n",
2835	array_n(functionData->rangeBddVars));
2836	if (info->quantifyVarMddIdArray) {
2837	array_t *bddArray;
2838
2839	bddArray = mdd_id_array_to_bdd_array(mddManager,
2840	info->quantifyVarMddIdArray);
2841	fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n",
2842	array_n(bddArray));
2843	mdd_array_free(bddArray);
2844	} else {
2845	fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n",
2846	array_n(functionData->quantifyBddVars));
2847	}
2848	if (((direction == Img_Forward_c) \|\| (direction == Img_Both_c)) &&
2849	(info->fwdClusteredRelationArray != NIL(array_t))) {
2850	(void) fprintf(vis_stdout,
2851	"Shared size of transition relation for forward image ");
2852	(void) fprintf(vis_stdout,
2853	"computation is %10ld BDD nodes (%-4d components)\n",
2854	bdd_size_multiple(info->fwdClusteredRelationArray),
2855	array_n(info->fwdClusteredRelationArray));
2856	}
2857	if (((direction == Img_Backward_c) \|\| (direction == Img_Both_c)) &&
2858	(info->bwdClusteredRelationArray != NIL(array_t))) {
2859	(void) fprintf(vis_stdout,
2860	"Shared size of transition relation for backward image ");
2861	(void) fprintf(vis_stdout,
2862	"computation is %10ld BDD nodes (%-4d components)\n",
2863	bdd_size_multiple(info->bwdClusteredRelationArray),
2864	array_n(info->bwdClusteredRelationArray));
2865	}
2866	}/* if verbosity > 0 */
2867
2868	if(direction == Img_Backward_c \|\| direction == Img_Both_c)
2869	ResetClusteredCofactoredRelationArray(mddManager, info);
2870	}
2871
2872
2873
2874	/Function******************************************************************
2875
2876	Synopsis [Prints integers from an array.]
2877
2878	Description [Prints integers from an array.]
2879
2880	SideEffects []
2881
2882	******************************************************************************/
2883	void
2884	ImgPrintIntegerArray(array_t *idArray)
2885	{
2886	int i;
2887	fprintf(vis_stdout,
2888	"************** printing bdd ids from the bdd array *********\n");
2889	fprintf(vis_stdout,"%d::\t", array_n(idArray));
2890	for (i=0;i<array_n(idArray); i++) {
2891	fprintf(vis_stdout," %d ", array_fetch(int, idArray, i));
2892	}
2893	}
2894
2895
2896	/Function******************************************************************
2897
2898	Synopsis [Prints the given parition.]
2899
2900	Description [Prints the given parition.]
2901
2902	SideEffects []
2903
2904	******************************************************************************/
2905	void
2906	ImgPrintPartition(graph_t *partition)
2907	{
2908	vertex_t *vertex;
2909	lsList vertexList = g_get_vertices(partition);
2910	lsGen gen;
2911	st_table *vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
2912	fprintf(vis_stdout,"\n");
2913	lsForEachItem(vertexList, gen, vertex) {
2914	if (lsLength(g_get_out_edges(vertex)) == 0)
2915	PrintPartitionRecursively(vertex,vertexTable,0);
2916	}
2917	st_free_table(vertexTable);
2918	}
2919
2920
2921	/Function******************************************************************
2922
2923	Synopsis [Prints info of the partitioned transition relation.]
2924
2925	Description [Prints info of the partitioned transition relation.]
2926
2927	SideEffects []
2928
2929	******************************************************************************/
2930	void
2931	ImgPrintPartitionedTransitionRelation(mdd_manager *mddManager,
2932	array_t *relationArray,
2933	array_t *arraySmoothVarBddArray)
2934	{
2935	int i, j, n;
2936	mdd_t *relation;
2937	mdd_t *bdd;
2938	array_t *smoothVarBddArray;
2939	array_t *bvar_list = mdd_ret_bvar_list(mddManager);
2940	var_set_t *vset;
2941	bvar_type bv;
2942
2943	n = array_n(relationArray);
2944
2945	fprintf(vis_stdout, "# of relations = %d\n", n);
2946	if (arraySmoothVarBddArray) {
2947	smoothVarBddArray = array_fetch(array_t *, arraySmoothVarBddArray, 0);
2948	fprintf(vis_stdout, "Early smooth(%d) = ", array_n(smoothVarBddArray));
2949	for (j = 0; j < array_n(smoothVarBddArray); j++) {
2950	bdd = array_fetch(mdd_t *, smoothVarBddArray, j);
2951	mdd_print_support_to_file(vis_stdout, " %s", bdd);
2952	}
2953	fprintf(vis_stdout, "\n");
2954	}
2955	for (i = 0; i < n; i++) {
2956	relation = array_fetch(mdd_t *, relationArray, i);
2957	fprintf(vis_stdout, "T[%d] : bdd_size = %d\n", i, bdd_size(relation));
2958	fprintf(vis_stdout, " support(%d) = ",
2959	mdd_get_number_of_bdd_support(mddManager, relation));
2960	vset = bdd_get_support(relation);
2961	for (j = 0; j < array_n(bvar_list); j++) {
2962	if (var_set_get_elt(vset, j) == 1) {
2963	bv = array_fetch(bvar_type, bvar_list, j);
2964	mdd_print_support_to_file(vis_stdout, " %s", bv.node);
2965	}
2966	}
2967	var_set_free(vset);
2968	fprintf(vis_stdout, "\n");
2969	if (arraySmoothVarBddArray) {
2970	smoothVarBddArray = array_fetch(array_t *, arraySmoothVarBddArray, i + 1);
2971	fprintf(vis_stdout, " smooth(%d) = ", array_n(smoothVarBddArray));
2972	for (j = 0; j < array_n(smoothVarBddArray); j++) {
2973	bdd = array_fetch(mdd_t *, smoothVarBddArray, j);
2974	mdd_print_support_to_file(vis_stdout, " %s", bdd);
2975	}
2976	fprintf(vis_stdout, "\n");
2977	}
2978	}
2979	}
2980
2981
2982	/Function******************************************************************
2983
2984	Synopsis [Eliminates dependent variables from transition relation.]
2985
2986	Description [Eliminates dependent variables from a transition
2987	relation. Returns a simplified copy of the given states if successful;
2988	NULL otherwise.]
2989
2990	SideEffects [relationArray is also modified.]
2991
2992	SeeAlso []
2993
2994	******************************************************************************/
2995	mdd_t *
2996	ImgTrmEliminateDependVars(ImgFunctionData_t *functionData,
2997	array_t *relationArray,
2998	mdd_t states, mdd_t *dependRelations,
2999	int *nDependVars)
3000	{
3001	int i, j;
3002	int howMany = 0; /* number of latches that can be eliminated */
3003	mdd_t var, newStates, abs, positive, phi, tmp, *relation;
3004	int nSupports; /* vars in the support of the state set */
3005	int candidates; / vars to be considered for elimination */
3006	double minStates;
3007	var_set_t *supportVarSet;
3008	graph_t *mddNetwork;
3009	mdd_manager *mddManager;
3010
3011	mddNetwork = functionData->mddNetwork;
3012	mddManager = Part_PartitionReadMddManager(mddNetwork);
3013
3014	if (dependRelations)
3015	*dependRelations = mdd_one(mddManager);
3016	newStates = mdd_dup(states);
3017
3018	nSupports = 0;
3019	supportVarSet = bdd_get_support(newStates);
3020	for (i = 0; i < supportVarSet->n_elts; i++) {
3021	if (var_set_get_elt(supportVarSet, i) == 1)
3022	nSupports++;
3023	}
3024	candidates = ALLOC(int, nSupports);
3025	if (candidates == NULL) {
3026	var_set_free(supportVarSet);
3027	return(NULL);
3028	}
3029	nSupports = 0;
3030	for (i = 0; i < supportVarSet->n_elts; i++) {
3031	if (var_set_get_elt(supportVarSet, i) == 1) {
3032	candidates[nSupports] = i;
3033	nSupports++;
3034	}
3035	}
3036	var_set_free(supportVarSet);
3037
3038	/* The signatures of the variables in a function are the number
3039	** of minterms of the positive cofactors with respect to the
3040	** variables themselves. */
3041	signatures = bdd_cof_minterm(newStates);
3042	if (signatures == NULL) {
3043	FREE(candidates);
3044	return(NULL);
3045	}
3046	/* We now extract a positive quantity which is higher for those
3047	** variables that are closer to being essential. */
3048	minStates = signatures[nSupports];
3049	for (i = 0; i < nSupports; i++) {
3050	double z = signatures[i] / minStates - 1.0;
3051	signatures[i] = (z < 0.0) ? -z : z; /* make positive */
3052	}
3053	qsort((void *)candidates, nSupports, sizeof(int),
3054	(int ()(const void , const void *))TrmSignatureCompare);
3055	FREE(signatures);
3056
3057	/* Now process the candidates in the given order. */
3058	for (i = 0; i < nSupports; i++) {
3059	var = bdd_var_with_index(mddManager, candidates[i]);
3060	if (bdd_var_is_dependent(newStates, var)) {
3061	abs = bdd_smooth_with_cube(newStates, var);
3062	if (abs == NULL)
3063	return(NULL);
3064	positive = bdd_cofactor(newStates, var);
3065	if (positive == NULL)
3066	return(NULL);
3067	phi = Img_MinimizeImage(positive, abs, Img_DefaultMinimizeMethod_c, 1);
3068	if (phi == NULL)
3069	return(NULL);
3070	mdd_free(positive);
3071	if (bdd_size(phi) < IMG_MAX_DEP_SIZE) {
3072	howMany++;
3073	for (j = 0; j < array_n(relationArray); j++) {
3074	relation = array_fetch(mdd_t *, relationArray, j);
3075	if (dependRelations)
3076	tmp = bdd_smooth_with_cube(relation, var);
3077	else
3078	tmp = bdd_compose(relation, var, phi);
3079	mdd_free(relation);
3080	array_insert(mdd_t *, relationArray, j, tmp);
3081	}
3082	mdd_free(newStates);
3083	newStates = abs;
3084	if (dependRelations) {
3085	relation = mdd_xnor(var, phi);
3086	tmp = ImgSubstitute(relation, functionData, Img_R2D_c);
3087	mdd_free(relation);
3088	relation = mdd_and(*dependRelations, tmp, 1, 1);
3089	mdd_free(*dependRelations);
3090	*dependRelations = relation;
3091	}
3092	} else {
3093	mdd_free(abs);
3094	}
3095	mdd_free(phi);
3096	}
3097	}
3098	FREE(candidates);
3099
3100	*nDependVars = howMany;
3101	return(newStates);
3102	} /* end of ImgTrmEliminateDependVars */
3103
3104
3105	/---------------------------------------------------------------------------/
3106	/* Definition of static functions */
3107	/---------------------------------------------------------------------------/
3108
3109	/Function******************************************************************
3110
3111	Synopsis [Reset the clusteredcofactoredrelationarray to the
3112	clusteredrelationarray.]
3113
3114	Description [Copy the clustered array into the clusteredcofactored array, and
3115	set the caresetarray to (1). Assumes either both the caresetarray and the
3116	cofactoredarray are NIL, or that they both contain sensible data.]
3117
3118	SideEffects []
3119
3120	******************************************************************************/
3121	static void
3122	ResetClusteredCofactoredRelationArray(
3123	mdd_manager *mddManager,
3124	Iwls95Info_t *info)
3125	{
3126	int i;
3127	mdd_t *cluster;
3128
3129	assert(info->bwdClusteredRelationArray != NIL(array_t));
3130
3131	FreeClusteredCofactoredRelationArray(info);
3132
3133	info->careSetArray = array_alloc(mdd_t *, 1);
3134	array_insert_last(mdd_t *, info->careSetArray, mdd_one(mddManager));
3135	info->bwdClusteredCofactoredRelationArray = array_alloc(mdd_t *, 0);
3136
3137	arrayForEachItem(mdd_t *, info->bwdClusteredRelationArray, i, cluster){
3138	array_insert_last(mdd_t *, info->bwdClusteredCofactoredRelationArray,
3139	mdd_dup(cluster));
3140	}
3141	}
3142
3143
3144	/Function******************************************************************
3145
3146	Synopsis [Frees the clusteredcofactoredrelationarray]
3147
3148
3149	Description [Frees the clusteredCofactoredRelationArray, and the
3150	careSetArray, and sets them to NIL to signify that they are invalid.]
3151
3152	SideEffects []
3153
3154	******************************************************************************/
3155	static void
3156	FreeClusteredCofactoredRelationArray(
3157	Iwls95Info_t *info)
3158	{
3159	/* one should only be NIL if the other is, too */
3160	assert((info->bwdClusteredCofactoredRelationArray != NIL(array_t)) ==
3161	(info->careSetArray != NIL(array_t)));
3162
3163	if(info->bwdClusteredCofactoredRelationArray == NIL(array_t))
3164	return;
3165
3166	mdd_array_free(info->bwdClusteredCofactoredRelationArray);
3167	info->bwdClusteredCofactoredRelationArray = NIL(array_t);
3168	mdd_array_free(info->careSetArray);
3169	info->careSetArray = NIL(array_t);
3170	}
3171
3172
3173	/Function******************************************************************
3174
3175	Synopsis [Gets the necessary options for computing the image and returns
3176	in the option structure.]
3177
3178	Description [Gets the necessary options for computing the image and returns
3179	in the option structure.]
3180
3181	SideEffects []
3182
3183	******************************************************************************/
3184
3185	static ImgTrmOption_t *
3186	TrmGetOptions(void)
3187	{
3188	char *flagValue;
3189	ImgTrmOption_t *option;
3190
3191	option = ALLOC(ImgTrmOption_t, 1);
3192
3193	flagValue = Cmd_FlagReadByName("image_cluster_size");
3194	if (flagValue == NIL(char)) {
3195	option->clusterSize = 5000; /* the default value */
3196	}
3197	else {
3198	option->clusterSize = atoi(flagValue);
3199	}
3200
3201	flagValue = Cmd_FlagReadByName("image_verbosity");
3202	if (flagValue == NIL(char)) {
3203	option->verbosity = 0; /* the default value */
3204	}
3205	else {
3206	option->verbosity = atoi(flagValue);
3207	}
3208
3209	flagValue = Cmd_FlagReadByName("image_W1");
3210	if (flagValue == NIL(char)) {
3211	option->W1 = 6; /* the default value */
3212	}
3213	else {
3214	option->W1 = atoi(flagValue);
3215	}
3216
3217	flagValue = Cmd_FlagReadByName("image_W2");
3218	if (flagValue == NIL(char)) {
3219	option->W2 = 1; /* the default value */
3220	}
3221	else {
3222	option->W2 = atoi(flagValue);
3223	}
3224
3225	flagValue = Cmd_FlagReadByName("image_W3");
3226	if (flagValue == NIL(char)) {
3227	option->W3 = 1; /* the default value */
3228	}
3229	else {
3230	option->W3 = atoi(flagValue);
3231	}
3232
3233	flagValue = Cmd_FlagReadByName("image_W4");
3234	if (flagValue == NIL(char)) {
3235	option->W4 = 2; /* the default value */
3236	}
3237	else {
3238	option->W4 = atoi(flagValue);
3239	}
3240
3241	flagValue = Cmd_FlagReadByName("image_print_depend_matrix");
3242	if (flagValue == NIL(char)) {
3243	option->printDepMatrix = 0; /* the default value */
3244	}
3245	else {
3246	option->printDepMatrix = atoi(flagValue);
3247	}
3248
3249
3250	flagValue = Cmd_FlagReadByName("mlp_method");
3251	if (flagValue == NIL(char)) {
3252	option->mlpMethod = 0; /* the default value */
3253	}
3254	else {
3255	option->mlpMethod = atoi(flagValue);
3256	}
3257
3258	flagValue = Cmd_FlagReadByName("mlp_cluster");
3259	if (flagValue == NIL(char)) {
3260	option->mlpCluster = 1; /* the default value */
3261	}
3262	else {
3263	option->mlpCluster = atoi(flagValue);
3264	}
3265
3266	flagValue = Cmd_FlagReadByName("mlp_cluster_dynamic");
3267	if (flagValue == NIL(char)) {
3268	option->mlpClusterDynamic = 1; /* the default value */
3269	}
3270	else {
3271	option->mlpClusterDynamic = atoi(flagValue);
3272	}
3273
3274	flagValue = Cmd_FlagReadByName("mlp_affinity_threshold");
3275	if (flagValue == NIL(char)) {
3276	option->mlpAffinityThreshold = 0.0; /* the default value */
3277	}
3278	else {
3279	sscanf(flagValue, "%f", &option->mlpAffinityThreshold);
3280	}
3281
3282	flagValue = Cmd_FlagReadByName("mlp_cluster_quantify_vars");
3283	if (flagValue == NIL(char)) {
3284	option->mlpClusterQuantifyVars = 0; /* the default value */
3285	}
3286	else {
3287	option->mlpClusterQuantifyVars = atoi(flagValue);
3288	}
3289
3290	flagValue = Cmd_FlagReadByName("mlp_cluster_sorted_list");
3291	if (flagValue == NIL(char)) {
3292	option->mlpClusterSortedList = 1; /* the default value */
3293	}
3294	else {
3295	option->mlpClusterSortedList = atoi(flagValue);
3296	}
3297
3298	flagValue = Cmd_FlagReadByName("mlp_initial_cluster");
3299	if (flagValue == NIL(char)) {
3300	option->mlpInitialCluster = 0; /* the default value */
3301	}
3302	else {
3303	option->mlpInitialCluster = atoi(flagValue);
3304	}
3305
3306	flagValue = Cmd_FlagReadByName("mlp_cs_first");
3307	if (flagValue == NIL(char)) {
3308	option->mlpCsFirst = 0; /* the default value */
3309	}
3310	else {
3311	option->mlpCsFirst = atoi(flagValue);
3312	}
3313
3314	flagValue = Cmd_FlagReadByName("mlp_skip_rs");
3315	if (flagValue == NIL(char)) {
3316	option->mlpSkipRs = 0; /* the default value */
3317	}
3318	else {
3319	option->mlpSkipRs = atoi(flagValue);
3320	}
3321
3322	flagValue = Cmd_FlagReadByName("mlp_skip_cs");
3323	if (flagValue == NIL(char)) {
3324	option->mlpSkipCs = 1; /* the default value */
3325	}
3326	else {
3327	option->mlpSkipCs = atoi(flagValue);
3328	}
3329
3330	flagValue = Cmd_FlagReadByName("mlp_row_based");
3331	if (flagValue == NIL(char)) {
3332	option->mlpRowBased = 0; /* the default value */
3333	}
3334	else {
3335	option->mlpRowBased = atoi(flagValue);
3336	}
3337
3338	flagValue = Cmd_FlagReadByName("mlp_reorder");
3339	if (flagValue == NIL(char)) {
3340	option->mlpReorder = 0; /* the default value */
3341	}
3342	else {
3343	option->mlpReorder = atoi(flagValue);
3344	}
3345
3346	flagValue = Cmd_FlagReadByName("mlp_pre_reorder");
3347	if (flagValue == NIL(char)) {
3348	option->mlpPreReorder = 0; /* the default value */
3349	}
3350	else {
3351	option->mlpPreReorder = atoi(flagValue);
3352	}
3353
3354	flagValue = Cmd_FlagReadByName("mlp_postprocess");
3355	if (flagValue == NIL(char)) {
3356	option->mlpPostProcess = 0; /* the default value */
3357	}
3358	else {
3359	option->mlpPostProcess = atoi(flagValue);
3360	}
3361
3362	flagValue = Cmd_FlagReadByName("mlp_decompose_scc");
3363	if (flagValue == NIL(char)) {
3364	option->mlpDecomposeScc = 1; /* the default value */
3365	}
3366	else {
3367	option->mlpDecomposeScc = atoi(flagValue);
3368	}
3369
3370	flagValue = Cmd_FlagReadByName("mlp_cluster_scc");
3371	if (flagValue == NIL(char)) {
3372	option->mlpClusterScc = 1; /* the default value */
3373	}
3374	else {
3375	option->mlpClusterScc = atoi(flagValue);
3376	}
3377
3378	flagValue = Cmd_FlagReadByName("mlp_sort_scc");
3379	if (flagValue == NIL(char)) {
3380	option->mlpSortScc = 1; /* the default value */
3381	}
3382	else {
3383	option->mlpSortScc = atoi(flagValue);
3384	}
3385
3386	flagValue = Cmd_FlagReadByName("mlp_sort_scc_mode");
3387	if (flagValue == NIL(char)) {
3388	option->mlpSortSccMode = 2; /* the default value */
3389	}
3390	else {
3391	option->mlpSortSccMode = atoi(flagValue);
3392	}
3393
3394	flagValue = Cmd_FlagReadByName("mlp_cluster_merge");
3395	if (flagValue == NIL(char)) {
3396	option->mlpClusterMerge = 0; /* the default value */
3397	}
3398	else {
3399	option->mlpClusterMerge = atoi(flagValue);
3400	}
3401
3402	flagValue = Cmd_FlagReadByName("mlp_multiway");
3403	if (flagValue == NIL(char)) {
3404	option->mlpMultiway = 0; /* the default value */
3405	}
3406	else {
3407	option->mlpMultiway = atoi(flagValue);
3408	}
3409
3410	flagValue = Cmd_FlagReadByName("mlp_lambda_mode");
3411	if (flagValue == NIL(char)) {
3412	option->mlpLambdaMode = 0; /* the default value */
3413	}
3414	else {
3415	option->mlpLambdaMode = atoi(flagValue);
3416	}
3417
3418	flagValue = Cmd_FlagReadByName("mlp_sorted_rows");
3419	if (flagValue == NIL(char)) {
3420	option->mlpSortedRows = 1; /* the default value */
3421	}
3422	else {
3423	option->mlpSortedRows = atoi(flagValue);
3424	}
3425
3426	flagValue = Cmd_FlagReadByName("mlp_sorted_cols");
3427	if (flagValue == NIL(char)) {
3428	option->mlpSortedCols = 1; /* the default value */
3429	}
3430	else {
3431	option->mlpSortedCols = atoi(flagValue);
3432	}
3433
3434	flagValue = Cmd_FlagReadByName("mlp_pre_swap_state_vars");
3435	if (flagValue == NIL(char)) {
3436	option->mlpPreSwapStateVars = 0; /* the default value */
3437	}
3438	else {
3439	option->mlpPreSwapStateVars = atoi(flagValue);
3440	}
3441
3442	flagValue = Cmd_FlagReadByName("mlp_print_matrix");
3443	if (flagValue == NIL(char)) {
3444	option->mlpPrintMatrix = 0; /* the default value */
3445	}
3446	else {
3447	option->mlpPrintMatrix = atoi(flagValue);
3448	}
3449
3450	flagValue = Cmd_FlagReadByName("mlp_write_order");
3451	if (flagValue == NIL(char)) {
3452	option->mlpWriteOrder = NIL(char); /* the default value */
3453	}
3454	else {
3455	option->mlpWriteOrder = util_strsav(flagValue);
3456	}
3457
3458	flagValue = Cmd_FlagReadByName("mlp_verbosity");
3459	if (flagValue == NIL(char)) {
3460	option->mlpVerbosity = 0; /* the default value */
3461	}
3462	else {
3463	option->mlpVerbosity = atoi(flagValue);
3464	}
3465
3466	flagValue = Cmd_FlagReadByName("mlp_debug");
3467	if (flagValue == NIL(char)) {
3468	option->mlpDebug = 0; /* the default value */
3469	}
3470	else {
3471	option->mlpDebug = atoi(flagValue);
3472	}
3473
3474	flagValue = Cmd_FlagReadByName("image_read_reorder_cluster");
3475	if (flagValue == NIL(char)) {
3476	option->readReorderCluster = 0; /* the default value */
3477	}
3478	else {
3479	option->readReorderCluster = atoi(flagValue);
3480	}
3481
3482	flagValue = Cmd_FlagReadByName("image_read_cluster");
3483	if (flagValue == NIL(char)) {
3484	option->readCluster = NIL(char); /* the default value */
3485	}
3486	else {
3487	option->readCluster = util_strsav(flagValue);
3488	}
3489
3490	flagValue = Cmd_FlagReadByName("image_write_cluster");
3491	if (flagValue == NIL(char)) {
3492	option->writeCluster = NIL(char); /* the default value */
3493	}
3494	else {
3495	option->writeCluster = util_strsav(flagValue);
3496	}
3497
3498	flagValue = Cmd_FlagReadByName("image_write_depend_matrix");
3499	if (flagValue == NIL(char)) {
3500	option->writeDepMatrix = NIL(char); /* the default value */
3501	}
3502	else {
3503	option->writeDepMatrix = util_strsav(flagValue);
3504	}
3505
3506	flagValue = Cmd_FlagReadByName("linear_grain_type");
3507	if (flagValue == NIL(char)) {
3508	option->linearFineGrainFlag = 0; /* the default value */
3509	}
3510	else {
3511	option->linearFineGrainFlag = 1;
3512	}
3513
3514	flagValue = Cmd_FlagReadByName("linear_optimize");
3515	if (flagValue == NIL(char)) {
3516	option->linearOptimize = Opt_None; /* the default value */
3517	}
3518	else {
3519	option->linearOptimize = Opt_NS;
3520	}
3521
3522	option->linearOrderVariable = 0;
3523	flagValue = Cmd_FlagReadByName("linear_order_variable");
3524	if (flagValue == NIL(char)) {
3525	option->linearOrderVariable = 0; /* the default value */
3526	}
3527	else {
3528	option->linearOrderVariable = 1;
3529	}
3530
3531	option->linearGroupStateVariable = 0;
3532	flagValue = Cmd_FlagReadByName("linear_group_state_variable");
3533	if (flagValue == NIL(char)) {
3534	option->linearGroupStateVariable = 0; /* the default value */
3535	}
3536	else {
3537	option->linearGroupStateVariable = 1;
3538	}
3539
3540	option->linearIncludeCS = 1;
3541	option->linearIncludeNS = 1;
3542	option->linearQuantifyCS = 0;
3543	option->linearComputeRange = 0;
3544	flagValue = Cmd_FlagReadByName("linear_exclude_cs");
3545	if (flagValue) option->linearIncludeCS = 0;
3546	flagValue = Cmd_FlagReadByName("linear_exclude_ns");
3547	if (flagValue) option->linearIncludeNS = 0;
3548
3549	return option;
3550	}
3551
3552	/Function******************************************************************
3553
3554	Synopsis [Creates the bit relations and the mdd id array for the
3555	quantifiable variables and stores it in the ImgIwls95
3556	structure. ]
3557
3558	Description [Creates the bit relations and the mdd id array for the
3559	quantifiable variables and stores it in the ImgIwls95
3560	structure. This is identical to the initialize procedure. Read the
3561	roots (next state mdds), compute the bit relations for each root. If
3562	there are some intermediate variables, add them to quantifiable
3563	vars. ]
3564
3565	SideEffects [bitRelationArray and quantifyVarMddIdArray fields are
3566	modified of the Iwls95Info_t struct.]
3567
3568	SeeAlso [ImgImageInfoInitializeIwls95]
3569
3570	******************************************************************************/
3571
3572	static void
3573	CreateBitRelationArray(Iwls95Info_t info, ImgFunctionData_t functionData)
3574	{
3575	array_t *bddRelationArray = NIL(array_t);
3576	array_t *domainVarMddIdArray = functionData->domainVars;
3577	array_t *rangeVarMddIdArray = functionData->rangeVars;
3578	array_t *quantifyVarMddIdArray = NIL(array_t);
3579	graph_t *mddNetwork = functionData->mddNetwork;
3580	array_t *roots = functionData->roots;
3581	int i;
3582	int n1, n2, nIntermediateVars = 0;
3583	mdd_manager *mddManager = NIL(mdd_manager);
3584	st_table *vertexTable = NIL(st_table);
3585	st_table *domainQuantifyVarMddIdTable = NIL(st_table);
3586	int mddId;
3587	char *nodeName;
3588
3589	if (info->bitRelationArray != NIL(array_t)) {
3590	assert(info->quantifyVarMddIdArray != NIL(array_t));
3591	return;
3592	}
3593
3594	bddRelationArray = array_alloc(mdd_t*, 0);
3595	quantifyVarMddIdArray = array_dup(functionData->quantifyVars);
3596	mddManager = Part_PartitionReadMddManager(mddNetwork);
3597	vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
3598	domainQuantifyVarMddIdTable = st_init_table(st_numcmp, st_numhash);
3599
3600	arrayForEachItem(int, domainVarMddIdArray, i, mddId) {
3601	st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
3602	}
3603	arrayForEachItem(int, quantifyVarMddIdArray, i, mddId) {
3604	st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
3605	}
3606
3607	arrayForEachItem(char *, roots, i, nodeName) {
3608	vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName);
3609	Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
3610	int mddId = array_fetch(int, rangeVarMddIdArray, i);
3611
3612	/mdd_t relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);*/
3613	array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager,
3614	mddId, mvf);
3615	array_append(bddRelationArray, varBddRelationArray);
3616	array_free(varBddRelationArray);
3617	/array_insert_last(mdd_t , bddRelationArray, relation);*/
3618	if (info->option->verbosity)
3619	n1 = array_n(bddRelationArray);
3620	else /* to remove uninitialized variable warning */
3621	n1 = 0;
3622	PartitionTraverseRecursively(mddManager, vertex, -1, vertexTable,
3623	bddRelationArray,
3624	domainQuantifyVarMddIdTable,
3625	quantifyVarMddIdArray);
3626	if (info->option->verbosity) {
3627	n2 = array_n(bddRelationArray);
3628	nIntermediateVars += n2 - n1;
3629	}
3630	}
3631	if (info->option->verbosity) {
3632	(void)fprintf(vis_stdout, "** img info: %d intermediate variables\n",
3633	nIntermediateVars);
3634	}
3635	st_free_table(vertexTable);
3636	st_free_table(domainQuantifyVarMddIdTable);
3637	info->bitRelationArray = bddRelationArray;
3638	info->quantifyVarMddIdArray = quantifyVarMddIdArray;
3639	return;
3640
3641	}
3642
3643	/Function******************************************************************
3644
3645	Synopsis [Frees bit relation array and the quantification variables.]
3646
3647
3648	Description [Frees bit relation array and quantification
3649	variables. Important: to set these field to NIL in case of reuse.]
3650
3651	SideEffects [Also frees the quantifVarMddIdArray field.]
3652	******************************************************************************/
3653	static void
3654	FreeBitRelationArray (Iwls95Info_t *info)
3655	{
3656	mdd_array_free(info->bitRelationArray);
3657	info->bitRelationArray = NIL(array_t);
3658	return;
3659	}
3660
3661
3662
3663	/Function******************************************************************
3664
3665	Synopsis [Takes an array of relations and does order, cluster,
3666	order on it according to the IWLS95 method. This forms a
3667	heuristically optimized clustered transition relation, plus a
3668	quantification schedule that goes with it.]
3669
3670	Description [Takes an array of relations and does order,
3671	cluster, order on it. This forms a heuristically optimized clustered
3672	transition relation, plus a quantification schedule that goes with
3673	it. Requires the relation array, quantify variables, a
3674	"from" variable array (contained in the quantify variables), a "to"
3675	variable array and direction of computation (image or
3676	preimage). Eventually orderedClusteredRelationArray holds an
3677	ordered-clustered-ordered version of the relationArray and
3678	smoothVarBddArrayPtr holds the quantification schedule that goes
3679	with orderClusteredRelationArray. If the freeRelationArray flag is
3680	set, the relationArray is freed. This code is identical to
3681	ImgInfoInitialize.]
3682
3683	SideEffects [The existing contents of
3684	orderedClusteredRelationArrayPtr or smoothVarBddArrayPtr are lost
3685	(not freed). relationArray is freed if the freeRelationArray flag
3686	is set.]
3687
3688	SeeAlso [ImgImageInfoInitializeIwls95]
3689
3690	******************************************************************************/
3691	static void
3692	OrderClusterOrder(mdd_manager *mddManager,
3693	array_t *relationArray,
3694	array_t *fromVarBddArray,
3695	array_t *toVarBddArray,
3696	array_t *quantifyVarBddArray,
3697	array_t **orderedClusteredRelationArrayPtr,
3698	array_t **smoothVarBddArrayPtr,
3699	ImgTrmOption_t *option,
3700	boolean freeRelationArray)
3701	{
3702	array_t clusteredRelationArray; /clustered version of orderedRelationArray*/
3703
3704	/*
3705	* Since clusters are formed by multiplying the latches starting
3706	* from one end we need to order the latches using some heuristics
3707	* first. Right now, we order the latches using the same heuristic
3708	* as the one used for ordering the clusters for early quantifiction.
3709	* However, since we are not interested in the quantification
3710	* schedule at this stage, we will pass a NIL(array_t*) as the last
3711	* argument.
3712	*/
3713	*orderedClusteredRelationArrayPtr = NIL(array_t);
3714	OrderRelationArray(mddManager, relationArray, fromVarBddArray,
3715	quantifyVarBddArray, toVarBddArray, option,
3716	orderedClusteredRelationArrayPtr, NIL(array_t *));
3717
3718	/* free relationArray if told to */
3719	if (freeRelationArray) mdd_array_free(relationArray);
3720
3721
3722	/* Create the clusters */
3723	clusteredRelationArray = CreateClusters(mddManager,
3724	*orderedClusteredRelationArrayPtr,
3725	option);
3726
3727	/* Free the orderedRelationArray */
3728	mdd_array_free(*orderedClusteredRelationArrayPtr);
3729
3730	/* Order the clusters for image and pre-image computation. */
3731	OrderRelationArray(mddManager, clusteredRelationArray, fromVarBddArray,
3732	quantifyVarBddArray, toVarBddArray, option,
3733	orderedClusteredRelationArrayPtr, smoothVarBddArrayPtr);
3734	/* Free the clusteredRelationArray. */
3735	mdd_array_free(clusteredRelationArray);
3736	}
3737
3738
3739	/Function******************************************************************
3740
3741	Synopsis [Forms the clusters of relations based on BDD size heuristic.]
3742
3743	Description [The clusters are formed by taking the product in order. Once the
3744	BDD size of the cluster reaches a threshold, a new cluster is
3745	started.]
3746
3747	SideEffects []
3748	******************************************************************************/
3749
3750	static array_t *
3751	CreateClusters(bdd_manager bddManager, array_t relationArray,
3752	ImgTrmOption_t *option)
3753	{
3754	array_t *clusterArray;
3755	int i;
3756	bdd_t cluster, relation, *tempCluster;
3757	int flag;
3758	int size;
3759
3760	clusterArray = array_alloc(bdd_t *, 0);
3761
3762	for (i=0; i<array_n(relationArray);) {
3763	cluster = bdd_one(bddManager);
3764	flag = 0;
3765	do{
3766	relation = array_fetch(bdd_t *,relationArray, i);
3767	i++;
3768	tempCluster = bdd_and_with_limit(cluster, relation, 1, 1,
3769	option->clusterSize);
3770	assert(flag \|\| tempCluster != NIL(mdd_t));
3771	if (tempCluster != NIL(mdd_t)) {
3772	size = bdd_size(tempCluster);
3773	if (size <= option->clusterSize \|\| flag == 0) {
3774	bdd_free(cluster);
3775	cluster = tempCluster;
3776	if (flag == 0 && size >= option->clusterSize)
3777	break;
3778	flag = 1;
3779	}
3780	else{
3781	bdd_free(tempCluster);
3782	i--;
3783	break;
3784	}
3785	}
3786	else {
3787	i--;
3788	break;
3789	}
3790	} while (i < array_n(relationArray));
3791	array_insert_last(bdd_t *, clusterArray, cluster);
3792	}
3793	return clusterArray;
3794	}
3795
3796	/Function******************************************************************
3797
3798	Synopsis [Returns an array of ordered relations and an array
3799	of BDD cubes (array of BDDs).]
3800
3801	Description [This function returns an array of ordered relations and an array
3802	of BDD cubes (array of BDDs).
3803	This consists of following steps:
3804	a. Initialize the array of ctrInfoStructs and varInfoStructs.
3805	b. Fill in the list of varItemStruct's of ctrInfo's and
3806	ctrItemStruct's of varInfo's.
3807	c. Simplify the relations by quantifying out the quantify
3808	variables local to a particular relation.
3809	d. Order the relations according to the cost function described
3810	in "CalculateRelationBenefit".]
3811	SideEffects []
3812
3813	******************************************************************************/
3814	static void
3815	OrderRelationArray(mdd_manager *mddManager,
3816	array_t *relationArray,
3817	array_t *domainVarBddArray,
3818	array_t *quantifyVarBddArray,
3819	array_t *rangeVarBddArray,
3820	ImgTrmOption_t *option,
3821	array_t **orderedRelationArrayPtr,
3822	array_t **arraySmoothVarBddArrayPtr)
3823	{
3824	array_t quantifyVarBddIdArray, domainVarBddIdArray, *rangeVarBddIdArray;
3825	array_t *domainAndQuantifyVarBddArray;
3826	array_t ctrInfoArray, varInfoArray, *simplifiedRelationArray;
3827	array_t *sortedMaxIndexArray;
3828	array_t *arrayDomainQuantifyVarsWithZeroNumCtr = NIL(array_t);
3829	int numRelation, numDomainVars, numQuantifyVars, numRangeVars;
3830	int numSmoothVars, numVars;
3831	int bddId;
3832	int i;
3833	int *sortedMaxIndexVector;
3834	int numSmoothVarsRemaining, numIntroducedVarsRemaining;
3835	st_table bddIdToVarInfoTable, bddIdToBddTable;
3836	bdd_t relation, bdd;
3837	CtrInfo_t *ctrInfo;
3838	VarInfo_t *varInfo;
3839	lsList remainingCtrInfoList;
3840
3841	numRelation = array_n(relationArray);
3842	numDomainVars = array_n(domainVarBddArray);
3843	numRangeVars = array_n(rangeVarBddArray);
3844	numQuantifyVars = array_n(quantifyVarBddArray);
3845	numSmoothVars = numDomainVars + numQuantifyVars;
3846	numVars = numSmoothVars + numRangeVars;
3847
3848	domainVarBddIdArray = bdd_get_varids(domainVarBddArray);
3849	rangeVarBddIdArray = bdd_get_varids(rangeVarBddArray);
3850	quantifyVarBddIdArray = bdd_get_varids(quantifyVarBddArray);
3851	domainAndQuantifyVarBddArray = array_join(domainVarBddArray,
3852	quantifyVarBddArray);
3853
3854	bddIdToBddTable = st_init_table(st_numcmp, st_numhash);
3855	HashIdToBddTable(bddIdToBddTable, domainVarBddIdArray, domainVarBddArray);
3856	HashIdToBddTable(bddIdToBddTable, quantifyVarBddIdArray, quantifyVarBddArray);
3857	HashIdToBddTable(bddIdToBddTable, rangeVarBddIdArray, rangeVarBddArray);
3858
3859	bddIdToVarInfoTable = st_init_table(st_numcmp, st_numhash);
3860
3861	/*
3862	* Create the array of ctrInfo's for each component
3863	*/
3864	ctrInfoArray = array_alloc(CtrInfo_t*, 0);
3865	varInfoArray = array_alloc(VarInfo_t*, 0);
3866
3867	/*
3868	* Create the array of varInfo for each variable
3869	*/
3870	for (i=0; i<numVars; i++) {
3871	varInfo = VarInfoStructAlloc();
3872	if (i<numDomainVars) {
3873	bddId = array_fetch(int, domainVarBddIdArray, i);
3874	varInfo->varType = domainVar_c;
3875	}
3876	else if (i < (numDomainVars+numQuantifyVars)) {
3877	bddId = array_fetch(int, quantifyVarBddIdArray, i-numDomainVars);
3878	varInfo->varType = quantifyVar_c;
3879	}
3880	else{
3881	bddId = array_fetch(int, rangeVarBddIdArray,
3882	(i-(numDomainVars+numQuantifyVars)));
3883	varInfo->varType = rangeVar_c;
3884	}
3885	array_insert_last(VarInfo_t*, varInfoArray, varInfo);
3886	varInfo->bddId = bddId;
3887	st_insert(bddIdToVarInfoTable, (char )(long) bddId, (char )varInfo);
3888	}
3889
3890	/*
3891	* Fill in the data structure of the ctrInfo and varInfo
3892	*/
3893	for (i=0; i<numRelation; i++) {
3894	st_table *supportTable;
3895	st_generator *stGen;
3896	VarItem_t *varItem;
3897	CtrItem_t *ctrItem;
3898	lsHandle varItemHandle, ctrItemHandle;
3899	long varId;
3900
3901	ctrInfo = CtrInfoStructAlloc();
3902	array_insert_last(CtrInfo_t*, ctrInfoArray, ctrInfo);
3903	ctrInfo->ctrId = i;
3904	relation = array_fetch(bdd_t*, relationArray, i);
3905	supportTable = ImgBddGetSupportIdTable(relation);
3906	st_foreach_item(supportTable, stGen, &varId, NULL) {
3907	varInfo = NIL(VarInfo_t);
3908	if (st_lookup(bddIdToVarInfoTable, (char *) varId, &varInfo) == 0) {
3909	/* This variable is of no interest, because it is not present
3910	* in the bddIdToVarInfoTable.
3911	*/
3912	continue;
3913	}
3914	varItem = ALLOC(VarItem_t,1);
3915	varItem->varInfo = varInfo;
3916	(void) lsNewBegin(ctrInfo->varItemList, (lsGeneric)varItem,
3917	(lsHandle *)&varItemHandle);
3918	ctrItem = ALLOC(CtrItem_t,1);
3919	ctrItem->ctrInfo = ctrInfo;
3920	(void) lsNewBegin(varInfo->ctrItemList, (lsGeneric)ctrItem,
3921	(lsHandle *)&ctrItemHandle);
3922	varItem->ctrItemHandle = ctrItemHandle;
3923	ctrItem->varItemHandle = varItemHandle;
3924	varInfo->numCtr++;
3925	}
3926	st_free_table(supportTable);
3927	} /* Initialization of ctrInfoArray and varInfoArray complete */
3928
3929	/*
3930	* Smooth out the quantify variables which are local to a particular cluster.
3931	*/
3932	simplifiedRelationArray = RelationArraySmoothLocalVars(relationArray,
3933	ctrInfoArray,
3934	varInfoArray,
3935	bddIdToBddTable);
3936
3937	assert(CheckCtrInfoArray(ctrInfoArray, numDomainVars, numQuantifyVars,
3938	numRangeVars));
3939	assert(CheckVarInfoArray(varInfoArray, numRelation));
3940
3941	/*
3942	* In the ordering scheme of clusters, the number of variables yet to be
3943	* quantified out and number of variables which are yet to be introduced is
3944	* taken into account. The number of smooth variables which are yet to be
3945	* quantified out could have changed. Also some of the range variables may
3946	* not be in the support of any of the clusters. This can happen while doing
3947	* the ordering for clusters for backward image (when a present state
3948	* variable does not appear in the support of any of the next state
3949	* functions. Recalculate these numbers. */
3950
3951	numSmoothVarsRemaining = numSmoothVars;
3952	numIntroducedVarsRemaining = numRangeVars;
3953
3954	/*
3955	* Find out which variables do not appear in the support of any cluster.
3956	* Update the numSmoothVarsRemaining and numIntroducedVarsRemaining
3957	* accordingly.
3958	* Also, these domainVars and quantifyVars can be quantified out as soon as
3959	* possible.
3960	*/
3961	if (arraySmoothVarBddArrayPtr != NIL(array_t *))
3962	arrayDomainQuantifyVarsWithZeroNumCtr = array_alloc(bdd_t*, 0);
3963	for (i=0; i<numVars; i++) {
3964	varInfo = array_fetch(VarInfo_t*, varInfoArray, i);
3965	if (varInfo->numCtr == 0) {
3966	if ((varInfo->varType == domainVar_c) \|\|
3967	(varInfo->varType == quantifyVar_c)) {
3968	numSmoothVarsRemaining--;
3969	if (arraySmoothVarBddArrayPtr != NIL(array_t *)) {
3970	st_lookup(bddIdToBddTable, (char *)(long)varInfo->bddId, &bdd);
3971	array_insert_last(bdd_t*, arrayDomainQuantifyVarsWithZeroNumCtr,
3972	bdd_dup(bdd));
3973	}
3974	}
3975	else numIntroducedVarsRemaining--;
3976	}
3977	}
3978
3979	/*
3980	* The ordering scheme also depends on the value of the maximum index of a
3981	* smooth variable which is yet to be quantified. For efficiency reasons, we
3982	* maintain a vector indicating the maximum index of the clusters. This
3983	* vector is sorted in the decreasing order of index. The rank of a cluster
3984	* is stored in its "rankMaxSmoothVarIndex" field.
3985	*/
3986	sortedMaxIndexArray = array_dup(ctrInfoArray);
3987	array_sort(sortedMaxIndexArray, CtrInfoMaxIndexCompare);
3988	sortedMaxIndexVector = ALLOC(int, numRelation);
3989	for (i=0; i<numRelation; i++) {
3990	ctrInfo = array_fetch(CtrInfo_t*, sortedMaxIndexArray, i);
3991	ctrInfo->rankMaxSmoothVarIndex = i;
3992	sortedMaxIndexVector[i] = ctrInfo->maxSmoothVarIndex;
3993	}
3994	array_free(sortedMaxIndexArray);
3995
3996	/*
3997	* Create a list of clusters which are yet to be ordered. Right now
3998	* put all the clusters. Later on the list will contain only those
3999	* clusters which have not yet been ordered.
4000	*/
4001	remainingCtrInfoList = lsCreate();
4002	for(i=0; i<numRelation; i++) {
4003	lsHandle ctrHandle;
4004	ctrInfo = array_fetch(CtrInfo_t*, ctrInfoArray, i);
4005	lsNewBegin(remainingCtrInfoList, (lsGeneric)ctrInfo, &ctrHandle);
4006	ctrInfo->ctrInfoListHandle = ctrHandle;
4007	}
4008
4009	/* Call the auxiliary routine to do the ordering. */
4010	OrderRelationArrayAux(simplifiedRelationArray, remainingCtrInfoList,
4011	ctrInfoArray, varInfoArray, sortedMaxIndexVector,
4012	numSmoothVarsRemaining, numIntroducedVarsRemaining,
4013	bddIdToBddTable, option, domainAndQuantifyVarBddArray,
4014	orderedRelationArrayPtr, arraySmoothVarBddArrayPtr,
4015	arrayDomainQuantifyVarsWithZeroNumCtr);
4016
4017	lsDestroy(remainingCtrInfoList,0);
4018
4019	/* Free the info arrays */
4020
4021	for (i=0; i<numRelation; i++) {
4022	ctrInfo = array_fetch(CtrInfo_t*, ctrInfoArray, i);
4023	CtrInfoStructFree(ctrInfo);
4024	}
4025	array_free(ctrInfoArray);
4026
4027	for (i=0; i<numVars; i++) {
4028	varInfo = array_fetch(VarInfo_t*, varInfoArray, i);
4029	assert(varInfo->numCtr == 0);
4030	VarInfoStructFree(varInfo);
4031	}
4032	array_free(varInfoArray);
4033
4034	if (option->verbosity >= 3) {
4035	int numRelation = array_n(*orderedRelationArrayPtr);
4036
4037	if (arraySmoothVarBddArrayPtr != NIL(array_t*)) {
4038	PrintSmoothIntroducedCount(*orderedRelationArrayPtr,
4039	arraySmoothVarBddArrayPtr,
4040	domainVarBddIdArray,
4041	rangeVarBddIdArray);
4042	}
4043	if (option->verbosity >= 4) {
4044	for (i= 0; i <numRelation; i++) {
4045	st_table *supportTable;
4046	(void) fprintf(vis_stdout, "Cluster # %d\n",i);
4047	supportTable = ImgBddGetSupportIdTable(
4048	array_fetch(bdd_t, orderedRelationArrayPtr, i));
4049	PrintBddIdTable(supportTable);
4050	if (arraySmoothVarBddArrayPtr != NIL(array_t*)) {
4051	(void) fprintf(vis_stdout, "Exist cube # %d\n",i);
4052	PrintBddIdFromBddArray(array_fetch(array_t*,
4053	*arraySmoothVarBddArrayPtr, i));
4054	}
4055	}
4056	}
4057	}
4058	FREE(sortedMaxIndexVector);
4059	array_free(simplifiedRelationArray);
4060
4061	/* Free BDD Id arrays */
4062	array_free(domainVarBddIdArray);
4063	array_free(quantifyVarBddIdArray);
4064	array_free(rangeVarBddIdArray);
4065	array_free(domainAndQuantifyVarBddArray);
4066	/* Free the st_tables */
4067	st_free_table(bddIdToBddTable);
4068	st_free_table(bddIdToVarInfoTable);
4069	}
4070
4071	/Function******************************************************************
4072
4073	Synopsis [This function takes an array of relations and quantifies out the
4074	quantify variables which are local to a particular relation.]
4075
4076	Description [This function takes an array of relations and quantifies out the
4077	quantify variables which are local to a particular relation.]
4078
4079	SideEffects [This function fills in the "numSmoothVars",
4080	"numLocalSmoothVars", "numIntroducedVars", "maxSmoothVarIndex"
4081	fields of ctrInfoStruct corresponding to each relation. It also
4082	alters the "numCtr" and "ctrItemList" field of those quantify
4083	variables which are quantified out in this function.]
4084
4085	******************************************************************************/
4086
4087	static array_t *
4088	RelationArraySmoothLocalVars(array_t relationArray, array_t ctrInfoArray,
4089	array_t *varInfoArray,
4090	st_table *bddIdToBddTable)
4091	{
4092	array_t arraySmoothVarBddArray, smoothVarBddArray;
4093	array_t *simplifiedRelationArray;
4094	bdd_t simplifiedRelation, relation, *varBdd;
4095	int maxSmoothVarIndexForAllCtr, i, numRelation;
4096
4097	numRelation = array_n(relationArray);
4098
4099	/*
4100	* Initialize the array of cubes (of quantified variables which occur in
4101	* only one relation), to be smoothed out.
4102	*/
4103	arraySmoothVarBddArray = array_alloc(array_t*, 0);
4104	for (i=0; i<numRelation; i++) {
4105	smoothVarBddArray = array_alloc(bdd_t*, 0);
4106	array_insert_last(array_t*, arraySmoothVarBddArray, smoothVarBddArray);
4107	}
4108
4109	maxSmoothVarIndexForAllCtr = -1;
4110	for (i=0; i<numRelation; i++) {
4111	VarItem_t *varItem;
4112	lsHandle varItemHandle;
4113	CtrInfo_t ctrInfo = array_fetch(CtrInfo_t, ctrInfoArray, i);
4114	int maxSmoothVarIndex = -1;
4115	lsGen varItemListGen = lsStart(ctrInfo->varItemList);
4116
4117	smoothVarBddArray = array_fetch(array_t *, arraySmoothVarBddArray, i);
4118	while (lsNext(varItemListGen, &varItem, &varItemHandle) ==
4119	LS_OK) {
4120	int varBddId;
4121	VarInfo_t *varInfo = varItem->varInfo;
4122	if (varInfo->varType == rangeVar_c) {
4123	ctrInfo->numIntroducedVars++;
4124	}
4125	else if (varInfo->numCtr == 1) {
4126	assert(lsLength(varInfo->ctrItemList) == 1);
4127	if (varInfo->varType == quantifyVar_c) {
4128	/*
4129	* The variable can be smoothed out.
4130	* Put it in an array of variables to be
4131	* smoothed out from the relation.
4132	*/
4133	CtrItem_t *ctrItem;
4134	varBddId = varInfo->bddId;
4135	st_lookup(bddIdToBddTable, (char *)(long)varBddId,&varBdd);
4136	array_insert_last(bdd_t*, smoothVarBddArray, bdd_dup(varBdd));
4137	varInfo->numCtr = 0;
4138	/* Remove the cluster from the ctrItemList of varInfo */
4139	lsRemoveItem(varItem->ctrItemHandle, &ctrItem);
4140	CtrItemStructFree(ctrItem);
4141	/* Remove the variable from the varItemList of ctrInfo.*/
4142	lsRemoveItem(varItemHandle, &varItem);
4143	VarItemStructFree(varItem);
4144	continue;
4145	}
4146	else {
4147	/* Increase the numLocalSmoothVars count of the corresponding ctr. */
4148	ctrInfo->numLocalSmoothVars++;
4149	ctrInfo->numSmoothVars++;
4150	if (maxSmoothVarIndex < varInfo->bddId) {
4151	maxSmoothVarIndex = varInfo->bddId;
4152	}
4153	}
4154	}
4155	else{ /* varInfo->numCtr > 1 */
4156	assert(varInfo->numCtr > 1);
4157	ctrInfo->numSmoothVars++;
4158	if (maxSmoothVarIndex < varInfo->bddId) {
4159	maxSmoothVarIndex = varInfo->bddId;
4160	}
4161	}
4162	}
4163	lsFinish(varItemListGen);
4164	if (maxSmoothVarIndex >= 0) {
4165	ctrInfo->maxSmoothVarIndex = maxSmoothVarIndex;
4166	}
4167	else{
4168	ctrInfo->maxSmoothVarIndex = 0;
4169	}
4170	if (maxSmoothVarIndexForAllCtr < maxSmoothVarIndex) {
4171	maxSmoothVarIndexForAllCtr = maxSmoothVarIndex;
4172	}
4173	}
4174
4175	/*
4176	* Initialization Finished. We need to smooth out those quantify
4177	* variables which appear in only one ctr.
4178	*/
4179	simplifiedRelationArray = array_alloc(bdd_t*, 0);
4180	for (i=0; i<numRelation; i++) {
4181	relation = array_fetch(bdd_t*, relationArray, i);
4182	smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i);
4183	if (array_n(smoothVarBddArray) != 0)
4184	simplifiedRelation = bdd_smooth(relation, smoothVarBddArray);
4185	else
4186	simplifiedRelation = bdd_dup(relation);
4187	array_insert_last(bdd_t*, simplifiedRelationArray, simplifiedRelation);
4188	}
4189	mdd_array_array_free(arraySmoothVarBddArray);
4190	return simplifiedRelationArray;
4191	}
4192
4193	/Function******************************************************************
4194
4195	Synopsis [An auxiliary routine for orderRelationArray to order the
4196	clusters.]
4197
4198	Description [This routine is called by orderRelationArray after the
4199	initialization is complete and the cluster relations are simplified wrt to
4200	the quantify variable local to the cluster. The algorithm is:
4201	While (there exists a cluster to be ordered) {
4202	Calculate benefit for each unordered cluster.
4203	Choose the cluster with the maximum benefit.
4204	Update the cost function parameters.
4205	}
4206	]
4207
4208	SideEffects [ctrInfo and varInfo structures are modified.]
4209
4210	******************************************************************************/
4211	static void
4212	OrderRelationArrayAux(array_t *relationArray,
4213	lsList remainingCtrInfoList,
4214	array_t *ctrInfoArray,
4215	array_t *varInfoArray,
4216	int *sortedMaxIndexVector,
4217	int numSmoothVarsRemaining,
4218	int numIntroducedVarsRemaining,
4219	st_table *bddIdToBddTable,
4220	ImgTrmOption_t *option,
4221	array_t *domainAndQuantifyVarBddArray,
4222	array_t **orderedRelationArrayPtr,
4223	array_t **arraySmoothVarBddArrayPtr,
4224	array_t *arrayDomainQuantifyVarsWithZeroNumCtr)
4225	{
4226	int numRelation, ctrCount, currentRankMaxSmoothVarIndex;
4227	int maxIndex = 0;
4228	array_t orderedRelationArray, arraySmoothVarBddArray;
4229	array_t *smoothVarBddArray;
4230	int *bestCtrIdVector;
4231	int maxNumLocalSmoothVars, maxNumSmoothVars, maxNumIntroducedVars;
4232	lsGen lsgen;
4233
4234	ctrCount = 0;
4235	currentRankMaxSmoothVarIndex = 0;
4236
4237	numRelation = array_n(relationArray);
4238
4239	arraySmoothVarBddArray = NIL(array_t);
4240	orderedRelationArray = array_alloc(bdd_t*, 0);
4241	*orderedRelationArrayPtr = orderedRelationArray;
4242	if (arraySmoothVarBddArrayPtr != NIL(array_t *)) {
4243	arraySmoothVarBddArray = array_alloc(array_t*, 0);
4244	*arraySmoothVarBddArrayPtr = arraySmoothVarBddArray;
4245	array_insert_last(array_t*, arraySmoothVarBddArray,
4246	arrayDomainQuantifyVarsWithZeroNumCtr);
4247	}
4248	bestCtrIdVector = ALLOC(int, numRelation);
4249
4250	while (ctrCount < numRelation) {
4251	float bestBenefit, benefit;
4252	int bestCtrId;
4253	bdd_t *bestRelation;
4254	lsGen ctrInfoListGen;
4255	CtrInfo_t ctrInfo, ctrInfoAux;
4256
4257	bestBenefit = -1.0e20; /* a safely small number */
4258	bestCtrId = -1;
4259	/* Find the maximum index of the remaining clusters */
4260	while (currentRankMaxSmoothVarIndex < numRelation &&
4261	(maxIndex = sortedMaxIndexVector[currentRankMaxSmoothVarIndex++]) == -1);
4262
4263	/* Calculate the maximum values of local smooth variables etc. */
4264	maxNumLocalSmoothVars = 0;
4265	maxNumSmoothVars = 0;
4266	maxNumIntroducedVars = 0;
4267	lsForEachItem(remainingCtrInfoList, lsgen, ctrInfo) {
4268	if (ctrInfo->numLocalSmoothVars > maxNumLocalSmoothVars) {
4269	maxNumLocalSmoothVars = ctrInfo->numLocalSmoothVars;
4270	}
4271	if (ctrInfo->numSmoothVars > maxNumSmoothVars) {
4272	maxNumSmoothVars = ctrInfo->numSmoothVars;
4273	}
4274	if (ctrInfo->numIntroducedVars > maxNumIntroducedVars) {
4275	maxNumIntroducedVars = ctrInfo->numIntroducedVars;
4276	}
4277	}
4278
4279	if (option->verbosity >= 4) {
4280	fprintf(vis_stdout, "maxNumLocalSmoothVars = %3d maxNumSmoothVars = %3d ",
4281	maxNumLocalSmoothVars, maxNumSmoothVars);
4282	fprintf(vis_stdout, "maxNumIntroducedVars = %3d\n", maxNumIntroducedVars);
4283	}
4284	/* Calculate the cost function of each of the cluster */
4285	ctrInfoListGen = lsStart(remainingCtrInfoList);
4286	while (lsNext(ctrInfoListGen, &ctrInfo, NIL(lsHandle)) ==
4287	LS_OK) {
4288	benefit = CalculateBenefit(ctrInfo, maxNumLocalSmoothVars,
4289	maxNumSmoothVars, maxIndex,
4290	maxNumIntroducedVars, option);
4291
4292	if (option->verbosity >= 4) {
4293	fprintf(vis_stdout,
4294	"id = %d: numLocalSmoothVars = %d numSmoothVars = %d benefit = %f\n",
4295	ctrInfo->ctrId, ctrInfo->numLocalSmoothVars,
4296	ctrInfo->numSmoothVars, benefit);
4297	}
4298	if (benefit > bestBenefit) {
4299	bestBenefit = benefit;
4300	bestCtrId = ctrInfo->ctrId;
4301	}
4302	}
4303	lsFinish(ctrInfoListGen);
4304	/*
4305	* Insert the relation in the ordered array of relations and put in the
4306	* appropriate cubes.
4307	*/
4308
4309	bestCtrIdVector[ctrCount] = bestCtrId;
4310	ctrInfo = array_fetch(CtrInfo_t*, ctrInfoArray, bestCtrId);
4311	lsRemoveItem(ctrInfo->ctrInfoListHandle, &ctrInfoAux);
4312	assert(ctrInfo == ctrInfoAux);
4313	bestRelation = array_fetch(bdd_t*, relationArray, bestCtrId);
4314	array_insert_last(bdd_t*, orderedRelationArray, bestRelation);
4315	if (option->verbosity >= 4) {
4316	fprintf(vis_stdout,
4317	"Best id = %d benefit = %f numLocalSmoothVars = %d numSmoothVars = %d\n",
4318	bestCtrId, bestBenefit, ctrInfo->numLocalSmoothVars,
4319	ctrInfo->numSmoothVars);
4320	}
4321	/*
4322	* Update the remaining ctrInfo's and the varInfo's affected by choosing
4323	* this cluster. Also get the array of smooth variables which can be
4324	* quantified once this cluster is multiplied in the product.
4325	*/
4326	smoothVarBddArray = UpdateInfoArrays(ctrInfo, bddIdToBddTable,
4327	&numSmoothVarsRemaining,
4328	&numIntroducedVarsRemaining);
4329	assert(CheckCtrInfo(ctrInfo, numSmoothVarsRemaining, 0,
4330	numIntroducedVarsRemaining));
4331
4332	if (arraySmoothVarBddArrayPtr != NIL(array_t *)) {
4333	if (ctrCount == numRelation-1) {
4334	/*
4335	* In the last element of arraySmoothVarBddArray, put all the domain
4336	* and quantify variables (in case some of them were not in the support
4337	* of any cluster).
4338	*/
4339	int i, j;
4340	st_table *varsTable = st_init_table((ST_PFICPCP)bdd_ptrcmp,
4341	(ST_PFICPI)bdd_ptrhash);
4342	array_t *tmpVarBddArray;
4343	mdd_t *tmpVar;
4344
4345	arrayForEachItem(array_t *, arraySmoothVarBddArray, i, tmpVarBddArray) {
4346	arrayForEachItem(mdd_t *, tmpVarBddArray, j, tmpVar) {
4347	st_insert(varsTable, (char *)tmpVar, NIL(char));
4348	}
4349	}
4350	arrayForEachItem(mdd_t *, smoothVarBddArray, i, tmpVar) {
4351	st_insert(varsTable, (char *)tmpVar, NIL(char));
4352	}
4353	arrayForEachItem(mdd_t *, domainAndQuantifyVarBddArray, i, tmpVar) {
4354	if (st_lookup(varsTable, (char )tmpVar, NIL(char )) == 0)
4355	array_insert_last(mdd_t *, smoothVarBddArray, mdd_dup(tmpVar));
4356	}
4357	st_free_table(varsTable);
4358	}
4359	array_insert_last(array_t*, arraySmoothVarBddArray, smoothVarBddArray);
4360	}
4361	else{
4362	mdd_array_free(smoothVarBddArray);
4363	}
4364	sortedMaxIndexVector[ctrInfo->rankMaxSmoothVarIndex] = -1;
4365	ctrCount++;
4366	}
4367	assert(numIntroducedVarsRemaining == 0);
4368	assert(numSmoothVarsRemaining == 0);
4369	if (option->verbosity >= 3) {
4370	int i;
4371	(void) fprintf(vis_stdout,"Cluster Sequence = ");
4372	for (i=0; i<numRelation; i++) {
4373	(void) fprintf(vis_stdout, "%d ", bestCtrIdVector[i]);
4374	}
4375	(void) fprintf(vis_stdout,"\n");
4376	}
4377
4378	FREE(bestCtrIdVector);
4379	}
4380
4381
4382	/Function******************************************************************
4383
4384	Synopsis [This function computes the set of variables which can be
4385	smoothed out once a particular cluster is chosen to be multiplied in the
4386	product.]
4387
4388	Description [The support variable list (varItemList) of the cluster (ctrInfo)
4389	is traversed and depending upon the type of the variable and the number of
4390	unordered clustered relations which depend on that variable following actions
4391	are taken:
4392
4393	a. If the variable is of range type:
4394	This implies that this variable is appearing for the first time in the
4395	product. Since it is already introduced in the product, the cost function
4396	of any other unordered relation which depends on this variable will get
4397	modified. The numIntroducedVariables field of each of the cluster which
4398	depends on this variable is decreased by 1. Also this varItemStruct
4399	corresponding to this variable is removed from the varItemList field of
4400	the cluster.
4401
4402	b. If the variable is of domain or quantify type:
4403	b1. If number of clusters which depend on this variable is 1 (numCtr == 1):
4404	In this case, this variable can be quantified out once the chosen
4405	cluster is multiplied in the product. Hence the variable is put in
4406	the smoothVarBddArray.
4407	b2. If (numCtr == 2)
4408	In this case, there is one more unordered cluster which depends on
4409	this variable. But once the current cluster is multiplied in the
4410	product, the "numLocalSmoothVars" field of ctrInfo corresponding to
4411	the other dependent cluster needs to be increased by 1.
4412	b3. If (numCtr > 2)
4413	In this case, we just need to decrease the numCtr of the variable by
4414	1.
4415
4416	In any case, for each varInfo in the support variable list (varItemList) of
4417	the cluster (ctrInfo) the following invariant is maintained:
4418	varInfo->numCtr == lsLength(varInfo->ctrItemList)
4419	]
4420
4421	SideEffects [The fields of ctrInfo and varInfo are changed as mentioned
4422	above.]
4423
4424	******************************************************************************/
4425	static array_t *
4426	UpdateInfoArrays(CtrInfo_t ctrInfo, st_table bddIdToBddTable,
4427	int *numSmoothVarsRemainingPtr,
4428	int *numIntroducedVarsRemainingPtr)
4429	{
4430	array_t *smoothVarBddArray;
4431	lsGen varItemListGen;
4432	int numSmoothVarsRemaining = *numSmoothVarsRemainingPtr;
4433	int numIntroducedVarsRemaining = *numIntroducedVarsRemainingPtr;
4434	VarItem_t *varItem;
4435	lsHandle varItemHandle;
4436
4437	smoothVarBddArray = array_alloc(bdd_t*, 0);
4438	varItemListGen = lsStart(ctrInfo->varItemList);
4439	while (lsNext(varItemListGen, &varItem, &varItemHandle) ==
4440	LS_OK) {
4441	VarInfo_t *varInfo = varItem->varInfo;
4442	CtrItem_t *ctrItem;
4443	assert(varInfo->numCtr == lsLength(varInfo->ctrItemList));
4444	lsRemoveItem(varItem->ctrItemHandle, &ctrItem);
4445	CtrItemStructFree(ctrItem);
4446	varInfo->numCtr--;
4447	lsRemoveItem(varItemHandle, &varItem);
4448	VarItemStructFree(varItem);
4449
4450	/*
4451	* If this variable is to be smoothed (domain or quantify type) and
4452	* the numCtr is 1, then it should be added to the smoothVarBddArray,
4453	* otherwise, the numCtr should be decreased by 1.
4454	* If the variable is of the range type then the number of introduced
4455	* vars remaining and the number of introduced vars should be
4456	* appropriately modified.
4457	*/
4458	if ((varInfo->varType == domainVar_c) \|\|
4459	(varInfo->varType == quantifyVar_c)) {
4460	if (varInfo->numCtr == 0) {
4461	bdd_t *varBdd;
4462	st_lookup(bddIdToBddTable, (char *)(long)(varInfo->bddId), &varBdd);
4463	array_insert_last(bdd_t*, smoothVarBddArray, bdd_dup(varBdd));
4464	numSmoothVarsRemaining--;
4465	ctrInfo->numLocalSmoothVars--;
4466	ctrInfo->numSmoothVars--;
4467	}
4468	else{
4469	if (varInfo->numCtr == 1) {
4470	/*
4471	* We need to update the numLocalSmoothVars of the ctr
4472	* which depends on it.
4473	*/
4474	lsFirstItem(varInfo->ctrItemList, &ctrItem, LS_NH);
4475	ctrItem->ctrInfo->numLocalSmoothVars++;
4476	}
4477	/*
4478	* else varInfo->numCtr > 1 : Nothing to be done because neither it
4479	* can be quantified out, nor it is effecting any cost function.
4480	*/
4481	ctrInfo->numSmoothVars--;
4482	}
4483	}
4484	else{/* The variable is of range type, so need to appropriately modify the
4485	* numIntroducedVars of those clusters which contain this range
4486	* variable in their support.
4487	*/
4488	lsHandle ctrItemHandle;
4489	lsGen ctrItemListGen = lsStart(varInfo->ctrItemList);
4490	ctrInfo->numIntroducedVars--;
4491	while (lsNext(ctrItemListGen, &ctrItem, &ctrItemHandle) == LS_OK) {
4492	ctrItem->ctrInfo->numIntroducedVars--;
4493	lsRemoveItem(ctrItem->varItemHandle,&varItem);
4494	lsRemoveItem(ctrItemHandle,&ctrItem);
4495	VarItemStructFree(varItem);
4496	CtrItemStructFree(ctrItem);
4497	}
4498	lsFinish(ctrItemListGen);
4499	numIntroducedVarsRemaining--;
4500	varInfo->numCtr = 0;
4501	}
4502	assert(varInfo->numCtr == lsLength(varInfo->ctrItemList));
4503	}
4504	lsFinish(varItemListGen);
4505	*numIntroducedVarsRemainingPtr = numIntroducedVarsRemaining;
4506	*numSmoothVarsRemainingPtr = numSmoothVarsRemaining;
4507	return smoothVarBddArray;
4508	}
4509
4510
4511	/Function******************************************************************
4512
4513	Synopsis [Gets the necessary options for computing the image and returns
4514	in the option structure.]
4515
4516	Description [
4517	The strategy
4518	Choose the cost function:
4519	The objective function attached with each Ti is
4520	Ci = W1 C1i + W2 C2i + W3 C3i - W4C4i
4521	where:
4522	W1 = weight attached with variable getting smoothed
4523	W2 = weight attached with the support count of the Ti
4524	W3 = weight attached with the max id of the Ti
4525	W4 = weight attached with variable getting introduced
4526	C1i = Ui/Vi
4527	C2i = Vi/Wi
4528	C3i = Mi/Max
4529	C4i = Xi/Yi
4530	Ui = number of variables getting smoothed
4531	Vi = number of ps support variables of Ti
4532	Wi = total number of ps variables remaining which have not been
4533	smoothed out
4534	Mi = value of Max id of Ti
4535	Max = value of Max id across all the Ti's remaining to be multiplied
4536	Xi = number of ns variables introduced
4537	Yi = total number of ns variables which have not been introduced so
4538	far.
4539	Get the weights from the global option]
4540
4541	SideEffects []
4542
4543	******************************************************************************/
4544	static float
4545	CalculateBenefit(CtrInfo_t *ctrInfo, int maxNumLocalSmoothVars, int
4546	maxNumSmoothVars, int maxIndex, int
4547	maxNumIntroducedVars, ImgTrmOption_t *option)
4548	{
4549	int W1, W2, W3, W4;
4550	float benefit;
4551
4552	W1 = option->W1;
4553	W2 = option->W2;
4554	W3 = option->W3;
4555	W4 = option->W4;
4556
4557	benefit = 0.0;
4558	benefit += (maxNumLocalSmoothVars ?
4559	((float)W1 * ((float)ctrInfo->numLocalSmoothVars /
4560	(float)maxNumLocalSmoothVars)) : 0.0);
4561
4562	benefit += (maxNumSmoothVars ?
4563	((float)W2 * ((float)ctrInfo->numSmoothVars /
4564	(float)maxNumSmoothVars)) : 0.0);
4565
4566	benefit += (maxIndex ?
4567	((float)W3 * ((float)ctrInfo->maxSmoothVarIndex /
4568	(float)maxIndex)) : 0.0);
4569
4570	benefit -= (maxNumIntroducedVars ?
4571	((float)W4 * ((float)ctrInfo->numIntroducedVars /
4572	(float)maxNumIntroducedVars)) : 0.0);
4573
4574	return benefit;
4575	}
4576
4577	/Function******************************************************************
4578
4579	Synopsis [Prints the option values used in IWLS95 techinique for
4580	image computation.]
4581
4582	Description [Prints the option values used in IWLS95 techinique for
4583	image computation.]
4584
4585	SideEffects []
4586
4587	******************************************************************************/
4588	static void
4589	PrintOption(Img_MethodType method, ImgTrmOption_t option, FILE fp)
4590	{
4591	if (method == Img_Iwls95_c)
4592	(void)fprintf(fp, "Printing Information about Image method: IWLS95\n");
4593	else if (method == Img_Mlp_c)
4594	(void)fprintf(fp, "Printing Information about Image method: MLP\n");
4595	else if (method == Img_Linear_c)
4596	(void)fprintf(fp, "Printing Information about Image method: LINEAR\n");
4597	else
4598	assert(0);
4599	(void)fprintf(fp,
4600	"\tThreshold Value of Bdd Size For Creating Clusters = %d\n",
4601	option->clusterSize);
4602	(void)fprintf(fp,
4603	"\t\t(Use \"set image_cluster_size value\" to set this to desired value)\n");
4604	(void)fprintf(fp, "\tVerbosity = %d\n", option->verbosity);
4605	(void)fprintf(fp,
4606	"\t\t(Use \"set image_verbosity value\" to set this to desired value)\n");
4607	if (method == Img_Iwls95_c) {
4608	(void)fprintf(fp, "\tW1 =%3d W2 =%2d W3 =%2d W4 =%2d\n",
4609	option->W1, option->W2, option->W3, option->W4);
4610	(void)fprintf(fp,
4611	"\t\t(Use \"set image_W? value\" to set these to desired values)\n");
4612	}
4613	}
4614
4615	/Function******************************************************************
4616
4617	Synopsis [Allocates and initializes the info structure for IWLS95
4618	technique.]
4619
4620	Description [Allocates and initializes the info structure for IWLS95
4621	technique.]
4622
4623	SideEffects []
4624
4625	******************************************************************************/
4626	static Iwls95Info_t *
4627	Iwls95InfoStructAlloc(Img_MethodType method)
4628	{
4629	Iwls95Info_t *info;
4630	info = ALLOC(Iwls95Info_t, 1);
4631	memset(info, 0, sizeof(Iwls95Info_t));
4632	info->method = method;
4633	info->option = TrmGetOptions();
4634	info->PIoption = ImgGetPartialImageOptions();
4635	return info;
4636	}
4637
4638	/Function******************************************************************
4639
4640	Synopsis [Allocates and initializes memory for ctrInfoStruct.]
4641
4642	Description [Allocates and initializes memory for ctrInfoStruct.]
4643
4644	SideEffects []
4645
4646	******************************************************************************/
4647	static CtrInfo_t *
4648	CtrInfoStructAlloc(void)
4649	{
4650	CtrInfo_t *ctrInfo;
4651	ctrInfo = ALLOC(CtrInfo_t, 1);
4652	ctrInfo->ctrId = -1;
4653	ctrInfo->numLocalSmoothVars = 0;
4654	ctrInfo->numSmoothVars = 0;
4655	ctrInfo->maxSmoothVarIndex = -1;
4656	ctrInfo->numIntroducedVars = 0;
4657	ctrInfo->varItemList = lsCreate();
4658	ctrInfo->ctrInfoListHandle = NULL;
4659	return ctrInfo;
4660	}
4661
4662
4663	/Function******************************************************************
4664
4665	Synopsis [Frees the memory associated with ctrInfoStruct.]
4666
4667	Description [Frees the memory associated with ctrInfoStruct.]
4668
4669	SideEffects []
4670
4671	******************************************************************************/
4672	static void
4673	CtrInfoStructFree(CtrInfo_t *ctrInfo)
4674	{
4675	lsDestroy(ctrInfo->varItemList, 0);
4676	FREE(ctrInfo);
4677	}
4678
4679	/Function******************************************************************
4680
4681	Synopsis [Allocates and initializes memory for varInfoStruct.]
4682
4683	Description [Allocates and initializes memory for varInfoStruct.]
4684
4685	SideEffects []
4686
4687	******************************************************************************/
4688	static VarInfo_t *
4689	VarInfoStructAlloc(void)
4690	{
4691	VarInfo_t *varInfo;
4692	varInfo = ALLOC(VarInfo_t, 1);
4693	varInfo->bddId = -1;
4694	varInfo->numCtr = 0;
4695	varInfo->varType = -1;
4696	varInfo->ctrItemList = lsCreate();
4697	return varInfo;
4698	}
4699
4700	/Function******************************************************************
4701
4702	Synopsis [Frees the memory associated with varInfoStruct.]
4703
4704	Description [Frees the memory associated with varInfoStruct.]
4705
4706	SideEffects []
4707
4708	******************************************************************************/
4709	static void
4710	VarInfoStructFree(VarInfo_t *varInfo)
4711	{
4712	lsDestroy(varInfo->ctrItemList,0);
4713	FREE(varInfo);
4714	}
4715
4716	/Function******************************************************************
4717
4718	Synopsis [Frees the memory associated with CtrItemStruct]
4719
4720	Description [Frees the memory associated with CtrItemStruct]
4721
4722	SideEffects []
4723
4724	******************************************************************************/
4725	static void
4726	CtrItemStructFree(CtrItem_t *ctrItem)
4727	{
4728	FREE(ctrItem);
4729	}
4730
4731	/Function******************************************************************
4732
4733	Synopsis [Frees the memory associated with VarItemStruct]
4734
4735	Description [Frees the memory associated with VarItemStruct]
4736
4737	SideEffects []
4738
4739	******************************************************************************/
4740	static void
4741	VarItemStructFree(VarItem_t *varItem)
4742	{
4743	FREE(varItem);
4744	}
4745
4746	/Function******************************************************************
4747
4748	Synopsis [Compare function used to sort the ctrInfoStruct based on the
4749	maxSmoothVarIndex field.]
4750
4751	Description [This function is used to sort the array of clusters based on the
4752	maximum index of the support variable.]
4753
4754	SideEffects []
4755
4756	******************************************************************************/
4757	static int
4758	CtrInfoMaxIndexCompare(const void * p1, const void * p2)
4759	{
4760	CtrInfo_t infoCtr1 = (CtrInfo_t ) p1;
4761	CtrInfo_t infoCtr2 = (CtrInfo_t ) p2;
4762	return ((infoCtr1)->maxSmoothVarIndex > (infoCtr2)->maxSmoothVarIndex);
4763	}
4764
4765	/* **************************************************************************
4766	* Debugging Related Routines.
4767	***************************************************************************/
4768
4769
4770	/Function******************************************************************
4771
4772	Synopsis [Prints the CtrInfo_t data structure.]
4773
4774	Description [Prints the CtrInfo_t data structure.]
4775
4776	SideEffects []
4777
4778	******************************************************************************/
4779	static void
4780	PrintCtrInfoStruct(CtrInfo_t *ctrInfo)
4781	{
4782	lsGen lsgen;
4783	VarItem_t *varItem;
4784
4785	(void) fprintf(vis_stdout,"Ctr ID = %d\tNumLocal = %d\tNumSmooth=%d\tNumIntro=%d\tmaxSmooth=%d\trank=%d\n",
4786	ctrInfo->ctrId, ctrInfo->numLocalSmoothVars,
4787	ctrInfo->numSmoothVars, ctrInfo->numIntroducedVars,
4788	ctrInfo->maxSmoothVarIndex, ctrInfo->rankMaxSmoothVarIndex);
4789	lsgen = lsStart(ctrInfo->varItemList);
4790	while (lsNext(lsgen, &varItem, NIL(lsHandle)) == LS_OK) {
4791	(void) fprintf(vis_stdout,"%d\t", varItem->varInfo->bddId);
4792	}
4793	lsFinish(lsgen);
4794	fprintf(vis_stdout,"\n");
4795	}
4796	/Function******************************************************************
4797
4798	Synopsis [Prints the VarInfo_t structure.]
4799
4800	Description [Prints the VarInfo_t structure.]
4801
4802	SideEffects []
4803
4804	******************************************************************************/
4805	static void
4806	PrintVarInfoStruct(VarInfo_t *varInfo)
4807	{
4808	lsGen lsgen;
4809	CtrItem_t *ctrItem;
4810
4811	(void) fprintf(vis_stdout,"Var ID = %d\tNumCtr = %d\tVarType=%d\n",
4812	varInfo->bddId, varInfo->numCtr, varInfo->varType);
4813	lsgen = lsStart(varInfo->ctrItemList);
4814	while (lsNext(lsgen, &ctrItem, NIL(lsHandle)) == LS_OK) {
4815	(void) fprintf(vis_stdout,"%d\t", ctrItem->ctrInfo->ctrId);
4816	}
4817	lsFinish(lsgen);
4818	fprintf(vis_stdout,"\n");
4819	}
4820
4821	/Function******************************************************************
4822
4823	Synopsis [Given an array of BDD's representing the relations and another
4824	array of BDD cubes (in the form of array of bdd_t of variable) representing
4825	the quantification schedule, this function checks if the schedule is correct.
4826	]
4827
4828	Description [Assume Ci represents the ith cube in the array and the Ti
4829	represents the ith relation. The correctness of the schedule is defined as
4830	follows:
4831	a. For all Tj: j > i, SUP(Tj) and SUP(Ci) do not intersect, i.e., the
4832	variables which are quantified in Ci should not appear in the Tj for j>i.
4833	b. For any i, j, SUP(Ci) and SUP(Cj) do not intersect. However this is
4834	not true for the last cube (Cn-1). This is because the last cube contains
4835	all the smooth variables.
4836	]
4837	SideEffects []
4838
4839	******************************************************************************/
4840	static int
4841	CheckQuantificationSchedule(array_t *relationArray,
4842	array_t *arraySmoothVarBddArray)
4843	{
4844	int i, j;
4845	long varId;
4846	st_table smoothVarTable, supportTable;
4847	bdd_t *relation;
4848	array_t smoothVarBddArray, smoothVarBddIdArray;
4849	st_generator *stgen;
4850
4851	assert(array_n(relationArray) + 1 == array_n(arraySmoothVarBddArray));
4852
4853	smoothVarTable = st_init_table(st_numcmp, st_numhash);
4854
4855	smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, 0);
4856	smoothVarBddIdArray = bdd_get_varids(smoothVarBddArray);
4857	for (j=0; j<array_n(smoothVarBddIdArray); j++) {
4858	varId = (long) array_fetch(int, smoothVarBddIdArray, j);
4859	assert(st_insert(smoothVarTable, (char *) varId, NIL(char))==0);
4860	}
4861	array_free(smoothVarBddIdArray);
4862
4863	for (i=0; i<array_n(relationArray); i++) {
4864	relation = array_fetch(bdd_t*, relationArray, i);
4865	supportTable = ImgBddGetSupportIdTable(relation);
4866	/*
4867	* Check that none of the variables in the support have already been
4868	* quantified.
4869	*/
4870	st_foreach_item(supportTable, stgen, &varId, NULL) {
4871	assert(st_is_member(smoothVarTable, (char *) varId) == 0);
4872
4873	}
4874	st_free_table(supportTable);
4875	if (i == (array_n(relationArray)-1)) {
4876	/* Since last element of arraySmoothVarBddArray has all the
4877	* smooth variables, it will not satisfy the condition.
4878	*/
4879	continue;
4880	}
4881
4882	/*
4883	* Put each of the variables quantified at this step in the
4884	* smoothVarTable. And check that none of these smooth variables
4885	* have been introduced before.
4886	*/
4887	smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i + 1);
4888	smoothVarBddIdArray = bdd_get_varids(smoothVarBddArray);
4889	for (j=0; j<array_n(smoothVarBddIdArray); j++) {
4890	varId = (long) array_fetch(int, smoothVarBddIdArray, j);
4891	assert(st_insert(smoothVarTable, (char *) varId, NIL(char))==0);
4892	}
4893	array_free(smoothVarBddIdArray);
4894	}
4895	st_free_table(smoothVarTable);
4896	return 1;
4897	}
4898
4899	/Function******************************************************************
4900
4901	Synopsis [Checks the validity of an array of CtrInfoStructs.]
4902
4903	Description [Checks the validity of an array of CtrInfoStructs.]
4904
4905	SideEffects []
4906
4907	******************************************************************************/
4908	static int
4909	CheckCtrInfoArray(array_t *ctrInfoArray, int numDomainVars, int
4910	numQuantifyVars, int numRangeVars)
4911	{
4912	int i;
4913	for (i=0; i<array_n(ctrInfoArray); i++) {
4914	CheckCtrInfo(array_fetch(CtrInfo_t *, ctrInfoArray, i),
4915	numDomainVars, numQuantifyVars, numRangeVars);
4916	}
4917	return 1;
4918	}
4919
4920	/Function******************************************************************
4921
4922	Synopsis [Checks the validity of a CtrInfoStruct.]
4923
4924	Description [Checks the validity of a CtrInfoStruct.]
4925
4926	SideEffects []
4927
4928	******************************************************************************/
4929	static int
4930	CheckCtrInfo(CtrInfo_t *ctrInfo, int numDomainVars,
4931	int numQuantifyVars, int numRangeVars)
4932	{
4933	assert(ctrInfo->numLocalSmoothVars <= (numDomainVars +
4934	numQuantifyVars));
4935	assert(ctrInfo->numSmoothVars <= (numDomainVars +
4936	numQuantifyVars));
4937	assert(ctrInfo->numIntroducedVars <= numRangeVars);
4938	assert(lsLength(ctrInfo->varItemList) ==
4939	(ctrInfo->numSmoothVars+ctrInfo->numIntroducedVars));
4940	return 1;
4941	}
4942
4943	/Function******************************************************************
4944
4945	Synopsis [Checks the validity of an array of VarInfoStruct.]
4946
4947	Description [Checks the validity of an array of VarInfoStruct.]
4948
4949	SideEffects []
4950
4951	******************************************************************************/
4952	static int
4953	CheckVarInfoArray(array_t *varInfoArray, int numRelation)
4954	{
4955	int i;
4956	for (i=0; i<array_n(varInfoArray); i++) {
4957	VarInfo_t *varInfo;
4958	varInfo = array_fetch(VarInfo_t *, varInfoArray, i);
4959	assert(varInfo->numCtr <= numRelation);
4960	assert(varInfo->varType >= 0);
4961	assert(varInfo->varType <= 2);
4962	assert(lsLength(varInfo->ctrItemList) == varInfo->numCtr);
4963	}
4964	return 1;
4965	}
4966
4967	/* ****************************************************************
4968	* Utility Routines.
4969	****************************************************************/
4970
4971	/Function******************************************************************
4972
4973	Synopsis [Duplicates an array of BDDs.]
4974
4975	Description [Duplicates an array of BDDs.]
4976
4977	SideEffects []
4978
4979	******************************************************************************/
4980	static array_t *
4981	BddArrayDup(array_t *bddArray)
4982	{
4983	int i;
4984	array_t *resultArray;
4985	bdd_t *bdd;
4986	resultArray = array_alloc(bdd_t*, 0);
4987	arrayForEachItem(bdd_t *, bddArray, i, bdd) {
4988	array_insert_last(bdd_t*, resultArray, bdd_dup(bdd));
4989	}
4990	return resultArray;
4991	}
4992
4993	static array_t *
4994	BddArrayArrayDup(array_t *bddArray)
4995	{
4996	int i;
4997	array_t *resultArray;
4998	array_t arr, tarr;
4999
5000	resultArray = array_alloc(bdd_t*, 0);
5001	arrayForEachItem(array_t *, bddArray, i, arr) {
5002	tarr = BddArrayDup(arr);
5003	array_insert_last(array_t*, resultArray, tarr);
5004	}
5005	return resultArray;
5006	}
5007
5008
5009	/Function******************************************************************
5010
5011	Synopsis [Returns a BDD after taking the product of fromSet with the
5012	BDDs in the relationArray and quantifying out the variables using
5013	the schedule given in the arraySmoothVarBddArray.]
5014
5015	Description [The product is taken from the left, i.e., fromSet is
5016	multiplied with relationArray[0]. The array of variables given by
5017	arraySmoothVarBddArray[i] are quantified when the relationArray[i]
5018	is multiplied in the product. We notice that no simplification is
5019	used in the computation. It was found to be the fastest way to
5020	compute the image. When partial image is allowed, a partial image is
5021	computed based on the method specified. If the method is "approx",
5022	approximation is applied to some intermediate product. If the method
5023	is "clipping", clipping is introduced during and-abstract. A flag
5024	partial is set to indicate to the calling procedure that a partial
5025	image was computed as against an exact image. Partial flag comes in
5026	indicating whether partial images are allowed, and leave indicating
5027	whether the image was partial or not. ]
5028
5029	SideEffects [partial is set when some approximation is applied]
5030
5031	******************************************************************************/
5032	static mdd_t *
5033	BddLinearAndSmooth(mdd_manager *mddManager,
5034	bdd_t *fromSet,
5035	array_t *relationArray,
5036	array_t *arraySmoothVarBddArray,
5037	array_t *smoothVarCubeArray,
5038	int verbosity,
5039	ImgPartialImageOption_t *PIoption,
5040	boolean *partial, boolean lazySiftFlag)
5041	{
5042	int i;
5043	int intermediateSize = 0;
5044	int maxSize = 0;
5045	mdd_t *newProduct;
5046	boolean partialImageAllowed;
5047	bdd_t *product = fromSet;
5048	int clippingDepth = -1;
5049	int partialImageThreshold = 0;
5050	int partialImageMethod = Img_PIApprox_c;
5051	array_t *smoothVarBddArray = NIL(array_t);
5052	mdd_t *smoothVarCube = NIL(mdd_t);
5053	int nvars = -2;
5054
5055	assert(CheckQuantificationSchedule(relationArray, arraySmoothVarBddArray));
5056
5057	/* Copy (partial) which indicates whether partial image is allowed. /
5058	/* (partial) is set to TRUE later if partial image was performed. /
5059	partialImageAllowed = *partial;
5060	*partial = FALSE;
5061
5062	/* partial image options */
5063	if (PIoption != NULL) {
5064	nvars = PIoption->nvars;
5065	clippingDepth = (int) (PIoption->clippingDepthFrac*nvars);
5066	partialImageThreshold = PIoption->partialImageThreshold;
5067	partialImageMethod = PIoption->partialImageMethod;
5068	}
5069
5070	if (fromSet) {
5071	if (smoothVarCubeArray) {
5072	smoothVarCube = array_fetch(mdd_t*, smoothVarCubeArray, 0);
5073	if (bdd_is_tautology(smoothVarCube, 1))
5074	product = bdd_dup(fromSet);
5075	else
5076	product = bdd_smooth_with_cube(fromSet, smoothVarCube);
5077	} else {
5078	smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, 0);
5079	if (array_n(smoothVarBddArray) == 0)
5080	product = bdd_dup(fromSet);
5081	else
5082	product = bdd_smooth(fromSet, smoothVarBddArray);
5083	}
5084	} else
5085	product = bdd_one(mddManager);
5086
5087	for (i=0; i<array_n(relationArray); i++) {
5088	bdd_t relation, tmpProduct;
5089	boolean allowClipping = FALSE;
5090
5091	/* fetch relation to intersect with the next product. */
5092	relation = array_fetch(bdd_t*, relationArray, i);
5093	if (smoothVarCubeArray)
5094	smoothVarCube = array_fetch(mdd_t*, smoothVarCubeArray, i + 1);
5095	else
5096	smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i + 1);
5097
5098	/* Clipping allowed only if clipping option is specified, partial
5099	* image is allowed, clipping depth is meaningful and sizes are not
5100	* under control.
5101	*/
5102	if ((PIoption != NULL) &&
5103	(partialImageAllowed) &&
5104	(partialImageMethod == Img_PIClipping_c) &&
5105	(nvars >= clippingDepth)) {
5106	/* if conjuncts too small, dont clip. */
5107	if ((bdd_size(product) > partialImageThreshold) \|\|
5108	(bdd_size(relation) > partialImageThreshold)) {
5109	allowClipping = TRUE;
5110	}
5111	}
5112
5113	if (lazySiftFlag) {
5114	int j;
5115	int nVars = bdd_num_vars(mddManager);
5116	var_set_t *sup_ids = bdd_get_support(relation);
5117
5118	for (j = 0; j < nVars; j++) {
5119	if (var_set_get_elt(sup_ids, j) == 1) {
5120	if (bdd_is_ns_var(mddManager, j))
5121	bdd_reset_var_to_be_grouped(mddManager, j);
5122	else if (!bdd_is_ps_var(mddManager, j))
5123	bdd_reset_var_to_be_grouped(mddManager, j);
5124	}
5125	}
5126	var_set_free(sup_ids);
5127	}
5128
5129	/* if clipping not allowed, do regular and-abstract */
5130	if (!allowClipping) {
5131	if (smoothVarCubeArray) {
5132	if (bdd_is_tautology(smoothVarCube, 1))
5133	tmpProduct = bdd_and(product, relation, 1, 1);
5134	else {
5135	tmpProduct = bdd_and_smooth_with_cube(product, relation,
5136	smoothVarCube);
5137	}
5138	} else {
5139	if (array_n(smoothVarBddArray) == 0)
5140	tmpProduct = bdd_and(product, relation, 1, 1);
5141	else
5142	tmpProduct = bdd_and_smooth(product, relation, smoothVarBddArray);
5143	}
5144	} else {
5145	/* the conditions to clip are that partial image is allowed,
5146	* partial image method is set to clipping, clipping depth
5147	* is meaningful and either the product or the relation is
5148	* larger than the partial image threshold.
5149	*/
5150	if (smoothVarCubeArray)
5151	smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i+1);
5152	tmpProduct = ComputeClippedAndAbstract(product, relation,
5153	smoothVarBddArray, nvars,
5154	clippingDepth, partial, verbosity);
5155	}
5156
5157	if (lazySiftFlag) {
5158	int k, index;
5159	bdd_t *svar;
5160
5161	if (smoothVarCubeArray)
5162	smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i+1);
5163	for (k = 0; k < array_n(smoothVarBddArray); k++) {
5164	svar = array_fetch(bdd_t *, smoothVarBddArray, k);
5165	index = bdd_top_var_id(svar);
5166	bdd_set_var_to_be_grouped(mddManager, index);
5167	}
5168	}
5169
5170	bdd_free(product);
5171	product = tmpProduct;
5172
5173	/* subset if necessary */
5174	if ((i != array_n(relationArray)) &&
5175	(partialImageAllowed) &&
5176	(partialImageMethod == Img_PIApprox_c)) {
5177	intermediateSize = bdd_size(product);
5178	/* approximate if the intermediate product is too large. */
5179	if (intermediateSize > partialImageThreshold) {
5180	if (verbosity >= 2) {
5181	(void) fprintf(vis_stdout, "Intermediate Block %d Size = %10d\n", i,
5182	intermediateSize);
5183	}
5184	newProduct = ComputeSubsetOfIntermediateProduct(product, PIoption);
5185	if (verbosity >= 2) {
5186	if (!bdd_equal(newProduct, product)) {
5187	(void)fprintf(vis_stdout,
5188	"Intermediate Block Subset Size = %10d\n",
5189	bdd_size(newProduct));
5190	} else {
5191	(void)fprintf(vis_stdout, "Intermediate Block unchanged\n");
5192	}
5193	}
5194	/* record if partial image occurred */
5195	if (!bdd_equal(newProduct, product)) {
5196	*partial = TRUE;
5197	intermediateSize = bdd_size(product);
5198	}
5199	bdd_free(product);
5200	product = newProduct;
5201	}
5202	}
5203
5204	/* keep track of intermediate product size */
5205	if (verbosity >= 2) {
5206	if ((partialImageMethod != Img_PIApprox_c) \|\|
5207	(!partialImageAllowed) \|\|
5208	( i == array_n(relationArray))) {
5209	intermediateSize = bdd_size(product);
5210	}
5211	if (maxSize < intermediateSize) {
5212	maxSize = intermediateSize;
5213	}
5214	}
5215	}
5216	if (lazySiftFlag) {
5217	int nVars = bdd_num_vars(mddManager);
5218	for (i = 0; i < nVars; i++) {
5219	if (bdd_is_ps_var(mddManager, i))
5220	bdd_reset_var_to_be_grouped(mddManager, i);
5221	else
5222	bdd_set_var_to_be_grouped(mddManager, i);
5223	}
5224	}
5225	if (verbosity >= 2) {
5226	(void)fprintf(vis_stdout,
5227	"Max. BDD size for intermediate product = %10d\n", maxSize);
5228	}/* for all clusters */
5229
5230	return product;
5231	} /* end of BddLinearAndSmooth */
5232
5233	/Function******************************************************************
5234
5235	Synopsis [Hashes bdd id to bdd in the table.]
5236
5237	Description [The elements of the input array should be in one to one
5238	correpondence, i.e., idArray[i] should be the id of the variable
5239	bddArray[i]. Each element of idArray is hashed in the table with the value
5240	taken from the corresponding element from bddArray.]
5241
5242	SideEffects []
5243
5244	******************************************************************************/
5245
5246	static void
5247	HashIdToBddTable(st_table table, array_t idArray,
5248	array_t *bddArray)
5249	{
5250	int i;
5251	for (i=0; i<array_n(idArray); i++) {
5252	int id;
5253	bdd_t *bdd;
5254	id = array_fetch(int, idArray, i);
5255	bdd = array_fetch(bdd_t*, bddArray, i);
5256	st_insert(table, (char)(long)id, (char )bdd);
5257	}
5258	}
5259
5260
5261	/Function******************************************************************
5262
5263	Synopsis [Prints information about the schedule of clusters and
5264	the the corresponding smooth cubes.]
5265
5266	Description [This function is used to print information about the
5267	cluster sequence and the sequence of smooth cubes. For each cluster
5268	in sequence, it prints the number of variables quantified and the
5269	number of variables introduced.]
5270
5271	SideEffects []
5272
5273	******************************************************************************/
5274	static void
5275	PrintSmoothIntroducedCount(array_t *clusterArray, array_t
5276	**arraySmoothVarBddArrayPtr,
5277	array_t *psBddIdArray, array_t
5278	*nsBddIdArray)
5279	{
5280	int i,j;
5281	st_table nsBddIdTable, supportTable, *psBddIdTable;
5282	bdd_t *trans;
5283	int introducedCount;
5284	bdd_t *tmp;
5285	st_generator *stgen;
5286	long varId;
5287	array_t smoothVarBddArray, arraySmoothVarBddArray;
5288	array_t *smoothVarBddIdArray = NIL(array_t);
5289	int psCount, piNdCount;
5290
5291	if (arraySmoothVarBddArrayPtr == NIL(array_t*))
5292	arraySmoothVarBddArray = NIL(array_t);
5293	else
5294	arraySmoothVarBddArray = *arraySmoothVarBddArrayPtr;
5295
5296	(void) fprintf(vis_stdout, "**********************************************\n");
5297	nsBddIdTable = st_init_table(st_numcmp, st_numhash);
5298	for (i=0; i<array_n(nsBddIdArray); i++)
5299	st_insert(nsBddIdTable, (char *)(long) array_fetch(int, nsBddIdArray, i),
5300	(char *) NULL);
5301	psBddIdTable = st_init_table(st_numcmp, st_numhash);
5302	for (i=0; i<array_n(psBddIdArray); i++)
5303	st_insert(psBddIdTable, (char *)(long) array_fetch(int, psBddIdArray, i),
5304	(char *) NULL);
5305
5306	for (i=0; i<=array_n(clusterArray)-1; i++) {
5307	trans = array_fetch(bdd_t*, clusterArray, i);
5308	supportTable = ImgBddGetSupportIdTable(trans);
5309	psCount = 0;
5310	piNdCount = 0;
5311	if (arraySmoothVarBddArray != NIL(array_t)) {
5312	smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i);
5313	smoothVarBddIdArray = bdd_get_varids(smoothVarBddArray);
5314	for (j=0; j<array_n(smoothVarBddIdArray);j++) {
5315	if (st_is_member(psBddIdTable, (char *)(long)
5316	array_fetch(int, smoothVarBddIdArray, j)))
5317	psCount++;
5318	else
5319	piNdCount++;
5320	}
5321	}
5322	introducedCount = 0;
5323	st_foreach_item(nsBddIdTable, stgen, &varId, &tmp) {
5324	if (st_is_member(supportTable, (char *)varId)) {
5325	introducedCount++;
5326	st_delete(nsBddIdTable,&varId, NULL);
5327	}
5328	}
5329	(void)fprintf(vis_stdout,
5330	"Tr no = %3d\tSmooth PS # = %3d\tSmooth PI # = %3d\tIntroduced # = %d\n", i,
5331	psCount, piNdCount, introducedCount);
5332	st_free_table(supportTable);
5333	array_free(smoothVarBddIdArray);
5334	}
5335	st_free_table(nsBddIdTable);
5336	st_free_table(psBddIdTable);
5337	}
5338
5339	/Function******************************************************************
5340
5341	Synopsis [Prints Ids of an array of BDDs.]
5342
5343	Description [Prints Ids of an array of BDDs.]
5344
5345	SideEffects []
5346
5347	******************************************************************************/
5348	static void
5349	PrintBddIdFromBddArray(array_t *bddArray)
5350	{
5351	int i;
5352	array_t *idArray = bdd_get_varids(bddArray);
5353	fprintf(vis_stdout,
5354	"************** printing bdd ids from the bdd array *********\n");
5355	fprintf(vis_stdout,"%d::\t", array_n(idArray));
5356	for (i=0;i<array_n(idArray); i++) {
5357	fprintf(vis_stdout," %d ", (int)array_fetch(int, idArray, i));
5358	}
5359	fprintf(vis_stdout,"\n******************\n");
5360	array_free(idArray);
5361	return;
5362	}
5363
5364	/Function******************************************************************
5365
5366	Synopsis [Prints the integers from a symbol table.]
5367
5368	Description [Prints the integers from a symbol table.]
5369
5370	SideEffects []
5371
5372	******************************************************************************/
5373	static void
5374	PrintBddIdTable(st_table *idTable)
5375	{
5376	st_generator *stgen;
5377	long varId;
5378	fprintf(vis_stdout,
5379	"************** printing bdd ids from the id table *********\n");
5380	fprintf(vis_stdout,"%d::\t", st_count(idTable));
5381	st_foreach_item(idTable, stgen, &varId, NIL(char *)) {
5382	fprintf(vis_stdout," %d ", (int) varId);
5383	}
5384	fprintf(vis_stdout,"\n******************\n");
5385	return;
5386	}
5387
5388	/Function******************************************************************
5389
5390	Synopsis [Traverses the partition recursively, creating the
5391	relations for the intermediate vertices.]
5392
5393	Description [Traverses the partition recursively, creating the
5394	relations for the intermediate vertices.]
5395
5396	SideEffects []
5397
5398	******************************************************************************/
5399	static void
5400	PartitionTraverseRecursively(mdd_manager mddManager, vertex_t vertex,
5401	int mddId, st_table *vertexTable,
5402	array_t *relationArray,
5403	st_table *domainQuantifyVarMddIdTable,
5404	array_t *quantifyVarMddIdArray)
5405	{
5406	Mvf_Function_t *mvf;
5407	lsList faninEdges;
5408	lsGen gen;
5409	vertex_t *faninVertex;
5410	edge_t *faninEdge;
5411	array_t *varBddRelationArray;
5412
5413	if (st_is_member(vertexTable, (char *)vertex)) return;
5414	st_insert(vertexTable, (char *)vertex, NIL(char));
5415	if (mddId != -1) { /* This is not the next state function node */
5416	/* There is an mdd variable associated with this vertex */
5417	array_insert_last(int, quantifyVarMddIdArray, mddId);
5418	mvf = Part_VertexReadFunction(vertex);
5419	/relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);/
5420	varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf);
5421	array_append(relationArray, varBddRelationArray);
5422	array_free(varBddRelationArray);
5423	/array_insert_last(mdd_t , relationArray, relation);*/
5424	}
5425	faninEdges = g_get_in_edges(vertex);
5426	if (lsLength(faninEdges) == 0) return;
5427	lsForEachItem(faninEdges, gen, faninEdge) {
5428	faninVertex = g_e_source(faninEdge);
5429	mddId = Part_VertexReadMddId(faninVertex);
5430	if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) {
5431	/* This is either domain var or quantify var */
5432	/* continue */
5433	continue;
5434	}
5435	PartitionTraverseRecursively(mddManager, faninVertex, mddId, vertexTable,
5436	relationArray,
5437	domainQuantifyVarMddIdTable,
5438	quantifyVarMddIdArray);
5439	}
5440	}
5441
5442
5443	/Function******************************************************************
5444
5445	Synopsis [Prints the partition recursively.]
5446
5447	Description [Prints the partition recursively.]
5448
5449	SideEffects []
5450
5451	******************************************************************************/
5452	static void
5453	PrintPartitionRecursively(vertex_t vertex, st_table vertexTable, int indent)
5454	{
5455	int i;
5456	lsList faninEdges;
5457	lsGen gen;
5458	vertex_t *faninVertex;
5459	edge_t *faninEdge;
5460
5461	if (st_is_member(vertexTable, (char *)vertex)) return;
5462	st_insert(vertexTable, (char *)vertex, NIL(char));
5463	for(i=0; i<= indent; i++) fprintf(vis_stdout," ");
5464	fprintf(vis_stdout,"%s %d\n", Part_VertexReadName(vertex),
5465	Part_VertexReadMddId(vertex));
5466	faninEdges = g_get_in_edges(vertex);
5467	if (lsLength(faninEdges) == 0) return;
5468	lsForEachItem(faninEdges, gen, faninEdge) {
5469	faninVertex = g_e_source(faninEdge);
5470	PrintPartitionRecursively(faninVertex, vertexTable,indent+2);
5471	}
5472	}
5473
5474	/Function******************************************************************
5475
5476	Synopsis [Recompute partial image by relaxing the parameters.]
5477
5478	Description [Recompute partial image by relaxing the
5479	parameters. First the threshold to trigger approximation is
5480	increased and then the threshold to approximate is increased. If
5481	both fail to produce new states, the exact image is computed (no
5482	approximations).Partial flag comes in indicating whether partial
5483	images are allowed, and leave indicating whether the image was
5484	partial or not. ASSUME that toCareSet is in terms of
5485	function->domainVars.]
5486
5487	SideEffects [partial flag is modified with each image
5488	computation. IMPORTANT NOTE: image may be in terms of domain
5489	variables even when the reverse is expected.]
5490
5491	******************************************************************************/
5492	static bdd_t *
5493	RecomputeImageIfNecessary(ImgFunctionData_t *functionData,
5494	mdd_manager *mddManager,
5495	bdd_t *domainSubset,
5496	array_t *relationArray,
5497	array_t *arraySmoothVarBddArray,
5498	array_t *smoothVarCubeArray,
5499	int verbosity,
5500	ImgPartialImageOption_t *PIoption,
5501	array_t *toCareSetArray,
5502	boolean *partial, boolean lazySiftFlag)
5503	{
5504	int oldPIThreshold = 0, oldPISize;
5505	double oldClippingFrac = IMG_PI_CLIP_DEPTH;
5506	boolean realRequired = FALSE;
5507	mdd_t *image = NIL(mdd_t);
5508
5509	/* relax values to compute a non-trivial partial image */
5510	if (PIoption->partialImageMethod == Img_PIApprox_c) {
5511	oldPIThreshold = PIoption->partialImageThreshold;
5512	PIoption->partialImageThreshold *= 2;
5513	if (!PIoption->partialImageThreshold)
5514	PIoption->partialImageThreshold = IMG_PI_SP_THRESHOLD;
5515	} else if (PIoption->partialImageMethod == Img_PIClipping_c) {
5516	oldClippingFrac = PIoption->clippingDepthFrac;
5517	PIoption->clippingDepthFrac =
5518	(PIoption->clippingDepthFrac < IMG_PI_CLIP_DEPTH_FINAL) ?
5519	IMG_PI_CLIP_DEPTH_FINAL : PIoption->clippingDepthFrac;
5520	}
5521	if (((PIoption->partialImageMethod == Img_PIClipping_c) &&
5522	(oldClippingFrac != PIoption->clippingDepthFrac)) \|\|
5523	(PIoption->partialImageMethod == Img_PIApprox_c)) {
5524	if (verbosity >= 2) {
5525	fprintf(vis_stdout,
5526	"IMG: No new states, computing image again with relaxed thresholds.\n");
5527	if (PIoption->partialImageMethod == Img_PIApprox_c) {
5528	fprintf(vis_stdout, "IMG: Relaxed hd_partial_image_threshold to %d\n",
5529	PIoption->partialImageThreshold);
5530	} else if (PIoption->partialImageMethod == Img_PIClipping_c) {
5531	fprintf(vis_stdout,
5532	"IMG: Relaxed hd_partial_image_clipping_depth to %g\n",
5533	PIoption->clippingDepthFrac);
5534	}
5535	}
5536
5537	*partial = TRUE;
5538	/* if values were relaxed, compute image again. */
5539	image = BddLinearAndSmooth(mddManager, domainSubset, relationArray,
5540	arraySmoothVarBddArray, smoothVarCubeArray,
5541	verbosity, PIoption, partial, lazySiftFlag);
5542
5543	/* check if new states were produced. */
5544	if (*partial) {
5545	if (bdd_leq_array(image, toCareSetArray, 1, 0)) {
5546	bdd_free(image);
5547	if (PIoption->partialImageMethod == Img_PIApprox_c) {
5548	/* relax approximation values some more. */
5549	oldPISize = PIoption->partialImageSize;
5550	PIoption->partialImageSize *= 2;
5551	if (!PIoption->partialImageSize)
5552	PIoption->partialImageSize = IMG_PI_SP_THRESHOLD;
5553
5554	if (verbosity >= 2) {
5555	fprintf(vis_stdout,
5556	"IMG: No new states, computing image again with relaxed thresholds.\n");
5557	fprintf(vis_stdout, "IMG: Relaxed hd_partial_image_size to %d\n",
5558	PIoption->partialImageSize);
5559	}
5560
5561	*partial = TRUE;
5562	image = BddLinearAndSmooth(mddManager, domainSubset, relationArray,
5563	arraySmoothVarBddArray, smoothVarCubeArray,
5564	verbosity, PIoption, partial,
5565	lazySiftFlag);
5566	PIoption->partialImageSize = oldPISize;
5567
5568	/* check if new states were produced. */
5569	if (*partial) {
5570	if (bdd_leq_array(image, toCareSetArray, 1, 0)) {
5571	bdd_free(image);
5572	realRequired = TRUE;
5573	}
5574	}
5575	} else if (PIoption->partialImageMethod == Img_PIClipping_c) {
5576	/* compute real image since clipping depth cannot be increased. */
5577	realRequired = TRUE;
5578	}
5579	}
5580	} /* require recomputation */
5581	} else { /* clipping depth could not be increased. */
5582	/* compute real image since clipping depth cannot be increased. */
5583	realRequired = TRUE;
5584	}
5585
5586	/* reset the values to the orginal values. */
5587	if (PIoption->partialImageMethod == Img_PIClipping_c) {
5588	PIoption->clippingDepthFrac = oldClippingFrac;
5589	} else if (PIoption->partialImageMethod == Img_PIApprox_c) {
5590	PIoption->partialImageThreshold = oldPIThreshold;
5591	}
5592	/* if the actual image is required compute it. */
5593	if (realRequired) {
5594	if (verbosity >= 2) {
5595	fprintf(vis_stdout, "IMG: No new states, computing exact image.\n");
5596	}
5597	*partial = FALSE;
5598	image = BddLinearAndSmooth(mddManager, domainSubset, relationArray,
5599	arraySmoothVarBddArray, smoothVarCubeArray,
5600	verbosity, PIoption, partial, lazySiftFlag);
5601	assert(!(*partial));
5602	}
5603
5604	return (image);
5605	} /* end of RecomputeImageIfNecessary */
5606
5607
5608	/Function******************************************************************
5609
5610	Synopsis [Approximate intermediate product according to method.]
5611
5612	Description [Approximate intermediate product according to method.]
5613
5614	SideEffects []
5615
5616	******************************************************************************/
5617	static bdd_t *
5618	ComputeSubsetOfIntermediateProduct(bdd_t *product,
5619	ImgPartialImageOption_t *PIoption)
5620	{
5621	int partialImageSize = PIoption->partialImageSize;
5622	int nvars = PIoption->nvars;
5623	bdd_t *newProduct;
5624
5625	switch (PIoption->partialImageApproxMethod) {
5626	case BDD_APPROX_HB:
5627	{
5628	int tempSize;
5629	tempSize = (partialImageSize < IMG_PI_SP_THRESHOLD) ?
5630	IMG_PI_SP_THRESHOLD : partialImageSize;
5631	newProduct = bdd_approx_hb(product,
5632	(bdd_approx_dir_t)BDD_UNDER_APPROX,
5633	nvars, tempSize);
5634	break;
5635	}
5636	case BDD_APPROX_SP:
5637	{
5638	int tempSize;
5639	tempSize = (partialImageSize < IMG_PI_SP_THRESHOLD) ?
5640	IMG_PI_SP_THRESHOLD : partialImageSize;
5641	newProduct = bdd_approx_sp(product,
5642	(bdd_approx_dir_t)BDD_UNDER_APPROX,
5643	nvars, tempSize, 0);
5644	break;
5645	}
5646	case BDD_APPROX_UA:
5647	newProduct = bdd_approx_ua(product,
5648	(bdd_approx_dir_t)BDD_UNDER_APPROX,
5649	nvars, partialImageSize,
5650	0, PIoption->quality);
5651	break;
5652	case BDD_APPROX_RUA:
5653	newProduct = bdd_approx_remap_ua(product,
5654	(bdd_approx_dir_t)BDD_UNDER_APPROX,
5655	0, partialImageSize,
5656	PIoption->quality);
5657	break;
5658	case BDD_APPROX_COMP:
5659	{
5660	newProduct = bdd_approx_compress(product,
5661	(bdd_approx_dir_t)BDD_UNDER_APPROX,
5662	nvars, partialImageSize);
5663	}
5664	break;
5665	case BDD_APPROX_BIASED_RUA:
5666	newProduct = bdd_approx_biased_rua(product,
5667	(bdd_approx_dir_t)BDD_UNDER_APPROX,
5668	PIoption->bias,
5669	0, partialImageSize,
5670	PIoption->quality,
5671	PIoption->qualityBias);
5672	break;
5673	default :
5674	newProduct = bdd_approx_remap_ua(product,
5675	(bdd_approx_dir_t)BDD_UNDER_APPROX,
5676	0, partialImageSize,
5677	PIoption->quality);
5678	break;
5679	}
5680	return newProduct;
5681	} /* end of ComputeSubsetOfIntermediateProduct */
5682
5683	/Function******************************************************************
5684
5685	Synopsis [Clipping and-abstract]
5686
5687	Description [Compute clipping and-abstract. Try twice. If fail,
5688	compute exact and-abstract]
5689
5690	SideEffects [partial flag is modified.]
5691
5692	******************************************************************************/
5693	static bdd_t *
5694	ComputeClippedAndAbstract(bdd_t *product,
5695	bdd_t *relation,
5696	array_t *smoothVarBddArray,
5697	int nvars,
5698	int clippingDepth,
5699	boolean *partial,
5700	int verbosity)
5701	{
5702	bdd_t *tmpProduct;
5703
5704	/* compute clipped image */
5705	tmpProduct = bdd_clipping_and_smooth(product, relation,
5706	smoothVarBddArray, clippingDepth, 0);
5707	/* if product is zero, compute clipped image with increased
5708	* clipping depth
5709	*/
5710	if (bdd_is_tautology(tmpProduct, 0)) {
5711	bdd_free(tmpProduct);
5712	tmpProduct = bdd_clipping_and_smooth(product, relation,
5713	smoothVarBddArray,
5714	(int) (nvars*IMG_PI_CLIP_DEPTH_FINAL),
5715	0);
5716
5717	/* if clipped image is zero, compute unclipped image */
5718	if (bdd_is_tautology(tmpProduct, 0)) {
5719	if (verbosity >= 2) {
5720	fprintf(vis_stdout,
5721	"IMG: Clipping failed, computing exact and-abstract\n");
5722	}
5723	bdd_free(tmpProduct);
5724	tmpProduct = bdd_and_smooth(product, relation,
5725	smoothVarBddArray);
5726	} else *partial = TRUE;
5727
5728	} else *partial = TRUE;
5729
5730	return tmpProduct;
5731	} /* end of ComputeClippedAndAbstract */
5732
5733
5734	/Function******************************************************************
5735
5736	Synopsis [Copy an array of bdd array.]
5737
5738	Description [Copy an array of bdd array.]
5739
5740	SideEffects []
5741
5742	******************************************************************************/
5743	static array_t *
5744	CopyArrayBddArray(array_t *arrayBddArray)
5745	{
5746	int i, j;
5747	array_t newArrayBddArray = array_alloc(array_t , 0);
5748	array_t bddArray, newBddArray;
5749	mdd_t *bdd;
5750
5751	for (i = 0; i < array_n(arrayBddArray); i++) {
5752	bddArray = array_fetch(array_t *, arrayBddArray, i);
5753	newBddArray = array_alloc(mdd_t *, 0);
5754	for (j = 0; j < array_n(bddArray); j++) {
5755	bdd = array_fetch(mdd_t *, bddArray, j);
5756	array_insert(mdd_t *, newBddArray, j, bdd_dup(bdd));
5757	}
5758	array_insert(array_t *, newArrayBddArray, i, newBddArray);
5759	}
5760
5761	return(newArrayBddArray);
5762	}
5763
5764
5765	/Function******************************************************************
5766
5767	Synopsis [Prints info of the partitioned transition relation.]
5768
5769	Description [Prints info of the partitioned transition relation.]
5770
5771	SideEffects []
5772
5773	******************************************************************************/
5774	static void
5775	PrintPartitionedTransitionRelation(mdd_manager *mddManager,
5776	Iwls95Info_t *info,
5777	Img_DirectionType directionType)
5778	{
5779	array_t *relationArray;
5780	array_t *arraySmoothVarBddArray;
5781
5782	if (directionType == Img_Forward_c) {
5783	relationArray = info->fwdClusteredRelationArray;
5784	arraySmoothVarBddArray = info->fwdArraySmoothVarBddArray;
5785	} else if (directionType == Img_Backward_c) {
5786	relationArray = info->bwdClusteredRelationArray;
5787	arraySmoothVarBddArray = info->bwdArraySmoothVarBddArray;
5788	} else {
5789	return;
5790	}
5791
5792	ImgPrintPartitionedTransitionRelation(mddManager, relationArray,
5793	arraySmoothVarBddArray);
5794	}
5795
5796
5797	/Function******************************************************************
5798
5799	Synopsis [Reorder partitioned transition relation.]
5800
5801	Description [Reorder partitioned transition relation.]
5802
5803	SideEffects []
5804
5805	******************************************************************************/
5806	static void
5807	ReorderPartitionedTransitionRelation(Iwls95Info_t *info,
5808	ImgFunctionData_t *functionData,
5809	Img_DirectionType directionType)
5810	{
5811	array_t *domainVarMddIdArray = functionData->domainVars;
5812	array_t *rangeVarMddIdArray = functionData->rangeVars;
5813	array_t *quantifyVarMddIdArray = array_dup(functionData->quantifyVars);
5814	graph_t *mddNetwork = functionData->mddNetwork;
5815	mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork);
5816	array_t rangeVarBddArray, domainVarBddArray, *quantifyVarBddArray;
5817	array_t *clusteredRelationArray;
5818	st_table *varsTable = st_init_table(st_numcmp, st_numhash);
5819	int i, j, k, mddId;
5820	array_t smoothVarBddArray, arraySmoothVarBddArray;
5821	mdd_t *mdd;
5822	array_t *supportIdArray;
5823
5824	/* Finds the variables which are neither state variable nor primary input
5825	* from previous smooth variable array, and put those variable into
5826	* quantify variable array.
5827	*/
5828	for (i =0 ; i< array_n(domainVarMddIdArray); i++) {
5829	mddId = array_fetch(int, domainVarMddIdArray, i);
5830	st_insert(varsTable, (char *)(long)mddId, NIL(char));
5831	}
5832	for (i = 0; i < array_n(rangeVarMddIdArray); i++) {
5833	mddId = array_fetch(int, rangeVarMddIdArray, i);
5834	st_insert(varsTable, (char *)(long)mddId, NIL(char));
5835	}
5836	for (i = 0; i < array_n(quantifyVarMddIdArray); i++) {
5837	mddId = array_fetch(int, quantifyVarMddIdArray, i);
5838	st_insert(varsTable, (char *)(long)mddId, NIL(char));
5839	}
5840	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c)
5841	arraySmoothVarBddArray = info->fwdArraySmoothVarBddArray;
5842	else
5843	arraySmoothVarBddArray = info->bwdArraySmoothVarBddArray;
5844	for (i = 0; i < array_n(arraySmoothVarBddArray); i++) {
5845	smoothVarBddArray = array_fetch(array_t *, arraySmoothVarBddArray, i);
5846	for (j = 0; j < array_n(smoothVarBddArray); j++) {
5847	mdd = array_fetch(mdd_t *, smoothVarBddArray, j);
5848	supportIdArray = mdd_get_support(mddManager, mdd);
5849	for (k = 0; k < array_n(supportIdArray); k++) {
5850	mddId = array_fetch(int, supportIdArray, k);
5851	if (!st_lookup(varsTable, (char )(long)mddId, NIL(char ))) {
5852	array_insert_last(int, quantifyVarMddIdArray, mddId);
5853	st_insert(varsTable, (char *)(long)mddId, NIL(char));
5854	}
5855	}
5856	array_free(supportIdArray);
5857	}
5858	}
5859	st_free_table(varsTable);
5860
5861	/* Get the Bdds from Mdd Ids */
5862	rangeVarBddArray = functionData->rangeBddVars;
5863	domainVarBddArray = functionData->domainBddVars;
5864	quantifyVarBddArray = mdd_id_array_to_bdd_array(mddManager,
5865	quantifyVarMddIdArray);
5866	array_free(quantifyVarMddIdArray);
5867
5868	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c) {
5869	clusteredRelationArray = info->fwdClusteredRelationArray;
5870	mdd_array_array_free(info->fwdArraySmoothVarBddArray);
5871	info->fwdClusteredRelationArray = NIL(array_t);
5872	info->fwdArraySmoothVarBddArray = NIL(array_t);
5873	if (info->method == Img_Iwls95_c) {
5874	OrderRelationArray(mddManager, clusteredRelationArray,
5875	domainVarBddArray, quantifyVarBddArray,
5876	rangeVarBddArray, info->option,
5877	&info->fwdClusteredRelationArray,
5878	&info->fwdArraySmoothVarBddArray);
5879	} else if (info->method == Img_Mlp_c) {
5880	ImgMlpOrderRelationArray(mddManager, clusteredRelationArray,
5881	domainVarBddArray, quantifyVarBddArray,
5882	rangeVarBddArray, Img_Forward_c,
5883	&info->fwdClusteredRelationArray,
5884	&info->fwdArraySmoothVarBddArray,
5885	info->option);
5886	} else
5887	assert(0);
5888	mdd_array_free(clusteredRelationArray);
5889
5890	if (functionData->createVarCubesFlag) {
5891	if (info->fwdSmoothVarCubeArray)
5892	mdd_array_free(info->fwdSmoothVarCubeArray);
5893	info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
5894	info->fwdArraySmoothVarBddArray);
5895	}
5896
5897	if (info->option->verbosity > 2) {
5898	PrintPartitionedTransitionRelation(mddManager, info, Img_Forward_c);
5899	}
5900	}
5901
5902	if (directionType == Img_Backward_c \|\| directionType == Img_Both_c) {
5903	clusteredRelationArray = info->bwdClusteredRelationArray;
5904	mdd_array_array_free(info->bwdArraySmoothVarBddArray);
5905	info->bwdClusteredRelationArray = NIL(array_t);
5906	info->bwdArraySmoothVarBddArray = NIL(array_t);
5907	if (info->method == Img_Iwls95_c) {
5908	OrderRelationArray(mddManager, clusteredRelationArray,
5909	rangeVarBddArray, quantifyVarBddArray,
5910	domainVarBddArray, info->option,
5911	&info->bwdClusteredRelationArray,
5912	&info->bwdArraySmoothVarBddArray);
5913	} else if (info->method == Img_Mlp_c) {
5914	ImgMlpOrderRelationArray(mddManager, clusteredRelationArray,
5915	domainVarBddArray, quantifyVarBddArray,
5916	rangeVarBddArray, Img_Backward_c,
5917	&info->bwdClusteredRelationArray,
5918	&info->bwdArraySmoothVarBddArray, info->option);
5919	} else
5920	assert(0);
5921	mdd_array_free(clusteredRelationArray);
5922
5923	if (functionData->createVarCubesFlag) {
5924	if (info->bwdSmoothVarCubeArray)
5925	mdd_array_free(info->bwdSmoothVarCubeArray);
5926	info->bwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
5927	info->bwdArraySmoothVarBddArray);
5928	}
5929
5930	if (info->option->verbosity > 2) {
5931	PrintPartitionedTransitionRelation(mddManager, info, Img_Backward_c);
5932	}
5933	}
5934
5935	/* Free the Bdd arrays */
5936	mdd_array_free(quantifyVarBddArray);
5937	}
5938
5939
5940	/Function******************************************************************
5941
5942	Synopsis [Updates quantification schedule.]
5943
5944	Description [Updates quantification schedule.]
5945
5946	SideEffects []
5947
5948	******************************************************************************/
5949	static void
5950	UpdateQuantificationSchedule(Iwls95Info_t *info,
5951	ImgFunctionData_t *functionData,
5952	Img_DirectionType directionType)
5953	{
5954	graph_t *mddNetwork = functionData->mddNetwork;
5955	mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork);
5956	array_t *clusteredRelationArray;
5957	st_table *quantifyVarsTable;
5958	var_set_t *supportVarSet;
5959	int i, j, id, nRelations;
5960	int pos;
5961	long longid;
5962	array_t smoothVarBddArray, *smoothVarBddArrayPtr;
5963	bdd_t bdd, relation;
5964	st_generator *gen;
5965
5966	if (directionType == Img_Forward_c \|\| directionType == Img_Both_c) {
5967	nRelations = array_n(info->fwdClusteredRelationArray);
5968	quantifyVarsTable = st_init_table(st_numcmp, st_numhash);
5969	for (i = 0; i <= nRelations; i++) {
5970	smoothVarBddArray = array_fetch(array_t *,
5971	info->fwdArraySmoothVarBddArray, i);
5972	for (j = 0; j < array_n(smoothVarBddArray); j++) {
5973	bdd = array_fetch(mdd_t *, smoothVarBddArray, j);
5974	id = (int)bdd_top_var_id(bdd);
5975	st_insert(quantifyVarsTable, (char *)(long)id, NIL(char));
5976	}
5977	}
5978
5979	clusteredRelationArray = info->fwdClusteredRelationArray;
5980	for (i = 0; i < nRelations; i++) {
5981	relation = array_fetch(bdd_t *, clusteredRelationArray, i);
5982	supportVarSet = bdd_get_support(relation);
5983	for (j = 0; j < supportVarSet->n_elts; j++) {
5984	if (var_set_get_elt(supportVarSet, j) == 1) {
5985	if (st_is_member(quantifyVarsTable, (char *)(long)j))
5986	st_insert(quantifyVarsTable, (char )(long)j, (char )(long)(i+1));
5987	}
5988	}
5989	var_set_free(supportVarSet);
5990	}
5991
5992	mdd_array_array_free(info->fwdArraySmoothVarBddArray);
5993	info->fwdArraySmoothVarBddArray = array_alloc(array_t *, nRelations + 1);
5994	smoothVarBddArrayPtr = ALLOC(array_t , sizeof(array_t ) * (nRelations+1));
5995	for (i = 0; i <= nRelations; i++) {
5996	smoothVarBddArray = array_alloc(bdd_t *, 0);
5997	smoothVarBddArrayPtr[i] = smoothVarBddArray;
5998	array_insert(array_t *, info->fwdArraySmoothVarBddArray, i,
5999	smoothVarBddArray);
6000	}
6001
6002	st_foreach_item_int(quantifyVarsTable, gen, &longid, &pos) {
6003	id = (int) longid;
6004	smoothVarBddArray = array_fetch(array_t *,
6005	info->fwdArraySmoothVarBddArray, pos);
6006	bdd = bdd_var_with_index(mddManager, id);
6007	array_insert_last(bdd_t *, smoothVarBddArray, bdd);
6008	}
6009
6010	FREE(smoothVarBddArrayPtr);
6011	st_free_table(quantifyVarsTable);
6012
6013	if (functionData->createVarCubesFlag) {
6014	if (info->fwdSmoothVarCubeArray)
6015	mdd_array_free(info->fwdSmoothVarCubeArray);
6016	info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
6017	info->fwdArraySmoothVarBddArray);
6018	}
6019
6020	if (info->option->verbosity > 2) {
6021	PrintPartitionedTransitionRelation(mddManager, info, Img_Forward_c);
6022	}
6023	}
6024
6025	if (directionType == Img_Backward_c \|\| directionType == Img_Both_c) {
6026	nRelations = array_n(info->bwdClusteredRelationArray);
6027	quantifyVarsTable = st_init_table(st_numcmp, st_numhash);
6028	for (i = 0; i <= nRelations; i++) {
6029	smoothVarBddArray = array_fetch(array_t *,
6030	info->bwdArraySmoothVarBddArray, i);
6031	for (j = 0; j < array_n(smoothVarBddArray); j++) {
6032	bdd = array_fetch(mdd_t *, smoothVarBddArray, j);
6033	id = (int)bdd_top_var_id(bdd);
6034	st_insert(quantifyVarsTable, (char )(long)id, (char )(long)0);
6035	}
6036	}
6037
6038	clusteredRelationArray = info->bwdClusteredRelationArray;
6039	for (i = 0; i < nRelations; i++) {
6040	relation = array_fetch(bdd_t *, clusteredRelationArray, i);
6041	supportVarSet = bdd_get_support(relation);
6042	for (j = 0; j < supportVarSet->n_elts; j++) {
6043	if (var_set_get_elt(supportVarSet, j) == 1) {
6044	if (st_is_member(quantifyVarsTable, (char *)(long)j))
6045	st_insert(quantifyVarsTable, (char )(long)j, (char )(long)(i+1));
6046	}
6047	}
6048	var_set_free(supportVarSet);
6049	}
6050
6051	mdd_array_array_free(info->bwdArraySmoothVarBddArray);
6052	info->bwdArraySmoothVarBddArray = array_alloc(array_t *, nRelations + 1);
6053	smoothVarBddArrayPtr = ALLOC(array_t , sizeof(array_t ) * (nRelations+1));
6054	for (i = 0; i <= nRelations; i++) {
6055	smoothVarBddArray = array_alloc(bdd_t *, 0);
6056	smoothVarBddArrayPtr[i] = smoothVarBddArray;
6057	array_insert(array_t *, info->bwdArraySmoothVarBddArray, i,
6058	smoothVarBddArray);
6059	}
6060
6061	st_foreach_item_int(quantifyVarsTable, gen, &longid, &pos) {
6062	id = (int) longid;
6063	smoothVarBddArray = array_fetch(array_t *,
6064	info->bwdArraySmoothVarBddArray, pos);
6065	bdd = bdd_var_with_index(mddManager, id);
6066	array_insert_last(bdd_t *, smoothVarBddArray, bdd);
6067	}
6068
6069	FREE(smoothVarBddArrayPtr);
6070	st_free_table(quantifyVarsTable);
6071
6072	if (functionData->createVarCubesFlag) {
6073	if (info->bwdSmoothVarCubeArray)
6074	mdd_array_free(info->bwdSmoothVarCubeArray);
6075	info->bwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager,
6076	info->bwdArraySmoothVarBddArray);
6077	}
6078
6079	if (info->option->verbosity > 2) {
6080	PrintPartitionedTransitionRelation(mddManager, info, Img_Backward_c);
6081	}
6082	}
6083	}
6084
6085
6086	/Function******************************************************************
6087
6088	Synopsis [Returns array of cubes of smoothing variables.]
6089
6090	Description [Returns array of cubes of smoothing variables.]
6091
6092	SideEffects []
6093
6094	******************************************************************************/
6095	static array_t *
6096	MakeSmoothVarCubeArray(mdd_manager mddManager, array_t arraySmoothVarBddArray)
6097	{
6098	int i, j;
6099	array_t *smoothVarBddArray;
6100	array_t cubeArray = array_alloc(mdd_t , 0);
6101	mdd_t cube, var, *tmp;
6102
6103	arrayForEachItem(array_t *, arraySmoothVarBddArray, i, smoothVarBddArray) {
6104	cube = mdd_one(mddManager);
6105	arrayForEachItem(mdd_t *, smoothVarBddArray, j, var) {
6106	tmp = mdd_and(cube, var, 1, 1);
6107	mdd_free(cube);
6108	cube = tmp;
6109	}
6110	array_insert_last(mdd_t *, cubeArray, cube);
6111	}
6112	return(cubeArray);
6113	}
6114
6115
6116	/Function******************************************************************
6117
6118	Synopsis [Eliminates dependent variables from transition relation.]
6119
6120	Description [Eliminates dependent variables from a transition
6121	relation. Returns a simplified copy of the given states if successful;
6122	NULL otherwise.]
6123
6124	SideEffects [relationArray is also modified.]
6125
6126	SeeAlso []
6127
6128	******************************************************************************/
6129	static mdd_t *
6130	TrmEliminateDependVars(Img_ImageInfo_t imageInfo, array_t relationArray,
6131	mdd_t states, mdd_t *dependRelations)
6132	{
6133	int nDependVars;
6134	mdd_t *newStates;
6135	Iwls95Info_t info = (Iwls95Info_t ) imageInfo->methodData;
6136
6137	newStates = ImgTrmEliminateDependVars(&imageInfo->functionData, relationArray,
6138	states, dependRelations, &nDependVars);
6139	if (nDependVars) {
6140	if (imageInfo->verbosity > 0)
6141	(void)fprintf(vis_stdout, "Eliminated %d vars.\n", nDependVars);
6142	info->averageFoundDependVars = (info->averageFoundDependVars *
6143	(float)info->nFoundDependVars + (float)nDependVars) /
6144	(float)(info->nFoundDependVars + 1);
6145	info->nFoundDependVars++;
6146	}
6147
6148	info->nPrevEliminatedFwd = nDependVars;
6149	return(newStates);
6150	} /* end of TfmEliminateDependVars */
6151
6152
6153	/Function******************************************************************
6154
6155	Synopsis [Comparison function used by qsort.]
6156
6157	Description [Comparison function used by qsort to order the
6158	variables according to their signatures.]
6159
6160	SideEffects [None]
6161
6162	******************************************************************************/
6163	static int
6164	TrmSignatureCompare(int ptrX, int ptrY)
6165	{
6166	if (signatures[ptrY] > signatures[ptrX])
6167	return(1);
6168	if (signatures[ptrY] < signatures[ptrX])
6169	return(-1);
6170	return(0);
6171	} /* end of TrmSignatureCompare */
6172
6173
6174	/Function******************************************************************
6175
6176	Synopsis [Setups lazy sifting.]
6177
6178	Description [Setups lazy sifting.]
6179
6180	SideEffects [None]
6181
6182	******************************************************************************/
6183	static void
6184	SetupLazySifting(mdd_manager mddManager, array_t bddRelationArray,
6185	array_t domainVarBddArray, array_t quantifyVarBddArray,
6186	array_t *rangeVarBddArray, int verbosity)
6187	{
6188	int i, id, psId, nsId, psLevel, nsLevel;
6189	int nVars = bdd_num_vars(mddManager);
6190	int nUngroup = 0;
6191	int nGroup = 0;
6192	int nConst = 0;
6193	int *nonLambda = ALLOC(int, nVars);
6194	int nLambda = 0;
6195	int nDepend1to1 = 0;
6196	int nIndepend1to1 = 0;
6197	int nPairPsOnce = 0;
6198	int pairPsId;
6199	int constFlag;
6200	int dependFlag;
6201	int nDependPs;
6202	int nDependPi;
6203	bdd_t* relation;
6204	var_set_t* supIds;
6205	bdd_t bdd, psVar, *nsVar;
6206
6207	bdd_discard_all_var_groups(mddManager);
6208	for (i = 0; i < array_n(quantifyVarBddArray); i++) {
6209	bdd = array_fetch(bdd_t *, quantifyVarBddArray, i);
6210	id = bdd_top_var_id(bdd);
6211	bdd_set_pair_index(mddManager, id, id);
6212	bdd_set_pi_var(mddManager, id);
6213	bdd_reset_var_to_be_grouped(mddManager, id);
6214	}
6215
6216	for (i = 0; i < array_n(rangeVarBddArray); i++) {
6217	psVar = array_fetch(bdd_t *, domainVarBddArray, i);
6218	nsVar = array_fetch(bdd_t *, rangeVarBddArray, i);
6219	psId = bdd_top_var_id(psVar);
6220	nsId = bdd_top_var_id(nsVar);
6221	bdd_set_pair_index(mddManager, psId, nsId);
6222	bdd_set_pair_index(mddManager, nsId, psId);
6223	bdd_set_ps_var(mddManager, psId);
6224	bdd_set_ns_var(mddManager, nsId);
6225	bdd_reset_var_to_be_grouped(mddManager, psId);
6226	bdd_set_var_to_be_grouped(mddManager, nsId);
6227	}
6228
6229	if (array_n(domainVarBddArray) > array_n(rangeVarBddArray)) {
6230	for (i = array_n(rangeVarBddArray); i < array_n(domainVarBddArray); i++) {
6231	bdd = array_fetch(bdd_t *, domainVarBddArray, i);
6232	id = bdd_top_var_id(bdd);
6233	bdd_set_pair_index(mddManager, id, id);
6234	bdd_set_pi_var(mddManager, id);
6235	bdd_reset_var_to_be_grouped(mddManager, id);
6236	}
6237	}
6238
6239	memset(nonLambda, 0, sizeof(int) * nVars);
6240	for (i = 0; i < array_n(bddRelationArray); i++) {
6241	nsId = -1;
6242	pairPsId = -1;
6243	constFlag = 1;
6244	dependFlag = 0;
6245	nDependPs = 0;
6246	nDependPi = 0;
6247	relation = array_fetch(bdd_t *, bddRelationArray, i);
6248	supIds = bdd_get_support(relation);
6249
6250	for (id = 0; id < nVars; id++) {
6251	if (var_set_get_elt(supIds, id) == 1) {
6252	if (bdd_is_ns_var(mddManager, id)) {
6253	pairPsId = bdd_read_pair_index(mddManager, id);
6254	nsId = id;
6255	} else if (bdd_is_ps_var(mddManager, id)) {
6256	constFlag = 0; /* nonconst next sate function */
6257	nonLambda[id]++;
6258	psId = id;
6259	/* At least one next state function depends on psvar id */
6260	nDependPs++;
6261	} else {
6262	constFlag = 0; /* nonconst next state function */
6263	nDependPi++;
6264	}
6265	}
6266	}
6267	if (nsId >= 0) {
6268	/* bitwise transition relation depends on some nsvar */
6269	for (id = 0; id < nVars; id++) {
6270	if (var_set_get_elt(supIds, id) == 1) {
6271	if (pairPsId == id) {
6272	/* dependendent state pair */
6273	nGroup++;
6274	dependFlag = 1;
6275	}
6276	}
6277	}
6278	if (dependFlag != 1) {
6279	/* independent state pair */
6280	nUngroup++;
6281	if (constFlag == 1) {
6282	/* next state function is constant */
6283	psLevel = bdd_get_level_from_id(mddManager, pairPsId);
6284	nsLevel = bdd_get_level_from_id(mddManager, nsId);
6285	if (psLevel == nsLevel - 1) {
6286	bdd = bdd_var_with_index(mddManager, pairPsId);
6287	bdd_new_var_block(bdd, 2);
6288	bdd_free(bdd);
6289	nConst++;
6290	} else if (psLevel == nsLevel + 1) {
6291	bdd = bdd_var_with_index(mddManager, nsId);
6292	bdd_new_var_block(bdd, 2);
6293	bdd_free(bdd);
6294	nConst++;
6295	}
6296	} else {
6297	bdd_set_var_to_be_ungrouped(mddManager, pairPsId);
6298	bdd_set_var_to_be_ungrouped(mddManager, nsId);
6299	}
6300	} else if (nDependPs == 1) {
6301	psLevel = bdd_get_level_from_id(mddManager, pairPsId);
6302	nsLevel = bdd_get_level_from_id(mddManager, nsId);
6303	if (psLevel == nsLevel - 1) {
6304	bdd = bdd_var_with_index(mddManager, pairPsId);
6305	bdd_new_var_block(bdd, 2);
6306	bdd_free(bdd);
6307	nDepend1to1++;
6308	} else if (psLevel == nsLevel + 1) {
6309	bdd = bdd_var_with_index(mddManager, nsId);
6310	bdd_new_var_block(bdd, 2);
6311	bdd_free(bdd);
6312	nDepend1to1++;
6313	}
6314	} else if (nonLambda[pairPsId] == 1) {
6315	psLevel = bdd_get_level_from_id(mddManager, pairPsId);
6316	nsLevel = bdd_get_level_from_id(mddManager, nsId);
6317	if (psLevel == nsLevel - 1) {
6318	bdd = bdd_var_with_index(mddManager, pairPsId);
6319	bdd_new_var_block(bdd, 2);
6320	bdd_free(bdd);
6321	nPairPsOnce++;
6322	} else if (psLevel == nsLevel + 1) {
6323	bdd = bdd_var_with_index(mddManager, nsId);
6324	bdd_new_var_block(bdd, 2);
6325	bdd_free(bdd);
6326	nPairPsOnce++;
6327	}
6328	}
6329	} else {
6330	/* bitwise transition relation does not depend on any nsvar */
6331	nUngroup++;
6332	}
6333	var_set_free(supIds);
6334	}
6335	for (i = 0; i < nVars; i++) {
6336	if (bdd_is_ps_var(mddManager, i)) {
6337	if (nonLambda[i] == 0) {
6338	/* no next state function depends on psvar i */
6339	psId = i;
6340	nsId = bdd_read_pair_index(mddManager, psId);
6341	psLevel = bdd_get_level_from_id(mddManager, psId);
6342	nsLevel = bdd_get_level_from_id(mddManager, nsId);
6343	nLambda++;
6344	if (psLevel == nsLevel - 1) {
6345	bdd = bdd_var_with_index(mddManager, psId);
6346	bdd_new_var_block(bdd, 2);
6347	bdd_free(bdd);
6348	} else if (psLevel == nsLevel + 1) {
6349	bdd = bdd_var_with_index(mddManager, nsId);
6350	bdd_new_var_block(bdd, 2);
6351	bdd_free(bdd);
6352	}
6353	}
6354	} else if (bdd_is_pi_var(mddManager, i)) {
6355	bdd_set_var_to_be_ungrouped(mddManager, i);
6356	}
6357	}
6358	if (verbosity) {
6359	fprintf(vis_stdout, "#grp=%d(#depend1to1=%d,#pairpsonce=%d)",
6360	nGroup, nDepend1to1, nPairPsOnce);
6361	fprintf(vis_stdout,
6362	" #ungrp=%d(#const=%d,#lambda=%d, independ1to1=%d)\n",
6363	nUngroup, nConst, nLambda, nIndepend1to1);
6364	}
6365	FREE(nonLambda);
6366	}
6367
6368	/Function******************************************************************
6369
6370	Synopsis [Check whether the given transition relation is optimized.]
6371
6372	Description [Check whether the given transition relation is optimized.]
6373
6374	SideEffects [ ]
6375
6376	******************************************************************************/
6377	int
6378	Img_IsTransitionRelationOptimized(Img_ImageInfo_t * imageInfo)
6379	{
6380	Iwls95Info_t info = (Iwls95Info_t )imageInfo->methodData;
6381	if(info->fwdOptClusteredRelationArray &&
6382	info->fwdClusteredRelationArray) return(1);
6383	return(0);
6384	}
6385
6386	/Function******************************************************************
6387
6388	Synopsis [Compare the size of two MDDs.]
6389
6390	Description [Compare the size of two MDDs.]
6391
6392	SideEffects [ ]
6393
6394	******************************************************************************/
6395	static int
6396	MddSizeCompare(const void ptr1, const void ptr2)
6397	{
6398	mdd_t mdd1 = (mdd_t **)ptr1;
6399	mdd_t mdd2 = (mdd_t **)ptr2;
6400	int size1 = mdd_size(mdd1);
6401	int size2 = mdd_size(mdd2);
6402
6403	if (size1 > size2)
6404	return 1;
6405	else if (size1 < size2)
6406	return -1;
6407	else
6408	return 0;
6409	}
6410
6411	/Function******************************************************************
6412
6413	Synopsis [Restore original transition relations from restricted transition relations by conjoining with winning strategy]
6414
6415	Description [Restore original transition relations from restricted transition relations by conjoining with winning strategy]
6416
6417	SideEffects []
6418
6419	SeeAlso []
6420	******************************************************************************/
6421	void
6422	Img_ForwardImageInfoRecoverFromWinningStrategy(
6423	Img_ImageInfo_t * imageInfo
6424	)
6425	{
6426	Iwls95Info_t *info;
6427	array_t *new_;
6428
6429	info = (Iwls95Info_t *)imageInfo->methodData;
6430
6431	if(info->fwdOriClusteredRelationArray) {
6432	new_ = info->fwdClusteredRelationArray;
6433	info->fwdClusteredRelationArray = info->fwdOriClusteredRelationArray;
6434	info->fwdOriClusteredRelationArray = 0;
6435	mdd_array_free(new_);
6436	}
6437	}
6438
6439	/Function******************************************************************
6440
6441	Synopsis [Create restricted transition relations by conjoining with winning strategy]
6442
6443	Description [Create restricted transition relations by conjoining with winning strategy.]
6444
6445	SideEffects []
6446
6447	SeeAlso []
6448	******************************************************************************/
6449	void
6450	Img_ForwardImageInfoConjoinWithWinningStrategy(
6451	Img_ImageInfo_t * imageInfo,
6452	mdd_t *winningStrategy)
6453	{
6454	Iwls95Info_t *info;
6455	array_t old, new_;
6456	int i;
6457	mdd_t tr, ntr, *winning;
6458
6459
6460	old = 0;
6461	winning = 0;
6462	new_ = array_alloc(mdd_t *, 0);
6463	info = (Iwls95Info_t *)imageInfo->methodData;
6464	old = info->fwdClusteredRelationArray;
6465	info->fwdClusteredRelationArray = new_;
6466	info->fwdOriClusteredRelationArray = old;
6467	winning = mdd_dup(winningStrategy);
6468	/* winning = ImgSubstitute(winningStrategy, &(imageInfo->functionData), Img_D2R_c);*/
6469	for(i=0; i<array_n(old); i++) {
6470	tr = array_fetch(mdd_t *, old, i);
6471	ntr = mdd_and(tr, winning, 1, 1);
6472	array_insert_last(mdd_t *, new_, ntr);
6473	}
6474	mdd_free(winning);
6475	}
6476

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: vis_dev/vis-2.3/src/img/imgIwls95.c @ 93

Download in other formats: