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

Last change on this file since 87 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
63static 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
77typedef struct Iwls95InfoStruct Iwls95Info_t;
78typedef struct CtrInfoStruct CtrInfo_t;
79typedef struct VarInfoStruct VarInfo_t;
80typedef struct CtrItemStruct CtrItem_t;
81typedef 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
127struct 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******************************************************************************/
187struct 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
222struct 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******************************************************************************/
244struct 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******************************************************************************/
268struct 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
285static  double  *signatures;
286
287/*---------------------------------------------------------------------------*/
288/* Macro declarations                                                        */
289/*---------------------------------------------------------------------------*/
290
291
292/**AutomaticStart*************************************************************/
293
294/*---------------------------------------------------------------------------*/
295/* Static function prototypes                                                */
296/*---------------------------------------------------------------------------*/
297
298static void ResetClusteredCofactoredRelationArray(mdd_manager *mddManager, Iwls95Info_t *info);
299static void FreeClusteredCofactoredRelationArray(Iwls95Info_t *info);
300static ImgTrmOption_t * TrmGetOptions(void);
301static void CreateBitRelationArray(Iwls95Info_t *info, ImgFunctionData_t *functionData);
302static void FreeBitRelationArray(Iwls95Info_t *info);
303static 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);
304static array_t * CreateClusters(bdd_manager *bddManager, array_t *relationArray, ImgTrmOption_t *option);
305static 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);
306static array_t * RelationArraySmoothLocalVars(array_t *relationArray, array_t *ctrInfoArray, array_t *varInfoArray, st_table *bddIdToBddTable);
307static 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);
308static array_t * UpdateInfoArrays(CtrInfo_t *ctrInfo, st_table *bddIdToBddTable, int *numSmoothVarsRemainingPtr, int *numIntroducedVarsRemainingPtr);
309static float CalculateBenefit(CtrInfo_t *ctrInfo, int maxNumLocalSmoothVars, int maxNumSmoothVars, int maxIndex, int maxNumIntroducedVars, ImgTrmOption_t *option);
310static void PrintOption(Img_MethodType method, ImgTrmOption_t *option, FILE *fp);
311static Iwls95Info_t * Iwls95InfoStructAlloc(Img_MethodType method);
312static CtrInfo_t * CtrInfoStructAlloc(void);
313static void CtrInfoStructFree(CtrInfo_t *ctrInfo);
314static VarInfo_t * VarInfoStructAlloc(void);
315static void VarInfoStructFree(VarInfo_t *varInfo);
316static void CtrItemStructFree(CtrItem_t *ctrItem);
317static void VarItemStructFree(VarItem_t *varItem);
318static int CtrInfoMaxIndexCompare(const void * p1, const void * p2);
319static void PrintCtrInfoStruct(CtrInfo_t *ctrInfo);
320static void PrintVarInfoStruct(VarInfo_t *varInfo);
321static int CheckQuantificationSchedule(array_t *relationArray, array_t *arraySmoothVarBddArray);
322static int CheckCtrInfoArray(array_t *ctrInfoArray, int numDomainVars, int numQuantifyVars, int numRangeVars);
323static int CheckCtrInfo(CtrInfo_t *ctrInfo, int numDomainVars, int numQuantifyVars, int numRangeVars);
324static int CheckVarInfoArray(array_t *varInfoArray, int numRelation);
325static array_t * BddArrayDup(array_t *bddArray);
326static array_t * BddArrayArrayDup(array_t *bddArray);
327static 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);
328static void HashIdToBddTable(st_table *table, array_t *idArray, array_t *bddArray);
329static void PrintSmoothIntroducedCount(array_t *clusterArray, array_t **arraySmoothVarBddArrayPtr, array_t *psBddIdArray, array_t *nsBddIdArray);
330static void PrintBddIdFromBddArray(array_t *bddArray);
331static void PrintBddIdTable(st_table *idTable);
332static void PartitionTraverseRecursively(mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *relationArray, st_table *domainQuantifyVarMddIdTable, array_t *quantifyVarMddIdArray);
333static void PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int indent);
334static 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);
335static bdd_t * ComputeSubsetOfIntermediateProduct(bdd_t *product, ImgPartialImageOption_t *PIoption);
336static bdd_t * ComputeClippedAndAbstract(bdd_t *product, bdd_t *relation, array_t *smoothVarBddArray, int nvars, int clippingDepth, boolean *partial, int verbosity);
337static array_t * CopyArrayBddArray(array_t *arrayBddArray);
338static void PrintPartitionedTransitionRelation(mdd_manager *mddManager, Iwls95Info_t *info, Img_DirectionType directionType);
339static void ReorderPartitionedTransitionRelation(Iwls95Info_t *info, ImgFunctionData_t *functionData, Img_DirectionType directionType);
340static void UpdateQuantificationSchedule(Iwls95Info_t *info, ImgFunctionData_t *functionData, Img_DirectionType directionType);
341static array_t * MakeSmoothVarCubeArray(mdd_manager *mddManager, array_t *arraySmoothVarBddArray);
342static mdd_t * TrmEliminateDependVars(Img_ImageInfo_t *imageInfo, array_t *relationArray, mdd_t *states, mdd_t **dependRelations);
343static int TrmSignatureCompare(int *ptrX, int *ptrY);
344static void SetupLazySifting(mdd_manager *mddManager, array_t *bddRelationArray, array_t *domainVarBddArray, array_t *quantifyVarBddArray, array_t *rangeVarBddArray, int verbosity);
345static 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******************************************************************************/
376mdd_t*
377Img_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******************************************************************************/
408void
409Img_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******************************************************************************/
433void
434Img_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******************************************************************************/
457void
458Img_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******************************************************************************/
478void
479Img_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******************************************************************************/
551mdd_t*
552ImgMultiwayLinearAndSmooth(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******************************************************************************/
601mdd_t*
602ImgMultiwayLinearAndSmoothWithFrom(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******************************************************************************/
727mdd_t*
728ImgBddLinearAndSmooth(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******************************************************************************/
760array_t *
761ImgClusterRelationArray(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******************************************************************************/
894array_t *
895ImgGetQuantificationSchedule(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******************************************************************************/
971ImgTrmOption_t *
972ImgGetTrmOptions(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******************************************************************************/
990void
991ImgFreeTrmOptions(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
1014void 
1015ImgResetMethodDataLinearComputeRange(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******************************************************************************/
1031void 
1032ImgSetMethodDataLinearComputeRange(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******************************************************************************/
1048mdd_t *
1049Img_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
1080void *
1081ImgImageInfoInitializeIwls95(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******************************************************************************/
1532mdd_t *
1533ImgImageInfoComputeFwdIwls95(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******************************************************************************/
1871mdd_t *
1872ImgImageInfoComputeFwdWithDomainVarsIwls95(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******************************************************************************/
1927mdd_t *
1928ImgImageInfoComputeBwdIwls95(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******************************************************************************/
2033mdd_t *
2034ImgImageInfoComputeBwdWithDomainVarsIwls95(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******************************************************************************/
2073void
2074ImgImageInfoFreeIwls95(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******************************************************************************/
2131void
2132ImgImageInfoPrintMethodParamsIwls95(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******************************************************************************/
2160st_table *
2161ImgBddGetSupportIdTable(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******************************************************************************/
2191boolean
2192ImgImageWasPartialIwls95(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******************************************************************************/
2213void
2214ImgImageAllowPartialImageIwls95(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******************************************************************************/
2230void
2231ImgRestoreTransitionRelationIwls95(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******************************************************************************/
2288void
2289ImgDuplicateTransitionRelationIwls95(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******************************************************************************/
2355void
2356ImgMinimizeTransitionRelationIwls95(
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******************************************************************************/
2425void
2426ImgAbstractTransitionRelationIwls95(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******************************************************************************/
2510int
2511ImgApproximateTransitionRelationIwls95(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******************************************************************************/
2591array_t *
2592ImgGetTransitionRelationIwls95(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******************************************************************************/
2614void
2615ImgUpdateTransitionRelationIwls95(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******************************************************************************/
2636void
2637ImgReplaceIthPartitionedTransitionRelationIwls95(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******************************************************************************/
2663void
2664ImgImageFreeClusteredTransitionRelationIwls95(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******************************************************************************/
2728void
2729ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(
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******************************************************************************/
2883void
2884ImgPrintIntegerArray(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******************************************************************************/
2905void
2906ImgPrintPartition(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******************************************************************************/
2930void
2931ImgPrintPartitionedTransitionRelation(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******************************************************************************/
2995mdd_t *
2996ImgTrmEliminateDependVars(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******************************************************************************/
3121static void
3122ResetClusteredCofactoredRelationArray(
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******************************************************************************/
3155static void
3156FreeClusteredCofactoredRelationArray(
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
3185static ImgTrmOption_t *
3186TrmGetOptions(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
3572static void
3573CreateBitRelationArray(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******************************************************************************/
3653static void
3654FreeBitRelationArray (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******************************************************************************/
3691static void
3692OrderClusterOrder(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
3750static array_t *
3751CreateClusters(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******************************************************************************/
3814static void
3815OrderRelationArray(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
4087static array_t *
4088RelationArraySmoothLocalVars(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******************************************************************************/
4211static void
4212OrderRelationArrayAux(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******************************************************************************/
4425static array_t *
4426UpdateInfoArrays(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******************************************************************************/
4544static float
4545CalculateBenefit(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******************************************************************************/
4588static void
4589PrintOption(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******************************************************************************/
4626static Iwls95Info_t *
4627Iwls95InfoStructAlloc(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******************************************************************************/
4647static CtrInfo_t *
4648CtrInfoStructAlloc(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******************************************************************************/
4672static void
4673CtrInfoStructFree(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******************************************************************************/
4688static VarInfo_t *
4689VarInfoStructAlloc(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******************************************************************************/
4709static void
4710VarInfoStructFree(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******************************************************************************/
4725static void
4726CtrItemStructFree(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******************************************************************************/
4740static void
4741VarItemStructFree(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******************************************************************************/
4757static int
4758CtrInfoMaxIndexCompare(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******************************************************************************/
4779static void
4780PrintCtrInfoStruct(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******************************************************************************/
4805static void
4806PrintVarInfoStruct(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******************************************************************************/
4840static int
4841CheckQuantificationSchedule(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******************************************************************************/
4908static int
4909CheckCtrInfoArray(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******************************************************************************/
4929static int
4930CheckCtrInfo(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******************************************************************************/
4952static int
4953CheckVarInfoArray(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******************************************************************************/
4980static array_t *
4981BddArrayDup(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
4993static array_t *
4994BddArrayArrayDup(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******************************************************************************/
5032static mdd_t *
5033BddLinearAndSmooth(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
5246static void
5247HashIdToBddTable(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******************************************************************************/
5274static void
5275PrintSmoothIntroducedCount(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******************************************************************************/
5348static void
5349PrintBddIdFromBddArray(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******************************************************************************/
5373static void
5374PrintBddIdTable(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******************************************************************************/
5399static void
5400PartitionTraverseRecursively(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******************************************************************************/
5452static void
5453PrintPartitionRecursively(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******************************************************************************/
5492static bdd_t *
5493RecomputeImageIfNecessary(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******************************************************************************/
5617static bdd_t *
5618ComputeSubsetOfIntermediateProduct(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******************************************************************************/
5693static bdd_t *
5694ComputeClippedAndAbstract(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******************************************************************************/
5743static array_t *
5744CopyArrayBddArray(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******************************************************************************/
5774static void
5775PrintPartitionedTransitionRelation(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******************************************************************************/
5806static void
5807ReorderPartitionedTransitionRelation(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******************************************************************************/
5949static void
5950UpdateQuantificationSchedule(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******************************************************************************/
6095static array_t *
6096MakeSmoothVarCubeArray(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******************************************************************************/
6129static mdd_t *
6130TrmEliminateDependVars(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******************************************************************************/
6163static int
6164TrmSignatureCompare(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******************************************************************************/
6183static void
6184SetupLazySifting(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******************************************************************************/
6377int
6378Img_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******************************************************************************/
6395static int
6396MddSizeCompare(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******************************************************************************/
6421void
6422Img_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******************************************************************************/
6449void
6450Img_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.