source: vis_dev/vis-2.3/src/img/imgLinear.c @ 23

Last change on this file since 23 was 14, checked in by cecile, 13 years ago

vis2.3

File size: 138.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [imgLinear.c]
4
5  PackageName [img]
6
7  Synopsis    [Routines for image computation using Linear Arrangement
8   published in TACAS02.]
9
10  Description []
11
12  SeeAlso     []
13
14  Author      [HoonSang Jin]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35******************************************************************************/
36#include "imgInt.h"
37#include "fsm.h"
38#include "heap.h"
39
40static char rcsid[] UNUSED = "$Id: imgLinear.c,v 1.18 2010/04/10 00:37:06 fabio Exp $";
41static char linearVarString[] = "TCNI";
42
43
44/*---------------------------------------------------------------------------*/
45/* Constant declarations                                                     */
46/*---------------------------------------------------------------------------*/
47
48/*---------------------------------------------------------------------------*/
49/* Type declarations                                                         */
50/*---------------------------------------------------------------------------*/
51
52
53/*---------------------------------------------------------------------------*/
54/* Structure declarations                                                    */
55/*---------------------------------------------------------------------------*/
56
57
58/*---------------------------------------------------------------------------*/
59/* Variable declarations                                                     */
60/*---------------------------------------------------------------------------*/
61
62Cluster_t *__clu;
63
64/*---------------------------------------------------------------------------*/
65/* Macro declarations                                                        */
66/*---------------------------------------------------------------------------*/
67
68#define BACKWARD_REDUCTION_RATE 0.5
69#define FORWARD_REDUCTION_RATE 0.5
70
71/**AutomaticStart*************************************************************/
72
73/*---------------------------------------------------------------------------*/
74/* Static function prototypes                                                */
75/*---------------------------------------------------------------------------*/
76
77static void ImgLinearUpdateVariableArrayWithId(Relation_t *head, int cindex, int id);
78static int ImgLinearQuantifyVariablesFromConjunct(Relation_t *head, Conjunct_t *conjunct, array_t *smoothVarBddArray, int *bModified);
79static void ImgLinearConjunctRefine(Relation_t *head, Conjunct_t *conjunct);
80static void ImgLinearVariableArrayQuit(Relation_t *head);
81static void ImgLinearConjunctQuit(Conjunct_t *conjunct);
82static Conjunct_t ** ImgLinearAddConjunctIntoArray(Conjunct_t **array, int *nArray, Conjunct_t *con);
83static void ImgLinearFindSameSupportConjuncts(Relation_t *head, int from, int to);
84static void ImgLinearClusterSameSupportSet(Relation_t *head);
85static void ImgLinearExpandSameSupportSet(Relation_t *head);
86static int ImgLinearIsSameConjunct(Relation_t *head, Conjunct_t *con1, Conjunct_t *con2);
87static bdd_t * ImgLinearClusteringSmooth(Relation_t *head, Cluster_t *clu, int **failureHistory, int andExistLimit, int bddLimit);
88static int ImgLinearClusterUsingHeap(Relation_t *head, double affinityLimit, int andExistLimit, int varLimit, Img_OptimizeType optDir, int rangeFlag, int (*compare_func)(const void *, const void *));
89static void ImgLinearPrintTransitionInfo(Relation_t *head);
90static void ImgLinearComputeLifeTime(Relation_t *head, double *paal, double *patl);
91static void ImgLinearFreeSmoothArray(array_t *smoothVarBddArray);
92static void ImgLinearPrintMatrixFull(Relation_t *head, int matrixIndex);
93static void ImgLinearPrintMatrix(Relation_t *head);
94static void ImgLinearCAPOReadVariableOrder(Relation_t *head, char *baseName, int includeNS);
95static void ImgLinearCAPOInterfaceVariablePl(Relation_t *head, char *baseName, int includeNS);
96static void ImgLinearCAPOInterfaceVariableScl(Relation_t *head, char *baseName);
97static void ImgLinearCAPOInterfaceVariableNet(Relation_t *head, char *baseName, int includeNS);
98static void ImgLinearCAPOInterfaceVariableNodes(Relation_t *head, char *baseName, int includeNS);
99static void ImgLinearVariableOrder(Relation_t *head, char *baseName, int includeNS);
100static void ImgLinearCAPOReadConjunctOrder(Relation_t *head, char *baseName);
101static int ImgLinearCAPORun(char *capoExe, char *baseName, int brief);
102static void ImgLinearCAPOInterfaceAux(Relation_t *head, char *baseName);
103static void ImgLinearCAPOInterfaceConjunctPl(Relation_t *head, char *baseName);
104static void ImgLinearCAPOInterfaceConjunctScl(Relation_t *head, char *baseName);
105static void ImgLinearCAPOInterfaceConjunctNet(Relation_t *head, char *baseName);
106static void ImgLinearCAPOInterfaceConjunctNodes(Relation_t *head, char *baseName);
107static void ImgLinearConjunctionOrder(Relation_t *head, char *baseName, int refineFlag);
108static void ImgLinearConjunctOrderMain(Relation_t *head, int bRefineConjunctOrder);
109static void ImgLinearPrintDebugInfo(Relation_t *head);
110static void ImgLinearPrintVariableProfile(Relation_t *head, char *baseName);
111static void ImgLinearInsertClusterCandidate(Relation_t *head, int from, int to, int nDead, int nVar, double affinityLimit);
112static void ImgLinearInsertPairClusterCandidate(Relation_t *head, int from, double affinityLimit, int varLimit, int rangeFlag);
113static void ImgLinearBuildInitialCandidate(Relation_t *head, double affinityLimit, int varLimit, int rangeFlag, int (*compare_func)(const void *, const void *));
114static bdd_t * ImgLinearClusteringPairSmooth(Relation_t *head, Cluster_t *clu, int **failureHistory, int andExistLimit, int bddLimit);
115static void ImgLinearVariableArrayInit(Relation_t *head);
116static void ImgLinearSetEffectiveNumberOfStateVariable(Relation_t *head, int *rangeId, int *domainId, int *existStateVariable) ;
117static void ImgLinearVariableLifeQuit(VarLife_t *var);
118static void ImgLinearAddNextStateCase(Relation_t *head);
119static void ImgLinearAddSingletonCase(Relation_t *head);
120
121static int ImgLinearCompareDeadAffinityLive(const void *c1, const void *c2);
122static int ImgLinearCompareDeadLiveAffinity(const void *c1, const void *c2);
123static int ImgLinearCompareAffinityDeadLive(const void *c1, const void *c2);
124static int ImgLinearCompareLiveAffinityDead(const void *c1, const void *c2);
125static int ImgLinearHeapCompareDeadAffinityLive(const void *c1, const void *c2);
126static int ImgLinearHeapCompareDeadLiveAffinity(const void *c1, const void *c2);
127static int ImgLinearHeapCompareAffinityDeadLive(const void *c1, const void *c2);
128static int ImgLinearHeapCompareLiveAffinityDead(const void *c1, const void *c2);
129
130static int ImgLinearCompareVarIndex(const void *c1, const void *c2);
131static int ImgLinearCompareVarSize(const void *c1, const void *c2);
132static int ImgLinearCompareVarEffFromSmall(const void *c1, const void *c2);
133static int ImgLinearCompareVarEffFromLarge(const void *c1, const void *c2);
134static int ImgLinearCompareConjunctDummy(const void *c1, const void *c2);
135static int ImgLinearCompareConjunctIndex(const void *c1, const void *c2);
136static int ImgLinearCompareConjunctSize(const void *c1, const void *c2);
137static int ImgLinearCompareConjunctRangeMinusDomain(const void *c1, const void *c2);
138static int ImgLinearCompareVarId(const void *c1, const void *c2);
139static int ImgCheckRangeTestAndOverapproximate(Relation_t *head);
140static void ImgCountOnsetDisjunctiveArray(Relation_t *head);
141static int linearCheckRange(const void *tc);
142
143static void ImgLinearConjunctArrayRefine(Relation_t *head);
144/**AutomaticEnd***************************************************************/
145
146
147/*---------------------------------------------------------------------------*/
148/* Definition of exported functions                                          */
149/*---------------------------------------------------------------------------*/
150void ImgLinearConjunctOrderMainCC(Relation_t *head, int refineFlag);
151int ImgLinearClustering(Relation_t *head, Img_OptimizeType optDir);
152int ImgLinearPropagateConstant(Relation_t *head, int nextStateFlag);
153int ImgLinearOptimizeStateVariables(Relation_t *head, Img_OptimizeType optDir);
154void ImgLinearExtractNextStateCase(Relation_t *head);
155void ImgLinearExtractSingletonCase(Relation_t *head);
156/*void ImgLinearClusterRelationArray(mdd_manager *mgr, ImgFunctionData_t *functionData, array_t *relationArray, Img_DirectionType direction, array_t **clusteredRelationArrayPtr, array_t **arraySmoothVarBddArrayPtr, array_t **optClusteredRelationArrayPtr, array_t **optArraySmoothVarBddArrayPtr, ImgTrmOption_t *option);
157*/
158void ImgLinearConnectedComponent(Relation_t *head);
159void ImgLinearBuildConjunctArrayWithQuotientCC(Relation_t *head);
160void ImgLinearFindConnectedComponent(Relation_t *head, Conjunct_t *conjunct, int cc_index);
161void ImgLinearAddConjunctIntoClusterArray(Conjunct_t *base, Conjunct_t *con);
162
163
164/**Function********************************************************************
165
166  Synopsis    [Cluster fine grain transition relation]
167
168  Description [First the linear arrangement of transition relation that minimze max cut is generated and the iterative clustering is applied on it.]
169
170  SideEffects []
171
172  SeeAlso     []
173
174******************************************************************************/
175void
176ImgLinearClusterRelationArray(mdd_manager *mgr, 
177                             ImgFunctionData_t *functionData, 
178                             array_t *relationArray, 
179                             Img_DirectionType direction, 
180                             array_t **clusteredRelationArrayPtr, 
181                             array_t **arraySmoothVarBddArrayPtr, 
182                             array_t **optClusteredRelationArrayPtr, 
183                             array_t **optArraySmoothVarBddArrayPtr, 
184                             ImgTrmOption_t *option)
185{
186Img_OptimizeType optDir;
187int bGroupStateVariable;
188int bOrderVariable;
189
190int includeCS;
191int includeNS;
192int quantifyCS;
193array_t *initRelationArray;
194int bOptimize;
195Relation_t *head;
196bdd_t **smoothCubeArr, **optSmoothCubeArr;
197array_t *optRelationArr, *optSmoothVarBddArr;
198array_t *relationArr, *smoothVarBddArr;
199
200  if(option->linearComputeRange) {
201    option->linearIncludeCS = 0;
202    option->linearIncludeNS = 0;
203    option->linearQuantifyCS = 1;
204  }
205 
206  optRelationArr = relationArr = 0;
207  optSmoothVarBddArr = smoothVarBddArr = 0;
208
209  includeCS = option->linearIncludeCS;
210  includeNS = option->linearIncludeNS;
211  quantifyCS = option->linearQuantifyCS;
212  if(option->linearFineGrainFlag)       includeNS = 1;
213  optDir = option->linearOptimize;
214  bOrderVariable = option->linearOrderVariable;
215  bGroupStateVariable = option->linearGroupStateVariable;
216
217  head = ImgLinearRelationInit(mgr, relationArray, 
218          functionData->domainBddVars, functionData->rangeBddVars, 
219          functionData->quantifyBddVars, option);
220
221  if(head->verbosity >= 5) ImgLinearPrintDebugInfo(head);
222
223  ImgLinearOptimizeAll(head, Opt_None, 0);
224  ImgLinearRefineRelation(head);
225  initRelationArray = ImgLinearExtractRelationArrayT(head);
226
227  bOptimize = 0;
228
229  ImgLinearPrintMatrix(head);
230
231  if(bOrderVariable)
232    ImgLinearVariableOrder(head, "VarOrder", !bGroupStateVariable);
233
234  if((direction==0) || (direction==2))  {
235    ImgLinearPrintMatrix(head);
236
237    bOptimize |= ImgLinearOptimizeAll(head, optDir, 0);
238    ImgLinearRefineRelation(head);
239    ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
240
241    ImgLinearConjunctOrderMainCC(head, 0);
242
243    ImgLinearPrintMatrix(head);
244
245    bOptimize |= ImgLinearClustering(head, optDir);
246
247    ImgLinearRefineRelation(head);
248    ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
249    ImgLinearPrintTransitionInfo(head);
250
251    ImgLinearPrintMatrix(head);
252
253    ImgLinearPrintMatrixFull(head, 2);
254
255    if(bOptimize) {
256      optRelationArr = ImgLinearExtractRelationArrayT(head);
257      optSmoothCubeArr = ALLOC(bdd_t *, head->nSize+1);
258      optSmoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, optSmoothCubeArr);
259    }
260    else {
261      optRelationArr = ImgLinearExtractRelationArrayT(head);
262      optSmoothCubeArr = ALLOC(bdd_t *, head->nSize+1);
263      optSmoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, optSmoothCubeArr);
264      relationArr = 0;
265      smoothVarBddArr = 0;
266    }
267    ImgLinearPrintDebugInfo(head);
268    ImgLinearRelationQuit(head);
269
270    if(bOptimize) {
271      fprintf(vis_stdout, "Get Schedules without optimization\n");
272      head = ImgLinearRelationInit(mgr, initRelationArray, 
273          functionData->domainBddVars, functionData->rangeBddVars, 
274          functionData->quantifyBddVars, option);
275      ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
276      ImgLinearConjunctOrderMainCC(head, 0);
277      if(head->verbosity >= 5)
278        ImgLinearPrintMatrix(head);
279      ImgLinearClustering(head, Opt_None);
280       
281      relationArr = ImgLinearExtractRelationArrayT(head);
282      smoothCubeArr = ALLOC(bdd_t *, head->nSize+1);
283      smoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, smoothCubeArr);
284
285      ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
286      ImgLinearPrintDebugInfo(head);
287      ImgLinearPrintTransitionInfo(head);
288
289      ImgLinearRelationQuit(head);
290    }
291
292    if(optClusteredRelationArrayPtr)
293      *optClusteredRelationArrayPtr = optRelationArr;
294    else
295      mdd_array_free(optRelationArr);
296
297    if(optArraySmoothVarBddArrayPtr)
298      *optArraySmoothVarBddArrayPtr = optSmoothVarBddArr;
299    else if(optSmoothVarBddArr)
300      ImgLinearFreeSmoothArray(optSmoothVarBddArr);
301
302    if(clusteredRelationArrayPtr)
303      *clusteredRelationArrayPtr = relationArr;
304    else
305      mdd_array_free(relationArr);
306
307    if(arraySmoothVarBddArrayPtr)
308      *arraySmoothVarBddArrayPtr = smoothVarBddArr;
309    else if(smoothVarBddArr)
310      ImgLinearFreeSmoothArray(smoothVarBddArr);
311  }
312
313  if((direction==1) || (direction==2)) {
314  }
315}
316
317
318/**Function********************************************************************
319
320  Synopsis    [Initialize the data structure for linear arrangement and clustering.]
321
322  Description [Build initial data structure]
323
324  SideEffects []
325
326  SeeAlso     []
327
328******************************************************************************/
329Relation_t *
330ImgLinearRelationInit(mdd_manager *mgr,
331                        array_t *relationArray,
332                        array_t *domainBddVars,
333                        array_t *rangeBddVars,
334                        array_t *quantifyBddVars,
335                        ImgTrmOption_t *option)
336{
337Relation_t *head;
338Conjunct_t *conjunct, **conjunctArray;
339bdd_t *varBdd;
340int *domain2range, *range2domain;
341int *varArrayMap, *varType;
342bdd_t **constantCase, *relation;
343int i, j, id, tid, nSize;
344int *supList, listSize;
345char *flagValue;
346int *quantifyVars, nQuantify, *visited;
347
348  head = ALLOC(Relation_t, 1);
349  memset(head, 0, sizeof(Relation_t));
350  head->mgr = mgr;
351  head->nVar = bdd_num_vars(head->mgr);
352  head->bddLimit = option->clusterSize;
353
354  head->verbosity = option->verbosity;
355  flagValue = Cmd_FlagReadByName("linear_verbosity");
356  if(flagValue) {
357    head->verbosity += atoi(flagValue);
358  }
359
360
361  head->includeCS = option->linearIncludeCS;
362  head->includeNS = option->linearIncludeNS;
363  head->quantifyCS = option->linearQuantifyCS;
364  head->computeRange = option->linearComputeRange;
365
366  head->nInitRange = 0;
367  head->nInitDomain = 0;
368  head->nInitQuantify = 0;
369  head->nEffRange = 0;
370  head->nEffDomain = 0;
371  head->nEffQuantify = 0;
372
373  head->clusterArray = 0;
374  head->nClusterArray = 0;
375
376  head->nVarArray = 0;
377  head->varArray = 0;
378
379  head->nSingletonArray = 0;
380  head->singletonArray = 0;
381  head->nNextStateArray = 0;
382  head->nextStateArray = 0;
383
384  domain2range = ALLOC(int, head->nVar);
385  head->domain2range = domain2range;
386  memset(domain2range, -1, sizeof(int)*head->nVar);
387
388  range2domain = ALLOC(int, head->nVar);
389  head->range2domain = range2domain;
390  memset(range2domain, -1, sizeof(int)*head->nVar);
391
392  varType = ALLOC(int, head->nVar);
393  head->varType = varType;
394  memset(varType, 0, sizeof(int)*head->nVar);
395
396  head->nRange = array_n(rangeBddVars);
397  head->nDomain = array_n(domainBddVars);
398
399  head->domainVars = ALLOC(int, head->nDomain);
400  head->rangeVars = ALLOC(int, head->nRange);
401  for(i=0; i<head->nDomain; i++) {
402    varBdd = array_fetch(bdd_t *, domainBddVars, i);
403    id = (int)bdd_top_var_id(varBdd);
404    head->domainVars[i] = id;
405    varType[id] = 1;
406
407    varBdd = array_fetch(bdd_t *, rangeBddVars, i);
408    tid = (int)bdd_top_var_id(varBdd);
409    head->rangeVars[i] = tid;
410    varType[tid] = 2;
411
412    domain2range[id] = tid;
413    range2domain[tid] = id;
414  }
415
416  head->quantifyVars = quantifyVars = ALLOC(int, head->nVar);
417  memset(quantifyVars, 0, sizeof(int)*head->nVar);
418  for(nQuantify=0, i=0; i<array_n(quantifyBddVars); i++) {
419    varBdd = array_fetch(bdd_t *, quantifyBddVars, i);
420    id = (int)bdd_top_var_id(varBdd);
421    quantifyVars[nQuantify++] = id;
422    varType[id] = 3;
423  }
424
425  varArrayMap = ALLOC(int, head->nVar);
426  head->varArrayMap = varArrayMap;
427  memset(varArrayMap, -1, sizeof(int)*head->nVar);
428
429  constantCase = ALLOC(bdd_t *, head->nVar);
430  head->constantCase = constantCase;
431  memset(constantCase, 0, sizeof(bdd_t *)*head->nVar);
432
433
434  nSize = array_n(relationArray);
435  conjunctArray = ALLOC(Conjunct_t *, nSize+1);
436  head->nSize = nSize;
437  head->conjunctArray = conjunctArray;
438
439  visited = ALLOC(int, head->nVar);
440  memset(visited, 0, sizeof(int)*head->nVar);
441  for(i=0; i<nSize; i++) {
442    conjunct = ALLOC(Conjunct_t, 1);
443    memset(conjunct, 0, sizeof(Conjunct_t));
444    conjunct->index = i;
445    relation = array_fetch(bdd_t *, relationArray, i);
446
447    conjunct->relation = mdd_dup(relation);
448
449    supList = ImgLinearGetSupportBddId(head->mgr, relation, &listSize);
450    conjunct->supList = supList;
451    conjunct->nSize = listSize;
452    for(j=0; j<listSize; j++) {
453      id = supList[j];
454      if(varType[id] == 1)      conjunct->nDomain++;
455      else if(varType[id] == 2) conjunct->nRange++;
456      else if(varType[id] == 3) conjunct->nQuantify++;
457      else if(visited[id] == 0) {
458        quantifyVars[nQuantify++] = id;
459        visited[id] = 1;
460      }
461    }
462
463    conjunctArray[i] = conjunct;
464  }
465  conjunctArray[i] = 0;
466
467  head->nQuantify= nQuantify;
468  free(visited);
469
470  ImgLinearVariableArrayInit(head);
471  return(head);
472}
473
474
475/**Function********************************************************************
476
477  Synopsis    [Find support varaibles of bdd]
478
479  Description [Find support varaibles of bdd]
480
481  SideEffects []
482
483  SeeAlso     []
484
485******************************************************************************/
486int *
487ImgLinearGetSupportBddId(mdd_manager *mgr, bdd_t *f, int *nSize)
488{
489var_set_t *vset;
490array_t *bvar_list;
491int *supList, i, size;
492
493  bvar_list = mdd_ret_bvar_list(mgr);
494  vset = bdd_get_support(f);
495  size = 0;
496  supList = ALLOC(int, size+1);
497  supList[0] = -1;
498  for(i=0; i<array_n(bvar_list); i++) {
499    if(var_set_get_elt(vset, i) == 1) {
500      supList = REALLOC(int, supList, size+2); 
501      supList[size++] = i;
502      supList[size] = -1;
503    }
504  }
505  var_set_free(vset);
506  *nSize = size;
507  if(size == 0) {
508    free(supList);
509    supList = 0;
510  }
511  return(supList);
512}
513
514/**Function********************************************************************
515
516  Synopsis    [Create relation array for image computation from Relation_t data structure]
517
518  Description [Create relation array for image computation from Relation_t data structure]
519
520  SideEffects []
521
522  SeeAlso     []
523
524******************************************************************************/
525bdd_t **
526ImgLinearExtractRelationArray(Relation_t *head)
527{
528int i;
529bdd_t **relationArray;
530Conjunct_t *conjunct;
531
532  relationArray = ALLOC(bdd_t *, head->nSize+1);
533  for(i=0; i<head->nSize; i++) {
534    conjunct = head->conjunctArray[i];
535    relationArray[i] = bdd_dup(conjunct->relation);
536  }
537  relationArray[i] = 0;
538  return(relationArray);
539}
540/**Function********************************************************************
541
542  Synopsis    [Create relation array for image computation from Relation_t data structure]
543
544  Description [Create relation array for image computation from Relation_t data structure]
545
546  SideEffects []
547
548  SeeAlso     []
549
550******************************************************************************/
551array_t *
552ImgLinearExtractRelationArrayT(Relation_t *head)
553{
554int i;
555array_t *relationArray;
556Conjunct_t *conjunct;
557
558  relationArray = array_alloc(bdd_t *, head->nSize);
559  for(i=0; i<head->nSize; i++) {
560    conjunct = head->conjunctArray[i];
561    array_insert_last(bdd_t *, relationArray, bdd_dup(conjunct->relation));
562  }
563  return(relationArray);
564}
565
566
567/**Function********************************************************************
568
569  Synopsis    [Function for optimizing state varaibles]
570
571  Description [If the next or current state variables are eleminated after
572  applying clustering and constant propagation then delete corresponding
573  state variable from transition relation.]
574
575  SideEffects []
576
577  SeeAlso     []
578
579******************************************************************************/
580int
581ImgLinearOptimizeAll(Relation_t *head, Img_OptimizeType optDir, int constantNSOpt)
582{
583int bOptimize;
584
585  bOptimize = 0;
586  bOptimize |= ImgLinearPropagateConstant(head, constantNSOpt);
587  bOptimize |= ImgLinearOptimizeStateVariables(head, optDir);
588  ImgLinearOptimizeInternalVariables(head);
589  return(bOptimize);
590}
591/**Function********************************************************************
592
593  Synopsis    [Propagate the constant to simply the transition relation]
594
595  Description [Propagate the constant to simply the transition relation]
596
597  SideEffects []
598
599  SeeAlso     []
600
601******************************************************************************/
602int
603ImgLinearPropagateConstant(Relation_t *head, int nextStateFlag)
604{
605int nSize, i, j;
606int *supList;
607Conjunct_t **conjunctArray;
608Conjunct_t *conjunct;
609mdd_manager *mgr;
610bdd_t **constantCase;
611bdd_t *relation, *simpleRelation;
612int nConstantCase;
613int bOptimize;
614int id, cid, index;
615int *varType;
616int size;
617
618  bOptimize = 0;
619  mgr = head->mgr;
620  constantCase = head->constantCase;
621  varType = head->varType;
622
623  conjunctArray = head->conjunctArray;
624  nSize = head->nSize;
625  nConstantCase = 0;
626  for(index=0, i=0; i<nSize; i++) {
627    conjunct = conjunctArray[i];
628    if(conjunct == 0)   continue;
629    if(conjunct->relation == 0) continue;
630   
631    if(conjunct->nSize == 1) {
632      id = conjunct->supList[0];
633      if(varType[id] == 2) {
634        if(nextStateFlag) {
635          cid = head->range2domain[id]; 
636          if(constantCase[cid] == 0) {
637            constantCase[cid] = bdd_dup(conjunct->relation);
638            if(head->verbosity >= 4)
639              fprintf(vis_stdout, "Detect Constant Case %3d(%c)\n", cid, linearVarString[varType[cid]]);
640            nConstantCase++;
641          }
642        }
643        continue;
644      }
645      else {
646        if(constantCase[id] == 0) {
647          constantCase[id] = bdd_dup(conjunct->relation);
648          if(head->verbosity >= 4)
649            fprintf(vis_stdout, "Detect Constant Case %3d(%c)\n", id, linearVarString[varType[id]]);
650          nConstantCase++;
651        }
652        continue;
653      }
654    }
655  }
656
657  if(nConstantCase > 0) {
658    for(i=0; i<head->nSize; i++) {
659      conjunct = conjunctArray[i]; 
660      if(conjunct == 0) continue;
661      if(conjunct->relation == 0)       continue;
662      relation = conjunct->relation;
663      size = conjunct->nSize;
664      supList = conjunct->supList;
665
666      for(j=0; j<size; j++) {
667        id = supList[j];
668        if(constantCase[id] == 0)       continue;
669
670        simpleRelation = bdd_cofactor(relation, constantCase[id]); 
671        if(bdd_equal(relation, simpleRelation)) {
672          bdd_free(simpleRelation);
673          continue;
674        }
675        if(varType[id] == 1) bOptimize++;
676        bdd_free(conjunct->relation);
677        conjunct->relation = simpleRelation;
678        relation = conjunct->relation;
679        conjunct->bModified = 1;
680        head->bModified = 1;
681        head->bRefineVarArray = 1;
682
683
684        if(head->verbosity >= 2)
685          fprintf(vis_stdout, "Constant propagation is applied %3d(%c) to %3d'th relation\n", id, linearVarString[varType[id]],  i);
686      }
687      ImgLinearConjunctRefine(head, conjunct);
688    }
689  }
690
691  return(bOptimize);
692}
693
694/**Function********************************************************************
695
696  Synopsis    [Remove corresponding current (next) state variables if the next (current state variables are eleminated aftetr clustering]
697
698  Description [Remove corresponding current (next) state variables if the next (current state variables are eleminated aftetr clustering]
699
700  SideEffects []
701
702  SeeAlso     []
703
704******************************************************************************/
705int
706ImgLinearOptimizeStateVariables(Relation_t *head, Img_OptimizeType optDir)
707{
708int *rangeId, *domainId, *existStateVar;
709int *domain2range;
710int *range2domain;
711bdd_t *oneBdd, *varBdd;
712VarLife_t **varArray, *var;
713array_t *smoothVarBddArray;
714Conjunct_t *conjunct;
715int i, id;
716int bOptimize;
717int rangeBound, domainBound;
718int nRangeReduced, nDomainReduced;
719
720  if(optDir == Opt_None)        return(0);
721
722  id = 0;
723  ImgLinearVariableArrayInit(head);
724
725  bOptimize = 0;
726  rangeId = ALLOC(int, head->nRange+1);
727  memset(rangeId, 0, sizeof(int)*(head->nRange+1));
728  domainId = ALLOC(int, head->nDomain+1);
729  memset(domainId, 0, sizeof(int)*(head->nDomain+1));
730  existStateVar = ALLOC(int, head->nVar);
731  memset(existStateVar, 0, sizeof(int)*head->nVar);
732  ImgLinearSetEffectiveNumberOfStateVariable(head, rangeId, domainId, existStateVar);
733
734  rangeBound = (int)((double)head->nInitRange * BACKWARD_REDUCTION_RATE);
735  domainBound = (int)((double)head->nInitDomain * FORWARD_REDUCTION_RATE);
736  if(head->nEffDomain < domainBound) {
737    if(optDir == Opt_Both)      optDir = Opt_NS;
738    else if(optDir == Opt_CS)   optDir = Opt_None;
739  }
740  if(head->nEffRange < rangeBound) {
741    if(optDir == Opt_Both)      optDir = Opt_CS;
742    else if(optDir == Opt_NS)   optDir = Opt_None;
743  }
744  if(optDir == Opt_None)        return(0);
745
746  oneBdd = bdd_one(head->mgr);
747  domain2range = head->domain2range;
748  range2domain = head->range2domain;
749  varArray = head->varArray;
750
751  if(optDir == Opt_Both || optDir == Opt_CS) {
752    smoothVarBddArray = array_alloc(bdd_t *, 0);
753    nDomainReduced = 0;
754    for(i=0; i<head->nEffDomain; i++) {
755      id = domainId[i];
756      if(existStateVar[domain2range[id]])       continue;
757
758      var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0;
759      if(var) {
760        if(head->nEffDomain-nDomainReduced < domainBound)       break;
761        if(var->nSize-head->includeCS == 1) {
762          varBdd = bdd_get_variable(head->mgr, id);
763          array_insert_last(bdd_t *, smoothVarBddArray, varBdd);
764          nDomainReduced++;
765        }           
766      } 
767    }
768
769    if(array_n(smoothVarBddArray)) {
770      for(i=0; i<head->nSize; i++) {
771        conjunct = head->conjunctArray[i];
772        if(conjunct->nDomain == 0)      continue;
773        if(ImgLinearQuantifyVariablesFromConjunct(
774                      head, conjunct, smoothVarBddArray, &bOptimize)) {
775          fprintf(vis_stdout, "NOTICE : CS %3d quantified from %d'th relation\n", id, i);
776        }
777      }
778    }
779    mdd_array_free(smoothVarBddArray);
780  }
781
782  if(optDir == Opt_Both || optDir == Opt_NS) {
783    smoothVarBddArray = array_alloc(bdd_t *, 0);
784    nRangeReduced = 0;
785    for(i=0; i<head->nEffRange; i++) {
786      id = rangeId[i];
787      if(existStateVar[range2domain[id]])       continue;
788
789      var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] :
7900;
791      if(var) {
792        if(head->nEffRange-nRangeReduced < rangeBound)  break;
793        if(var->nSize-head->includeNS == 1) {
794          varBdd = bdd_get_variable(head->mgr, id);
795          array_insert_last(bdd_t *, smoothVarBddArray, varBdd);
796          nRangeReduced++;
797        }           
798      } 
799    }
800
801    if(array_n(smoothVarBddArray)) {
802      for(i=0; i<head->nSize; i++) {
803        conjunct = head->conjunctArray[i];
804        if(conjunct->nRange == 0)       continue;
805        if(ImgLinearQuantifyVariablesFromConjunct(
806                  head, conjunct, smoothVarBddArray, &bOptimize)) {
807          fprintf(vis_stdout, "NOTICE : NS %3d quantified from %d'th relation\n", id, i);
808        }
809      }
810    }
811    mdd_array_free(smoothVarBddArray);
812  }
813
814  bdd_free(oneBdd);
815  free(rangeId);
816  free(domainId);
817  free(existStateVar);
818
819  ImgLinearVariableArrayInit(head);
820
821  return(bOptimize);
822}
823
824/**Function********************************************************************
825
826  Synopsis    [Remove intermediate variables after propagating constant.]
827
828  Description [Remove intermediate variables after propagating constant.]
829
830  SideEffects []
831
832  SeeAlso     []
833
834******************************************************************************/
835void
836ImgLinearOptimizeInternalVariables(Relation_t *head)
837{
838bdd_t *oneBdd, *varBdd;
839VarLife_t **varArray, *var;
840Conjunct_t **conjunctArray;
841array_t *smoothVarBddArray;
842int *varType;
843int i, bModified;
844
845  oneBdd = bdd_one(head->mgr);
846  while(1) {
847    bModified = 0;
848    varArray = head->varArray;
849    varType = head->varType;
850    conjunctArray = head->conjunctArray;
851    for(i=0; i<head->nVarArray; i++) {
852      var = head->varArray[i];
853      if(varType[var->id] == 2)
854        continue;
855      if(varType[var->id] == 1 && head->quantifyCS == 0)
856        continue;
857      if(var->from == var->to) {
858        if(conjunctArray[var->from] == 0)       continue;
859        varBdd = bdd_get_variable(head->mgr, var->id);
860        smoothVarBddArray = array_alloc(bdd_t *, 0);
861        array_insert_last(bdd_t *, smoothVarBddArray, varBdd);
862        ImgLinearQuantifyVariablesFromConjunct(
863                head, head->conjunctArray[var->from], smoothVarBddArray, &bModified);
864        mdd_array_free(smoothVarBddArray);
865      }
866    }
867    if(bModified == 0)  break;
868    ImgLinearVariableArrayInit(head);
869  }
870  bdd_free(oneBdd);
871  return;
872}
873
874
875
876
877/**Function********************************************************************
878
879  Synopsis    [Refine transition relation.]
880
881  Description [Clean up the Relation_t data structure after applying linear arrangement of transition relation]
882
883  SideEffects []
884
885  SeeAlso     []
886
887******************************************************************************/
888void
889ImgLinearRefineRelation(Relation_t *head)
890{
891  ImgLinearConjunctArrayRefine(head);
892  ImgLinearVariableArrayInit(head);
893}
894
895/**Function********************************************************************
896
897  Synopsis    [Order the fine grain transition relation.]
898
899  Description [First find the connected component and apply ordering procedure for each component.]
900
901  SideEffects []
902
903  SeeAlso     []
904
905******************************************************************************/
906void
907ImgLinearConjunctOrderMainCC(Relation_t *head, int refineFlag)
908{
909Conjunct_t **connectedArray;
910int i, index;
911char baseName[1024];
912
913  ImgLinearPrintMatrix(head);
914  ImgLinearExtractNextStateCase(head);
915  ImgLinearClusterSameSupportSet(head);
916  ImgLinearRefineRelation(head);
917
918  ImgLinearExtractSingletonCase(head);
919  ImgLinearRefineRelation(head);
920
921  ImgLinearConnectedComponent(head);
922
923  for(i=0; i<head->nConnectedComponent; i++) {
924    connectedArray = head->connectedComponent[i];
925    for(index=0; (long)(connectedArray[index])>0; index++);
926    head->conjunctArray = connectedArray;
927    head->nSize = index;
928    head->bModified = 1;
929    head->bRefineVarArray = 1;
930    qsort(head->conjunctArray, head->nSize, sizeof(Conjunct_t *), 
931          ImgLinearCompareConjunctSize);
932    ImgLinearVariableArrayInit(head);
933
934    ImgLinearConjunctOrderMain(head, 0);
935    fprintf(stdout, "NOTICE : %d'th connected component\n", i);
936    head->connectedComponent[i] = head->conjunctArray;
937    head->conjunctArray = 0;
938  }
939
940  ImgLinearBuildConjunctArrayWithQuotientCC(head);
941 
942  ImgLinearAddSingletonCase(head);
943  ImgLinearAddNextStateCase(head);
944  ImgLinearExpandSameSupportSet(head);
945  ImgLinearRefineRelation(head);
946
947  ImgLinearRefineRelation(head);
948  ImgLinearPrintMatrix(head);
949
950  sprintf(baseName, "profile");
951  ImgLinearPrintVariableProfile(head, baseName);
952  ImgLinearPrintMatrixFull(head, 2);
953}
954/**Function********************************************************************
955
956  Synopsis    [Order the each connected component]
957
958  Description [The new Relation_t is created for each connected component]
959
960  SideEffects []
961
962  SeeAlso     []
963
964******************************************************************************/
965void
966ImgLinearBuildConjunctArrayWithQuotientCC(Relation_t *head)
967{
968Conjunct_t *conjunct, *tConjunct;
969Conjunct_t **connectedArray;
970Conjunct_t **conjunctArray;
971Conjunct_t **newConjunctArray;
972st_table *table;
973int i, j, k, l;
974int index, id, size;
975int *varType, *supList;
976st_generator *gen;
977char baseName[1024];
978
979  if(head->nConnectedComponent == 1) {
980    size = 0;
981    newConjunctArray = ALLOC(Conjunct_t *, size+1);
982    connectedArray = head->connectedComponent[0];
983    for(j=0; (long)(connectedArray[j])>0; j++) {
984      tConjunct = connectedArray[j];
985      newConjunctArray[size++] = tConjunct;
986      newConjunctArray = REALLOC(Conjunct_t *, newConjunctArray, size+1);
987    }
988    free(head->conjunctArray);
989    head->nSize = size;
990    head->conjunctArray = newConjunctArray;
991    head->bModified = 1;
992    head->bRefineVarArray = 1;
993    ImgLinearRefineRelation(head);
994    return;
995  }
996
997  head->includeCS = 1;
998  head->includeNS = 1;
999  varType = head->varType;
1000  conjunctArray = ALLOC(Conjunct_t *, head->nConnectedComponent);
1001  for(i=0; i<head->nConnectedComponent; i++) {
1002    connectedArray = head->connectedComponent[i];
1003
1004    table = st_init_table(st_ptrcmp, st_ptrhash);
1005    for(j=0; (long)(connectedArray[j])>0; j++) {
1006      conjunct = connectedArray[j];
1007      size = conjunct->nSize;
1008      supList = conjunct->supList;
1009      for(k=0; k<size; k++) {
1010        id = supList[k];
1011        st_insert(table, (char *)(long)id, (char *)(long)id);
1012      }
1013      for(l=0; l<conjunct->nCluster; l++) {
1014        tConjunct = conjunct->clusterArray[l];
1015        size = tConjunct->nSize;
1016        supList = tConjunct->supList;
1017        for(k=0; k<size; k++) {
1018          id = supList[k];
1019          st_insert(table, (char *)(long)id, (char *)(long)id);
1020        }
1021      }
1022    }
1023
1024    conjunct = ALLOC(Conjunct_t, 1);
1025    memset(conjunct, 0, sizeof(Conjunct_t));
1026    conjunct->index = i;
1027    conjunct->dummy = (long)connectedArray;
1028    supList = ALLOC(int, table->num_entries);
1029    index = 0;
1030    st_foreach_item(table, gen, &id, &id) {
1031      if(varType[id] == 1)      conjunct->nDomain++;
1032      else if(varType[id] == 2) conjunct->nRange++;
1033      else if(varType[id] == 3) conjunct->nQuantify++;
1034      supList[index++] = id;
1035    }
1036    conjunct->supList = supList;
1037    conjunct->nSize = index;
1038
1039    conjunctArray[i] = conjunct;
1040    conjunct->index = i;
1041    conjunct->relation = bdd_zero(head->mgr);
1042  }
1043
1044  head->nSize = head->nConnectedComponent;
1045  head->conjunctArray = conjunctArray;
1046  head->bRefineVarArray = 1;
1047  ImgLinearVariableArrayInit(head);
1048
1049  sprintf(baseName, "TopCon");
1050  ImgLinearCAPOInterfaceConjunctNodes(head, baseName);
1051  ImgLinearCAPOInterfaceConjunctNet(head, baseName);
1052  ImgLinearCAPOInterfaceConjunctScl(head, baseName);
1053  ImgLinearCAPOInterfaceConjunctPl(head, baseName);
1054  ImgLinearCAPOInterfaceAux(head, baseName);
1055  ImgLinearCAPORun("MetaPlacer", baseName, 0);
1056  ImgLinearCAPOReadConjunctOrder(head, baseName);
1057
1058  size = 0;
1059  newConjunctArray = ALLOC(Conjunct_t *, size+1);
1060  conjunctArray = head->conjunctArray;
1061  for(i=0; i<head->nSize; i++) {
1062    conjunct = head->conjunctArray[i];
1063    connectedArray = (Conjunct_t **)conjunct->dummy;
1064    for(j=0; (long)(connectedArray[j])>0; j++) {
1065      tConjunct = connectedArray[j];
1066      newConjunctArray[size++] = tConjunct;
1067      newConjunctArray = REALLOC(Conjunct_t *, newConjunctArray, size+1);
1068    }
1069    ImgLinearConjunctQuit(conjunct);
1070  }
1071  free(conjunctArray);
1072  head->conjunctArray = newConjunctArray;
1073  head->nSize = size;
1074  head->bModified = 1;
1075  head->bRefineVarArray = 1;
1076  ImgLinearRefineRelation(head);
1077
1078}
1079
1080
1081/**Function********************************************************************
1082
1083  Synopsis    [Find the connected component from fine grain transition relation]
1084
1085  Description [Find the connected component from fine grain transition relation]
1086
1087  SideEffects []
1088
1089  SeeAlso     []
1090
1091******************************************************************************/
1092void
1093ImgLinearConnectedComponent(Relation_t *head)
1094{
1095Conjunct_t *conjunct;
1096Conjunct_t **connectedArray;
1097int i, j, index, cc_index;
1098int pre_index, pre_cc_index;
1099
1100  ImgLinearVariableArrayInit(head);
1101
1102  for(i=0; i<head->nSize; i++) {
1103    conjunct = head->conjunctArray[i];
1104    conjunct->dummy = 0;
1105  }
1106
1107  cc_index = 0;
1108  for(i=0; i<head->nSize; i++) {
1109    conjunct = head->conjunctArray[i];
1110    if(conjunct->dummy) continue;
1111    cc_index++;
1112    ImgLinearFindConnectedComponent(head, conjunct, cc_index);
1113  }
1114  qsort(head->conjunctArray, head->nSize, sizeof(Conjunct_t *), 
1115                     ImgLinearCompareConjunctDummy);
1116
1117  head->nConnectedComponent = 0;
1118  pre_index = 0;
1119  pre_cc_index = 1;
1120  for(i=0; i<head->nSize; i++) {
1121    conjunct = head->conjunctArray[i];
1122    if(conjunct->dummy != pre_cc_index) {
1123      if((i-pre_index) == 1) { /** singleton case **/
1124        head->singletonArray = ImgLinearAddConjunctIntoArray(
1125                head->singletonArray, &(head->nSingletonArray), 
1126                head->conjunctArray[i-1]);
1127      }
1128      else { /** connected component case **/
1129        if(head->nConnectedComponent)
1130          head->connectedComponent = REALLOC(Conjunct_t **, head->connectedComponent, head->nConnectedComponent+1);
1131        else
1132          head->connectedComponent = ALLOC(Conjunct_t **, head->nConnectedComponent+1);
1133
1134        connectedArray = ALLOC(Conjunct_t *, (i-pre_index+2));
1135        head->connectedComponent[head->nConnectedComponent++] = connectedArray;
1136        for(index=0, j=pre_index; j<i; j++)
1137          connectedArray[index++] = head->conjunctArray[j];
1138        connectedArray[index] = 0;
1139      }
1140
1141      pre_cc_index = conjunct->dummy;
1142      pre_index = i;
1143    }
1144  }
1145
1146  if((i-pre_index) == 1) { /** singleton case **/
1147    head->singletonArray = ImgLinearAddConjunctIntoArray(
1148                head->singletonArray, &(head->nSingletonArray), 
1149                head->conjunctArray[i-1]);
1150  }
1151  else { /** connected component case **/
1152    if(head->nConnectedComponent)
1153      head->connectedComponent = REALLOC(Conjunct_t **,
1154head->connectedComponent, head->nConnectedComponent+1);
1155
1156    else
1157      head->connectedComponent = ALLOC(Conjunct_t **,
1158head->nConnectedComponent+1);
1159
1160    connectedArray = ALLOC(Conjunct_t *, (i-pre_index+2));
1161    head->connectedComponent[head->nConnectedComponent++] = connectedArray;
1162    for(index=0, j=pre_index; j<i; j++)
1163      connectedArray[index++] = head->conjunctArray[j];
1164    connectedArray[index] = 0;
1165  }
1166  free(head->conjunctArray);
1167}
1168
1169/**Function********************************************************************
1170
1171  Synopsis    [Find the connected component from fine grain transition relation]
1172
1173  Description [Find the connected component from fine grain transition relation]
1174
1175  SideEffects []
1176
1177  SeeAlso     []
1178
1179******************************************************************************/
1180void
1181ImgLinearFindConnectedComponent(Relation_t *head, 
1182                                 Conjunct_t *conjunct, 
1183                                 int cc_index)
1184{
1185VarLife_t *var;
1186int *supList;
1187int id, size;
1188int index, i, j;
1189int *relArr;
1190Conjunct_t *tConjunct;
1191 
1192  if(conjunct->dummy)   return;
1193  supList = conjunct->supList;
1194  size = conjunct->nSize;
1195  conjunct->dummy = cc_index;
1196  for(i=0; i<size; i++) {
1197    id = supList[i];
1198    var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0;
1199   if(!var)     continue;
1200    relArr = var->relArr;
1201    for(j=0; j<var->nSize; j++) {
1202      index = relArr[j];
1203      if(index == MAXINT)       continue;
1204      if(index == MAXINT-1)     continue;
1205      tConjunct = head->conjunctArray[index];
1206      if(tConjunct->dummy)      continue;
1207      ImgLinearFindConnectedComponent(head, tConjunct, cc_index);
1208    }
1209  }
1210}
1211
1212
1213/**Function********************************************************************
1214
1215  Synopsis    [Extract the relation contains only one next state varaible]
1216
1217  Description [Extract the relation contains only one next state varaible]
1218
1219  SideEffects []
1220
1221  SeeAlso     []
1222
1223******************************************************************************/
1224void
1225ImgLinearExtractSingletonCase(Relation_t *head) 
1226{
1227int i, j, k, id, index;
1228VarLife_t **varArray, *var;
1229int nSingleton;
1230int *supList, *varType;
1231Conjunct_t *conjunct, **newSingletonArray;
1232int *singletonArray;
1233
1234  varType = head->varType;
1235  varArray = head->varArray;
1236  nSingleton = 0;
1237  singletonArray = ALLOC(int , nSingleton+1);
1238  for(i=0; i<head->nVarArray; i++) {
1239    var = varArray[i];
1240    if(var->stateVar == 2)      continue;
1241    if(var->stateVar == 1) {
1242      if(var->nSize - head->includeCS > 1)      continue;
1243    }
1244    else {
1245      if(var->nSize > 1)        continue;
1246    }
1247
1248    for(j=0; j<var->nSize; j++) {
1249      if(var->relArr[j] == MAXINT)      continue;
1250      if(var->relArr[j] == MAXINT-1)    continue;
1251      singletonArray[nSingleton++] = var->relArr[j];
1252      singletonArray = REALLOC(int , singletonArray, nSingleton+1);
1253    }
1254  }
1255
1256  for(i=0; i<nSingleton; i++) {
1257    conjunct = head->conjunctArray[singletonArray[i]];
1258    conjunct->bSingleton = 1;
1259  }
1260
1261  for(i=0; i<nSingleton; i++) {
1262    conjunct = head->conjunctArray[singletonArray[i]];
1263    if(conjunct->nRange == conjunct->nSize-conjunct->nRange &&
1264       conjunct->nSize-conjunct->nRange != 1) {
1265      conjunct->bSingleton = 0;
1266      continue;
1267    }
1268
1269    supList = conjunct->supList;
1270    for(j=0; j<conjunct->nSize; j++) {
1271      id = supList[j];
1272      if(varType[id] == 2)  continue;
1273      var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0;
1274      if(!var)  continue;
1275
1276      if(var->stateVar == 1) {
1277        if(var->nSize - head->includeCS == 1) continue;
1278      }
1279      else {
1280        if(var->nSize == 1)     continue;
1281      }
1282      for(k=0; k<var->nSize; k++) {
1283        index = var->relArr[k];
1284        if(index == MAXINT)     continue;
1285        if(index == MAXINT-1)   continue;
1286        (head->conjunctArray[index])->bSingleton = 0;
1287      }
1288    }
1289  }
1290 
1291  newSingletonArray = ALLOC(Conjunct_t *, nSingleton);
1292  for(index=0, i=0; i<nSingleton; i++) {
1293    conjunct = head->conjunctArray[singletonArray[i]];
1294    if(conjunct == 0)   continue;
1295    if(conjunct->bSingleton) {
1296      newSingletonArray[index++] = conjunct;
1297      head->conjunctArray[singletonArray[i]] = 0;
1298    }
1299  }
1300  head->nSingletonArray = index;
1301  free(singletonArray);
1302  qsort(newSingletonArray, head->nSingletonArray, 
1303          sizeof(Conjunct_t *), ImgLinearCompareConjunctRangeMinusDomain);
1304  head->singletonArray = newSingletonArray;
1305
1306  if(head->nSingletonArray)     {
1307    head->bModified = 1;
1308    head->bRefineVarArray = 1;
1309  }
1310}
1311
1312/**Function********************************************************************
1313
1314  Synopsis    [Add Conjunct into Cluster Array]
1315
1316  Description [Add Conjunct into Cluster Array]
1317
1318  SideEffects []
1319
1320  SeeAlso     []
1321
1322******************************************************************************/
1323void
1324ImgLinearAddConjunctIntoClusterArray(Conjunct_t *base, Conjunct_t *con)
1325{
1326  if(base->clusterArray == 0) {
1327    base->clusterArray = ALLOC(Conjunct_t *, base->nCluster+1);
1328    base->clusterArray[base->nCluster++] = con;
1329  }
1330  else {
1331    base->clusterArray = REALLOC(Conjunct_t *, base->clusterArray, base->nCluster+1);
1332    base->clusterArray[base->nCluster++] = con;
1333  }
1334  base->bClustered = 1;
1335}
1336
1337
1338
1339/**Function********************************************************************
1340
1341  Synopsis    [Extract the relation that contains next state varaibles only]
1342
1343  Description [Extract the relation that contains next state varaibles only]
1344
1345  SideEffects []
1346
1347  SeeAlso     []
1348
1349******************************************************************************/
1350void
1351ImgLinearExtractNextStateCase(Relation_t *head) 
1352{
1353int i, index, flag;
1354Conjunct_t *conjunct;
1355Conjunct_t **nextStateArray;
1356
1357  index = 0;
1358  flag = 1;
1359  nextStateArray = ALLOC(Conjunct_t *, index+1);
1360  for(index=0, i=head->nSize-1; i>=0; i--) {
1361    conjunct = head->conjunctArray[i];
1362    if(conjunct == 0)   continue;
1363    if(conjunct->nSize == conjunct->nRange && flag == 0) {
1364      nextStateArray[index++] = conjunct;
1365      nextStateArray = REALLOC(Conjunct_t *, nextStateArray, index+1);
1366      head->conjunctArray[i] = 0;
1367      head->bModified = 1;
1368    }
1369    if(conjunct->nSize != conjunct->nRange) flag = 0;
1370  }
1371  head->nextStateArray = nextStateArray;
1372  head->nNextStateArray = index;
1373
1374  ImgLinearRefineRelation(head);
1375}
1376
1377/**Function********************************************************************
1378
1379  Synopsis    [Free Relation_t data structure]
1380
1381  Description [Free Relation_t data structure]
1382
1383  SideEffects []
1384
1385  SeeAlso     []
1386
1387******************************************************************************/
1388void
1389ImgLinearRelationQuit(Relation_t *head)
1390{
1391int i;
1392Conjunct_t *conjunct;
1393
1394  if(head->varArray)            ImgLinearVariableArrayQuit(head);
1395  if(head->rangeVars)           free(head->rangeVars);
1396  if(head->domainVars)          free(head->domainVars);
1397  if(head->quantifyVars)        free(head->quantifyVars);
1398  if(head->varType)             free(head->varType);
1399  if(head->varArrayMap)         free(head->varArrayMap);
1400
1401  if(head->singletonArray)      free(head->singletonArray);
1402  if(head->nextStateArray)      free(head->nextStateArray);
1403
1404  if(head->constantCase) {
1405    for(i=0; i<head->nVar; i++)
1406      if(head->constantCase[i]) bdd_free(head->constantCase[i]);
1407  }
1408
1409  for(i=0; i<head->nSize; i++) {
1410    conjunct = head->conjunctArray[i];
1411    ImgLinearConjunctQuit(conjunct);
1412  }
1413  free(head);
1414}
1415
1416
1417/**Function********************************************************************
1418
1419  Synopsis    [Apply clustering iteratively]
1420
1421  Description [Apply clustering iteratively]
1422
1423  SideEffects []
1424
1425  SeeAlso     []
1426
1427******************************************************************************/
1428int
1429ImgLinearClusteringIteratively(Relation_t *head,
1430                                double affinityLimit,
1431                                int andExistLimit,
1432                                int varLimit,
1433                                int includeZeroGain,
1434                                int useFailureHistory,
1435                                Img_OptimizeType optDir,
1436                                int (*compare_func)(const void *, const void *))
1437{
1438int bddLimit, gainLimit;
1439int clusterLimit;
1440int bOptimize;
1441
1442  if(head->nSize < 2)   return(0);
1443
1444  bOptimize = 0;
1445  bddLimit = head->bddLimit;
1446  gainLimit = 50;
1447
1448  while(1) {
1449    if(head->nSize < 50)clusterLimit = head->nSize/2;
1450    else                clusterLimit = head->nSize/3+1;
1451    if(clusterLimit > 50)       clusterLimit = 50;
1452    /**
1453    clusterLimit = head->nSize/5;
1454    if(clusterLimit < 1)        clusterLimit = 3;
1455    **/
1456
1457    ImgLinearClusteringByConstraints(head, includeZeroGain, varLimit, clusterLimit, 
1458                                      gainLimit, affinityLimit, andExistLimit,
1459                                      bddLimit,  useFailureHistory, compare_func);
1460    if(head->bModified) {
1461      ImgLinearRefineRelation(head);
1462      bOptimize |= ImgLinearOptimizeAll(head, optDir, 0);
1463    }
1464    else break;
1465  }
1466  return(bOptimize);
1467}
1468/**Function********************************************************************
1469
1470  Synopsis    [Apply clustering with given priority function]
1471
1472  Description [Apply clustering with given priority function]
1473
1474  SideEffects []
1475
1476  SeeAlso     []
1477
1478******************************************************************************/
1479void
1480ImgLinearClusteringByConstraints(Relation_t *head, 
1481                                   int includeZeroGain,
1482                                   int varLimit,
1483                                   int clusterLimit,
1484                                   int gainLimit,
1485                                   double affinityLimit,
1486                                   int andExistLimit,
1487                                   int bddLimit, 
1488                                   int useFailureHistory,
1489                                   int (*compare_func)(const void *, const void *))
1490{
1491int size, begin, end;
1492int **nDead, **nVar, **nFailure;
1493int *dirtyBit;
1494int i, j, k, l, index;
1495int start, preGain;
1496int nClusterArray;
1497VarLife_t **varArray, *var;
1498Cluster_t **clusterArray, *clu;
1499Conjunct_t *conjunct;
1500bdd_t *clusteredRelation;
1501int fail_flag;
1502int from, to, splitable;
1503
1504  varArray = head->varArray;
1505  size = head->nSize;
1506
1507  nDead = ALLOC(int *, size);
1508  nVar = ALLOC(int *, size);
1509  nFailure = 0;
1510  if(useFailureHistory)
1511    nFailure = ALLOC(int *, size);
1512  for(i=0; i<size; i++) {
1513    nDead[i] = ALLOC(int, size);
1514    nVar[i] = ALLOC(int, size);
1515    if(useFailureHistory)
1516      nFailure[i] = ALLOC(int, size);
1517    memset(nDead[i], 0, sizeof(int)*size);
1518    memset(nVar[i], 0, sizeof(int)*size);
1519    if(useFailureHistory)
1520      memset(nFailure[i], 0, sizeof(int)*size);
1521  }
1522
1523  index = 0;
1524  for(l=0; l<head->nVarArray; l++) {
1525    var = varArray[l];
1526    begin = var->from;
1527    end = var->to;
1528    if(var->stateVar == 1)      begin = -1;
1529    else if(var->stateVar == 2) end = size;
1530
1531    for(i=0; i<=begin; i++)
1532      for(j=end; j<size; j++)
1533        nDead[i][j]++;
1534
1535    for(i=0; i<=var->effTo; i++) {
1536      if(i > var->effFrom) {
1537        for(k=0; k<var->nSize; k++) {
1538          index = var->relArr[k];
1539          if(index == MAXINT)   continue;
1540          if(index == MAXINT-1) continue;
1541          if(index >= i)        break;
1542        }
1543        if(index < i)   start = var->effTo;
1544        else            start = index;
1545      }
1546      else {
1547        start = var->effFrom;
1548      }
1549
1550      for(j=start; j<size; j++)
1551        nVar[i][j]++;
1552    }
1553  }
1554
1555  for(i=0; i<size; i++) {
1556    end = (size-1) < i+clusterLimit ? size-1 : i+clusterLimit;
1557    if(i==end)  continue;
1558    if(nDead[i][end] == 0 && !includeZeroGain)  continue;
1559
1560    preGain = -1;
1561    for(j=end; j>=i; j--) {
1562      if(varLimit < nVar[i][j]-nDead[i][j])     continue;
1563      if(gainLimit < nDead[i][j])               continue; 
1564
1565
1566      if(preGain != -1) {
1567        if(nDead[i][j] < preGain && nDead[i][j] >= 0) {
1568          to = j+1;
1569          for(from=i; from < to; from++) {
1570            if(nDead[from+1][to] != nDead[from][to])    break;
1571          }
1572          if(from != i) continue;
1573
1574          splitable = 0;
1575          for(k=from; k<to; k++) {
1576            if(nDead[from][to] == (nDead[from][k] + nDead[k+1][to])) {
1577              splitable = 1;
1578              break;
1579            }
1580          }
1581          if(!splitable)
1582            ImgLinearInsertClusterCandidate(head, from, to, 
1583                             nDead[from][to], nVar[from][to], affinityLimit);
1584        }
1585      }
1586
1587      if(nDead[i][j] == 0)      {
1588        if(includeZeroGain)
1589          ImgLinearInsertClusterCandidate(head, i, i+1, 
1590                             nDead[i][i+1], nVar[i][i+1], affinityLimit);
1591        break;
1592      }
1593
1594      preGain = nDead[i][j];
1595
1596    }
1597  }
1598 
1599  if(head->nClusterArray == 0)  return;
1600  qsort(head->clusterArray, head->nClusterArray, sizeof(Cluster_t *),
1601compare_func);
1602
1603  dirtyBit = ALLOC(int, size);
1604  memset(dirtyBit, 0, sizeof(int)*size);
1605
1606  clusterArray = head->clusterArray;
1607  nClusterArray = head->nClusterArray;
1608  for(i=0; i<nClusterArray; i++) {
1609    clu = clusterArray[i];
1610    if(useFailureHistory) {
1611      if(nFailure[clu->from][clu->to] == 1)     continue;
1612    }
1613    fail_flag = 0;
1614    for(j=clu->from; j<=clu->to; j++) {
1615      if(dirtyBit[j] == 1)      {
1616          fail_flag = 1;
1617        continue;
1618      }
1619    }
1620    if(fail_flag)       continue;
1621
1622    clusteredRelation = ImgLinearClusteringSmooth(head, clu, 
1623                           nFailure, andExistLimit, bddLimit);
1624
1625    conjunct = 0;
1626    if(clusteredRelation) {
1627      for(j=clu->from; j<=clu->to; j++) {
1628        conjunct = head->conjunctArray[j];
1629        if(conjunct->relation)  bdd_free(conjunct->relation);
1630        conjunct->relation = 0;
1631      }
1632      conjunct->relation = clusteredRelation;
1633      conjunct->bModified = 1;
1634      head->bModified = 1;
1635      for(j=clu->from; j<=clu->to; j++) dirtyBit[j] = 1;
1636
1637      if(head->verbosity >= 5)
1638        fprintf(stdout, "\tClustering Success : %4d -%4d G(%3d) V(%3d) A(%3d)\n",
1639              clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity);
1640    }
1641    fflush(stdout);
1642  }
1643
1644  for(i=0; i<nClusterArray; i++)
1645    free(clusterArray[i]);
1646  free(clusterArray);
1647  head->clusterArray = 0;
1648  head->nClusterArray = 0;
1649
1650  for(i=0; i<head->nSize; i++) {
1651    free(nDead[i]);
1652    free(nVar[i]);
1653    if(useFailureHistory)
1654      free(nFailure[i]);
1655  }
1656  free(nDead);
1657  free(nVar);
1658  if(useFailureHistory)
1659    free(nFailure);
1660
1661  return;
1662}
1663/**Function********************************************************************
1664
1665  Synopsis    [Add candidates for clustering]
1666
1667  Description [Add candidates for clustering, each condidate has pair of relation]
1668
1669  SideEffects []
1670
1671  SeeAlso     []
1672
1673******************************************************************************/
1674static void
1675ImgLinearInsertClusterCandidate(Relation_t *head, 
1676                                 int from, int to, 
1677                                 int nDead, int nVar,
1678                                 double affinityLimit)
1679{
1680Conjunct_t *conjunct;
1681Cluster_t *clu;
1682int *varType, *supList;
1683int i, j, id, size;
1684st_table *table;
1685double affinity, tAffinity;
1686int preSize, postSize, curSize, overlap;
1687
1688  varType = head->varType;
1689
1690  conjunct = head->conjunctArray[from];
1691  if(conjunct->relation == 0)   {
1692    return;
1693  }
1694
1695  supList = conjunct->supList;
1696  size = conjunct->nSize;
1697  table = st_init_table(st_numcmp, st_numhash);
1698  for(i=0; i<size; i++) {
1699    id = supList[i];
1700    if(varType[id] == 2)        continue;
1701    st_insert(table, (char *)(long)id, (char *)(long)id);
1702  }
1703
1704  tAffinity = 0.0;
1705  for(i=from+1; i<=to; i++) {
1706    preSize = table->num_entries;
1707
1708    conjunct = head->conjunctArray[i];
1709    if(conjunct->relation == 0) continue;
1710    supList = conjunct->supList;
1711    size = conjunct->nSize;
1712    curSize = 0;
1713    for(j=0; j<size; j++) {
1714      id = supList[j];
1715
1716      if(varType[id] == 2)      continue;
1717      curSize++;
1718      st_insert(table, (char *)(long)id, (char *)(long)id);
1719    }
1720
1721    postSize = table->num_entries;
1722
1723    overlap = curSize - (postSize-preSize);
1724
1725    if(curSize > preSize)       affinity = (double)overlap/(double)preSize;
1726    else                        affinity = (double)overlap/(double)curSize;
1727
1728    /**
1729    if(affinity < affinityLimit)        {
1730      st_free_table(table);
1731      return;
1732    }
1733    **/
1734    tAffinity += affinity;
1735  }
1736  st_free_table(table);
1737
1738  tAffinity /= (double)(to-from);
1739  clu = ALLOC(Cluster_t, 1);
1740  clu->from = from;
1741  clu->to = to;
1742  clu->nVar = nVar;
1743  clu->nDead = nDead;
1744  clu->nAffinity = (int)(tAffinity * 100.0);
1745
1746  head->clusterArray = REALLOC(Cluster_t *, head->clusterArray, head->nClusterArray+1);
1747  head->clusterArray[head->nClusterArray++] = clu;
1748  if(head->verbosity >= 5) {
1749    fprintf(stdout, "Candidate Cluster : %4d-%4d G(%3d) V(%3d) A(%3d)\n",
1750              clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity);
1751    fflush(stdout);
1752  }
1753
1754}
1755
1756/**Function********************************************************************
1757
1758  Synopsis    [Apply clustering while quantifying the variables that are isolated]
1759
1760  Description [Apply clustering while quantifying the variables that are isolated]
1761
1762  SideEffects []
1763
1764  SeeAlso     []
1765
1766******************************************************************************/
1767static bdd_t *
1768ImgLinearClusteringSmooth(Relation_t *head, 
1769                           Cluster_t *clu, 
1770                           int **failureHistory, 
1771                           int andExistLimit,
1772                           int bddLimit)
1773{
1774int *varType, *supList;
1775array_t *smoothVarBddArray, *smoothArray;
1776Conjunct_t *conjunct;
1777bdd_t *relation, *totalRelation;
1778bdd_t *varBdd, *tempRelation;
1779int i, j, k, tempSize, failFlag;
1780int id, tid;
1781st_table *deadTable;
1782VarLife_t *var;
1783
1784  varType = head->varType;
1785
1786  smoothVarBddArray = array_alloc(array_t *, 0);
1787  for(i=clu->from; i<=clu->to; i++) {
1788    smoothArray = array_alloc(bdd_t *, 0);
1789    array_insert_last(array_t *, smoothVarBddArray, smoothArray);
1790  }
1791
1792  deadTable = st_init_table(st_numcmp, st_numhash);
1793  for(i=clu->from; i<=clu->to; i++) {
1794    conjunct = head->conjunctArray[i];
1795    if(conjunct == 0)           continue;
1796    if(conjunct->relation == 0) continue;
1797    supList = conjunct->supList;
1798    for(j=0; j<conjunct->nSize; j++) {
1799      id = supList[j];
1800      if(varType[id] == 1 || varType[id] == 2)  continue;
1801
1802      if(st_lookup(deadTable, (char *)(long)id, &tid))  continue;
1803
1804      var = head->varArray[head->varArrayMap[id]];
1805
1806      if(clu->from <= var->from && var->to <= clu->to) {
1807        st_insert(deadTable, (char *)(long)id, (char *)(long)id);
1808        smoothArray = array_fetch(array_t *, smoothVarBddArray,
1809var->to-clu->from);
1810        varBdd = bdd_get_variable(head->mgr, var->id);
1811        array_insert_last(bdd_t *, smoothArray, varBdd);
1812      }
1813    }
1814  }
1815  st_free_table(deadTable);
1816
1817
1818  totalRelation = bdd_one(head->mgr);
1819  failFlag = 0;
1820  for(i=clu->from; i<=clu->to; i++) {
1821    conjunct = head->conjunctArray[i];
1822    if(conjunct == 0)           continue;
1823    if(conjunct->relation == 0) continue;
1824    relation = conjunct->relation;
1825    smoothArray = array_fetch(array_t *, smoothVarBddArray, i-clu->from);
1826
1827    tempRelation = bdd_and_smooth_with_limit(totalRelation, relation, 
1828                                        smoothArray, andExistLimit);
1829    if(tempRelation)    tempSize = bdd_size(tempRelation);
1830    else                tempSize = MAXINT;
1831
1832    if(tempSize > bddLimit) {
1833      bdd_free(totalRelation);
1834      if(tempRelation)  bdd_free(tempRelation);
1835      totalRelation = 0;
1836     
1837      if(failureHistory) {
1838        for(j=0; j<=clu->from; j++) 
1839          for(k=i; k<head->nSize; k++)
1840            failureHistory[j][k] = 1;
1841      }
1842
1843      if(head->verbosity >= 3)
1844        fprintf(stdout, "Clustering Failure : %4d-%4d G(%3d) V(%3d) A(%3d) At %3d S(%d)\n",
1845              clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity, i, tempSize);
1846      break;
1847    }
1848
1849    bdd_free(totalRelation);
1850    totalRelation = tempRelation;
1851  }
1852  ImgLinearFreeSmoothArray(smoothVarBddArray);
1853
1854  if(failFlag)  return(0);
1855  else          return(totalRelation);
1856}
1857
1858
1859/**Function********************************************************************
1860
1861  Synopsis    [ Apply clustering with priority queue]
1862
1863  Description [ Apply clustering with priority queue]
1864
1865  SideEffects []
1866
1867  SeeAlso     []
1868
1869******************************************************************************/
1870static int
1871ImgLinearClusterUsingHeap(Relation_t *head,
1872                           double affinityLimit,
1873                           int andExistLimit,
1874                           int varLimit,
1875                           Img_OptimizeType optDir,
1876                           int rangeFlag,
1877                           int (*compare_func)(const void *, const void *))
1878{
1879Cluster_t *clu;
1880int j;
1881Conjunct_t *conjunct;
1882bdd_t *clusteredRelation;
1883Heap_t *heap;
1884int bOptimize;
1885long dummy;
1886
1887  bOptimize = 0;
1888  ImgLinearBuildInitialCandidate(head, affinityLimit, varLimit, rangeFlag, compare_func);
1889  /** need to consider statevariable optimization **/
1890  heap = head->clusterHeap;
1891  while(Heap_HeapExtractMin(heap, &clu, &dummy)) {
1892    if(clu->flag) {
1893      free(clu);
1894      continue;
1895    }
1896    if(clu->to >= head->nSize) {
1897      free(clu);
1898      continue;
1899    }
1900
1901    clusteredRelation = ImgLinearClusteringPairSmooth(head, clu, 
1902                           0, andExistLimit, head->bddLimit);
1903    if(clusteredRelation) {
1904      if(head->verbosity >= 5)
1905        fprintf(stdout, "\tClustering Success : %4d -%4d G(%3d) V(%3d) A(%3d)\n",
1906              clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity);
1907      fflush(stdout);
1908
1909      for(j=clu->from+1; j<=clu->to; j++) {
1910        conjunct = head->conjunctArray[j];
1911        if(conjunct == 0)       continue;
1912        if(conjunct->relation == 0)     continue;
1913        bdd_free(conjunct->relation);
1914        conjunct->relation = 0;
1915      }
1916      conjunct = head->conjunctArray[clu->from];
1917      if(conjunct->relation)
1918        bdd_free(conjunct->relation);
1919      conjunct->relation = clusteredRelation;
1920      conjunct->bModified = 1;
1921      ImgLinearConjunctRefine(head, conjunct);
1922      head->bModified = 1;
1923      head->bRefineVarArray = 1;
1924
1925      Heap_HeapApplyForEachElement(heap, linearCheckRange);
1926      /**
1927      for(i=0; i<heap->nitems; i++) {
1928        tclu = (Cluster_t *)(heap->slots[i].item);
1929        if(tclu->from <= clu->from && clu->from <= tclu->to)
1930          tclu->flag = 1;
1931        if(tclu->from <= clu->to && clu->to <= tclu->to)
1932          tclu->flag = 1;
1933      }
1934      **/
1935
1936      ImgLinearInsertPairClusterCandidate(head, clu->from, affinityLimit, varLimit, rangeFlag);
1937      ImgLinearInsertPairClusterCandidate(head, clu->from-1, affinityLimit, varLimit, rangeFlag);
1938    }
1939    if(clu->nDead && clusteredRelation) {
1940      ImgLinearVariableArrayInit(head);
1941      bOptimize |= ImgLinearOptimizeAll(head, optDir, 0);
1942    }
1943    free(clu);
1944  }
1945  Heap_HeapFree(heap);
1946  head->clusterHeap = 0;
1947
1948  if(head->bModified) {
1949    if(head->verbosity >= 5)
1950      ImgLinearPrintMatrix(head);
1951
1952    bOptimize |= ImgLinearOptimizeAll(head, optDir, 0);
1953    ImgLinearRefineRelation(head);
1954
1955    if(head->verbosity >= 5)
1956      ImgLinearPrintMatrix(head);
1957  }
1958  return(bOptimize);
1959}
1960
1961/**Function********************************************************************
1962
1963  Synopsis    [compare function for checking range of cluster]
1964
1965  Description [compare function for checking range of cluster]
1966
1967  SideEffects []
1968
1969  SeeAlso     []
1970
1971******************************************************************************/
1972static int
1973linearCheckRange(const void *tc)
1974{
1975Cluster_t *tclu;
1976
1977  tclu = (Cluster_t *)tc;
1978  if(tclu->from <= __clu->from && __clu->from <= tclu->to)
1979    tclu->flag = 1;
1980  if(tclu->from <= __clu->to && __clu->to <= tclu->to)
1981    tclu->flag = 1;
1982
1983  return(1);
1984}
1985
1986/**Function********************************************************************
1987
1988  Synopsis    [Clustering pair of transition relation]
1989
1990  Description [Clustering pair of transition relation]
1991
1992  SideEffects []
1993
1994  SeeAlso     []
1995
1996******************************************************************************/
1997static bdd_t *
1998ImgLinearClusteringPairSmooth(Relation_t *head, 
1999                           Cluster_t *clu, 
2000                           int **failureHistory, 
2001                           int andExistLimit,
2002                           int bddLimit)
2003{
2004int *varType, *supList;
2005array_t *smoothArray;
2006Conjunct_t *conjunct;
2007bdd_t *totalRelation;
2008bdd_t *fromRelation, *toRelation;
2009bdd_t *varBdd;
2010int i, j, k, tempSize;
2011int id, tid, effTo;
2012st_table *deadTable;
2013VarLife_t *var;
2014
2015  varType = head->varType;
2016
2017  smoothArray = array_alloc(bdd_t *, 0);
2018
2019  for(effTo = clu->to+1; effTo<head->nSize; effTo++) {
2020    conjunct = head->conjunctArray[effTo];
2021    if(conjunct && conjunct->relation)  break;
2022  }
2023  effTo--;
2024
2025  deadTable = st_init_table(st_numcmp, st_numhash);
2026  for(i=clu->from; i<=clu->to; i++) {
2027    conjunct = head->conjunctArray[i];
2028    if(conjunct == 0)           continue;
2029    if(conjunct->relation == 0) continue;
2030    supList = conjunct->supList;
2031    for(j=0; j<conjunct->nSize; j++) {
2032      id = supList[j];
2033      if(varType[id] == 1 || varType[id] == 2)  continue;
2034
2035      if(st_lookup(deadTable, (char *)(long)id, &tid))  continue;
2036
2037      var = head->varArray[head->varArrayMap[id]];
2038
2039      if(clu->from <= var->from && var->to <= effTo) {
2040        st_insert(deadTable, (char *)(long)id, (char *)(long)id);
2041        varBdd = bdd_get_variable(head->mgr, var->id);
2042        array_insert_last(bdd_t *, smoothArray, varBdd);
2043      }
2044    }
2045  }
2046  st_free_table(deadTable);
2047
2048  conjunct = head->conjunctArray[clu->from];
2049  fromRelation = conjunct->relation;
2050  toRelation = 0;
2051  for(i=clu->from+1; i<=clu->to; i++) {
2052    conjunct = head->conjunctArray[i];
2053    if(conjunct == 0)           continue;
2054    if(conjunct->relation == 0) continue;
2055    toRelation = conjunct->relation;
2056    break;
2057  }
2058  if(toRelation == 0) {
2059    mdd_array_free(smoothArray);
2060    return(0);
2061  }
2062  if(fromRelation == 0 && toRelation == 0)      return(0);
2063  if(fromRelation == 0) {
2064    totalRelation = bdd_dup(toRelation);
2065  }
2066  else if(toRelation == 0) {
2067    totalRelation = bdd_dup(fromRelation);
2068  }
2069  else {
2070    totalRelation = bdd_and_smooth_with_limit(fromRelation, toRelation, 
2071                                                smoothArray, andExistLimit);
2072  }
2073  if(totalRelation)     tempSize = bdd_size(totalRelation);
2074  else                  tempSize = MAXINT;
2075
2076  if(tempSize > bddLimit) {
2077    if(totalRelation)   bdd_free(totalRelation);
2078    totalRelation = 0;
2079    if(failureHistory) {
2080      for(j=0; j<=clu->from; j++) 
2081        for(k=i; k<head->nSize; k++)
2082          failureHistory[j][k] = 1;
2083    }
2084    if(head->verbosity >= 3)
2085      fprintf(stdout, "Clustering Failure : %4d-%4d G(%3d) V(%3d) A(%3d) At %3d S(%d)\n",
2086              clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity, i, tempSize);
2087  }
2088  mdd_array_free(smoothArray);
2089
2090  return(totalRelation);
2091}
2092
2093
2094
2095/**Function********************************************************************
2096
2097  Synopsis    [Build data structure for clustering]
2098
2099  Description [Build data structure for clustering]
2100
2101  SideEffects []
2102
2103  SeeAlso     []
2104
2105******************************************************************************/
2106
2107static void 
2108ImgLinearBuildInitialCandidate(Relation_t *head, 
2109                                double affinityLimit,
2110                                int varLimit, 
2111                                int rangeFlag,
2112                                int (*compare_func)(const void *, const void *))
2113{
2114int size, i;
2115
2116  head->clusterHeap = Heap_HeapInitCompare(head->nSize, compare_func);
2117  size = head->nSize;
2118  for(i=0; i<size; i++) {
2119    ImgLinearInsertPairClusterCandidate(head, i, affinityLimit, varLimit, rangeFlag);
2120  }
2121 
2122  return;
2123}
2124/**Function********************************************************************
2125
2126  Synopsis    [Insert initial candidate set]
2127
2128  Description [Insert initial candidate set]
2129
2130  SideEffects []
2131
2132  SeeAlso     []
2133
2134******************************************************************************/
2135static void
2136ImgLinearInsertPairClusterCandidate(Relation_t *head, 
2137                                     int from, 
2138                                     double affinityLimit,
2139                                     int varLimit,
2140                                     int rangeFlag)
2141{
2142Conjunct_t *conjunct, *fromC, *toC;
2143Cluster_t *clu;
2144int *varType, *supList;
2145st_table *table;
2146double affinity;
2147int preSize, postSize, curSize, overlap;
2148int i, j, id, tid, size, nDead;
2149int to, effTo;
2150VarLife_t *var;
2151
2152  if(from < 0)  return;
2153  if(from == head->nSize-1)     return;
2154 
2155  conjunct = head->conjunctArray[from];
2156  if(conjunct == 0 || conjunct->relation == 0) {
2157    for(; from>=0; from--) {
2158      conjunct = head->conjunctArray[from];
2159      if(conjunct == 0) continue;
2160      if(conjunct->relation == 0)       continue;
2161      break;
2162    }
2163  }
2164  if(from < 0)  return;
2165
2166  to = -1;
2167  for(i=from+1; i<head->nSize; i++) {
2168    conjunct = head->conjunctArray[i];
2169    if(!conjunct)       continue;
2170    if(conjunct->relation == 0) continue;
2171    to = i;
2172    break;
2173  }
2174  if(to == -1)  return;
2175  for(effTo = to+1; effTo<head->nSize; effTo++) {
2176    conjunct = head->conjunctArray[effTo];
2177    if(conjunct && conjunct->relation)  break;
2178  }
2179  effTo--;
2180
2181
2182  varType = head->varType;
2183
2184  fromC = head->conjunctArray[from];
2185  toC = head->conjunctArray[to];
2186
2187  if(rangeFlag && 
2188     (fromC->nSize == fromC->nRange || toC->nSize == toC->nRange))
2189      return;
2190
2191  if(fromC->nSize == fromC->nRange && toC->nSize != toC->nRange)
2192    return;
2193  if(fromC->nSize != fromC->nRange && toC->nSize == toC->nRange)
2194    return;
2195
2196  nDead = 0;
2197  supList = fromC->supList;
2198  size = fromC->nSize;
2199  table = st_init_table(st_numcmp, st_numhash);
2200  for(i=0; i<size; i++) {
2201    id = supList[i];
2202    if(varType[id] == 2)        continue;
2203    preSize++;
2204    st_insert(table, (char *)(long)id, (char *)(long)id);
2205    var = head->varArray[head->varArrayMap[id]];
2206    if(from <= var->from && var->to <= effTo)   nDead++;
2207  }
2208
2209  preSize = table->num_entries;
2210  supList = toC->supList;
2211  size = toC->nSize;
2212  curSize = 0;
2213  for(j=0; j<size; j++) {
2214    id = supList[j];
2215    if(varType[id] == 2)        continue;
2216    curSize++;
2217    if(st_lookup(table, (char *)(long)id, &tid))        continue;
2218    st_insert(table, (char *)(long)id, (char *)(long)id);
2219    var = head->varArray[head->varArrayMap[id]];
2220    if(from <= var->from && var->to <= effTo)   nDead++;
2221  }
2222
2223  postSize = table->num_entries;
2224  overlap = curSize - (postSize-preSize);
2225  if(overlap == 0)      affinity = 0.0;
2226  else {
2227    if(curSize > preSize)affinity = (double)overlap/(double)preSize;
2228    else                 affinity = (double)overlap/(double)curSize;
2229  }
2230  st_free_table(table);
2231
2232  if(affinity < affinityLimit)  return;
2233
2234  if(affinity == 0.0 && postSize > 10 && 
2235          (fromC->bSingleton || toC->bSingleton))       return;
2236  if(postSize-nDead > varLimit) return;
2237
2238  clu = ALLOC(Cluster_t, 1);
2239  memset(clu, 0, sizeof(Cluster_t));
2240  clu->from = from;
2241  clu->to = to;
2242  clu->nVar = postSize;
2243  clu->nDead = nDead;
2244  clu->nAffinity = (int)(affinity * 100.0);
2245
2246  Heap_HeapInsertCompare(head->clusterHeap, (void *)clu, (long)clu);
2247  if(head->verbosity >= 5) {
2248    fprintf(stdout, "Candidate Cluster : %4d -%4d G(%3d) V(%3d) A(%3d)\n",
2249              clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity);
2250    fflush(stdout);
2251  }
2252}
2253
2254/**Function********************************************************************
2255
2256  Synopsis    [Print information of debug information]
2257
2258  Description [Print information of debug information]
2259
2260  SideEffects []
2261
2262  SeeAlso     []
2263
2264******************************************************************************/
2265static void
2266ImgLinearPrintDebugInfo(Relation_t *head)
2267{
2268int i, j, id;
2269Conjunct_t *conjunct;
2270int *supList;
2271array_t *smoothVarBddArray;
2272array_t *smoothArray;
2273bdd_t *varBdd;
2274int idPerLine;
2275
2276  idPerLine = 12;
2277
2278  fprintf(vis_stdout, "-----------------------------------------------------\n");
2279  fprintf(vis_stdout, "     Debug Information for Transition Relations\n");
2280  fprintf(vis_stdout, "-----------------------------------------------------\n");
2281  fprintf(vis_stdout, "List of Quantify Variables---------------------------\n");
2282  for(i=0; i<head->nQuantify; i++) {
2283    if(i!=0 && i%idPerLine == 0) fprintf(vis_stdout, "\n");
2284    fprintf(vis_stdout, "%3d ", head->quantifyVars[i]);
2285  }
2286  fprintf(vis_stdout, "\n");
2287
2288  fprintf(vis_stdout, "List of Domain Variables-----------------------------\n");
2289  for(i=0; i<head->nDomain; i++) {
2290    if(i!=0 && i%idPerLine == 0) fprintf(vis_stdout, "\n");
2291    fprintf(vis_stdout, "%3d ", head->domainVars[i]);
2292  }
2293  fprintf(vis_stdout, "\n");
2294
2295  fprintf(vis_stdout, "List of Range Variables------------------------------\n");
2296  for(i=0; i<head->nRange; i++) {
2297    if(i!=0 && i%idPerLine == 0) fprintf(vis_stdout, "\n");
2298    fprintf(vis_stdout, "%3d ", head->rangeVars[i]);
2299  }
2300  fprintf(vis_stdout, "\n");
2301
2302  fprintf(vis_stdout, "Varibles in Each Transition Relation-----------------\n");
2303  for(i=0; i<head->nSize; i++) {
2304    conjunct = head->conjunctArray[i];
2305    supList = conjunct->supList;
2306    fprintf(vis_stdout, "%3d'th : ", i);
2307    for(j=0; j<conjunct->nSize; j++) {
2308      if(j!=0 && j%idPerLine == 0) fprintf(vis_stdout, "\n         ");
2309      fprintf(vis_stdout, "%3d ", supList[j]);
2310    }
2311    fprintf(vis_stdout, "\n");
2312  }
2313
2314  smoothVarBddArray = ImgLinearMakeSmoothVarBdd(head, 0);
2315  fprintf(vis_stdout, "Quantified Schedule----------------------------------\n");
2316  for(i=0; i<=head->nSize; i++) {
2317    fprintf(vis_stdout, "%3d'th : ", i);
2318    smoothArray = array_fetch(array_t *, smoothVarBddArray, i);
2319    for(j=0; j<array_n(smoothArray); j++) {
2320      varBdd = array_fetch(bdd_t *, smoothArray, j);
2321      id = bdd_top_var_id(varBdd);
2322      if(j!=0 && j%idPerLine == 0) fprintf(vis_stdout, "\n         ");
2323      fprintf(vis_stdout, "%3d ", id);
2324    }
2325    fprintf(vis_stdout, "\n");
2326  }
2327  ImgLinearFreeSmoothArray(smoothVarBddArray);
2328}
2329
2330/**Function********************************************************************
2331
2332  Synopsis    [ Main function of linear arrangement]
2333
2334  Description [ Main function of linear arrangement]
2335
2336  SideEffects []
2337
2338  SeeAlso     []
2339
2340******************************************************************************/
2341static void
2342ImgLinearConjunctOrderMain(Relation_t *head, int bRefineConjunctOrder)
2343{
2344double aal, atl;
2345
2346/**
2347  head->includeCS = 0;
2348  ImgLinearConjunctionOrder(head, "FirstCon", bRefineConjunctOrder);
2349  ImgLinearComputeLifeTime(head, &aal, &atl);
2350  ImgLinearPrintMatrixFull(head, 0);
2351  head->includeCS = 1;
2352  tempConjunctArray = ALLOC(Conjunct_t *, head->nSize+1);
2353  for(i=0; i<head->nSize; i++)
2354    tempConjunctArray[i] = head->conjunctArray[i];
2355  tempAal = aal;
2356  tempAtl = atl;
2357  fprintf(stdout, "NOTICE : aal %.3f atl %.3f\n", aal, atl);
2358  ImgLinearPrintMatrix(head);
2359  **/
2360
2361
2362  ImgLinearConjunctionOrder(head, "SecondCon", bRefineConjunctOrder);
2363  ImgLinearComputeLifeTime(head, &aal, &atl);
2364  ImgLinearPrintMatrixFull(head, 1);
2365  fprintf(stdout, "NOTICE : aal %.3f atl %.3f\n", aal, atl);
2366  ImgLinearPrintMatrix(head);
2367
2368  /**
2369  if(tempAal < aal) {
2370    if( (aal-tempAal) > (tempAtl-atl)*2.0 ) {
2371      free(head->conjunctArray);
2372      head->conjunctArray = tempConjunctArray;
2373      head->bModified = 1;
2374      head->bRefineVarArray = 1;
2375      ImgLinearRefineRelation(head);
2376      fprintf(stdout, "includeCS = 0 is taken\n");
2377    }
2378    else {
2379      fprintf(stdout, "includeCS = 1 is taken\n");
2380    }
2381  }
2382  else {
2383    fprintf(stdout, "includeCS = 1 is taken\n");
2384  }
2385  **/
2386}
2387
2388/**Function********************************************************************
2389
2390  Synopsis    [Generate linear arrangement with CAPO]
2391
2392  Description [Generate linear arrangement with CAPO]
2393
2394  SideEffects []
2395
2396  SeeAlso     []
2397
2398******************************************************************************/
2399static void
2400ImgLinearConjunctionOrder(Relation_t *head, char *baseName, int refineFlag)
2401{
2402Conjunct_t *conjunct;
2403int i, j;
2404
2405
2406  if(head->nSize < 2)   return;
2407  for(i=0; i<head->nSize; i++) {
2408    conjunct = head->conjunctArray[i];
2409    conjunct->dummy = 0;
2410    for(j=0; j<conjunct->nSize; j++)
2411      conjunct->dummy += conjunct->supList[j];
2412  }
2413  qsort(head->conjunctArray, head->nSize, sizeof(Conjunct_t *), 
2414          ImgLinearCompareConjunctSize);
2415  head->bRefineVarArray = 1;
2416  ImgLinearRefineRelation(head);
2417
2418  ImgLinearCAPOInterfaceConjunctNodes(head, baseName);
2419  ImgLinearCAPOInterfaceConjunctNet(head, baseName);
2420  ImgLinearCAPOInterfaceConjunctScl(head, baseName);
2421  ImgLinearCAPOInterfaceConjunctPl(head, baseName);
2422  ImgLinearCAPOInterfaceAux(head, baseName);
2423  ImgLinearCAPORun("MetaPlacer", baseName, 0);
2424  ImgLinearCAPOReadConjunctOrder(head, baseName);
2425}
2426
2427
2428/**Function********************************************************************
2429
2430  Synopsis    [Make interface files for CAPO]
2431
2432  Description [Make interface files for CAPO]
2433
2434  SideEffects []
2435
2436  SeeAlso     []
2437
2438******************************************************************************/
2439static void
2440ImgLinearCAPOInterfaceConjunctNodes(Relation_t *head, char *baseName)
2441{
2442char filename[1024];
2443FILE *fout;
2444int i;
2445
2446  sprintf(filename, "%s.nodes", baseName);
2447  fout = fopen(filename, "w");
2448  fprintf(fout, "UCLA nodes 1.0\n");
2449  if(head->includeNS) {
2450    if(head->includeCS) {
2451      fprintf(fout, "NumNodes : %d\n", head->nSize+2);
2452      fprintf(fout, "NumTerminals : 2\n");
2453    }
2454    else {
2455      fprintf(fout, "NumNodes : %d\n", head->nSize+1);
2456      fprintf(fout, "NumTerminals : 1\n");
2457    }
2458  }
2459  else if(head->includeCS) {
2460    fprintf(fout, "NumNodes : %d\n", head->nSize+1);
2461    fprintf(fout, "NumTerminals : 1\n");
2462  }
2463  else {
2464    fprintf(fout, "NumNodes : %d\n", head->nSize);
2465    fprintf(fout, "NumTerminals : 0\n");
2466  }
2467 
2468  for(i=0; i<head->nSize; i++)
2469    fprintf(fout, "C%d 1 1\n", i);
2470
2471  if(head->includeCS) 
2472    fprintf(fout, "C%d 1 1 terminal\n", MAXINT-1);
2473
2474  if(head->includeNS)
2475    fprintf(fout, "C%d 1 1 terminal\n", MAXINT);
2476
2477  fclose(fout);
2478}
2479
2480/**Function********************************************************************
2481
2482  Synopsis    [Make interface files for CAPO]
2483
2484  Description [Make interface files for CAPO]
2485
2486  SideEffects []
2487
2488  SeeAlso     []
2489
2490******************************************************************************/
2491static void
2492ImgLinearCAPOInterfaceConjunctNet(Relation_t *head, char *baseName)
2493{
2494char filename[1024];
2495FILE *fout;
2496VarLife_t **varArray, *var;
2497int i, j, nPin;
2498
2499  varArray = head->varArray;
2500  sprintf(filename, "%s.nets", baseName);
2501  fout = fopen(filename, "w");
2502  fprintf(fout, "UCLA nets 1.0\n");
2503  fprintf(fout, "#NumNets : %d\n", head->nVarArray);
2504
2505  qsort(head->varArray, head->nVarArray, sizeof(VarLife_t *), ImgLinearCompareVarId);
2506  nPin = 0;
2507  for(i=0; i<head->nVarArray; i++) {
2508    var = varArray[i];
2509    if(var->nSize == 1) nPin += 2;
2510    else                nPin += var->nSize;
2511  }
2512  fprintf(fout, "NumPins : %d\n", nPin);
2513
2514  for(i=0; i<head->nVarArray; i++) {
2515    var = varArray[i];
2516    if(var->nSize == 1)
2517      fprintf(fout, "NetDegree : %d S%d\n", var->nSize+1, var->id);
2518    else
2519      fprintf(fout, "NetDegree : %d S%d\n", var->nSize, var->id);
2520
2521    for(j=0; j<var->nSize; j++)
2522      fprintf(fout, "C%d B\n", var->relArr[j]);
2523
2524    if(var->nSize == 1) 
2525      fprintf(fout, "C%d B\n", var->relArr[0]);
2526  }
2527  fclose(fout);
2528}
2529
2530
2531/**Function********************************************************************
2532
2533  Synopsis    [Make interface files for CAPO]
2534
2535  Description [Make interface files for CAPO]
2536
2537  SideEffects []
2538
2539  SeeAlso     []
2540
2541******************************************************************************/
2542static void
2543ImgLinearCAPOInterfaceConjunctScl(Relation_t *head, char *baseName)
2544{
2545char filename[1024];
2546FILE *fout;
2547
2548  sprintf(filename, "%s.scl", baseName);
2549  fout = fopen(filename, "w");
2550  fprintf(fout, "UCLA scl 1.0\n");
2551  fprintf(fout, "Numrows : 1\n");
2552  fprintf(fout, "CoreRow Horizontal\n");
2553  fprintf(fout, " Coordinate   : 1\n");
2554  fprintf(fout, " Height       : 1\n");
2555  fprintf(fout, " Sitewidth    : 1\n");
2556  fprintf(fout, " Sitespacing  : 1\n");
2557  fprintf(fout, " Siteorient   : N\n");
2558  fprintf(fout, " Sitesymmetry : Y\n");
2559  fprintf(fout, " SubrowOrigin : 0\n");
2560  fprintf(fout, " Numsites     : %d\n", head->nSize*2+2);
2561  fprintf(fout, "End\n");
2562  fclose(fout);
2563}
2564
2565/**Function********************************************************************
2566
2567  Synopsis    [Make interface files for CAPO]
2568
2569  Description [Make interface files for CAPO]
2570
2571  SideEffects []
2572
2573  SeeAlso     []
2574
2575******************************************************************************/
2576static void
2577ImgLinearCAPOInterfaceConjunctPl(Relation_t *head, char *baseName)
2578{
2579char filename[1024];
2580FILE *fout;
2581int i;
2582
2583  sprintf(filename, "%s.pl", baseName);
2584  fout = fopen(filename, "w");
2585
2586  fprintf(fout, "UCLA pl 1.0\n");
2587  for(i=0; i<head->nSize; i++)
2588    fprintf(fout, "C%d %d 1\n", i, (i+2)*2+1);
2589
2590  if(head->includeCS)
2591    fprintf(fout, "C%d 0 1 / N / FIXED\n", MAXINT-1);
2592
2593  if(head->includeNS)
2594    fprintf(fout, "C%d %d 1 / N / FIXED\n", MAXINT, (head->nSize+2)*2+1);
2595
2596  fclose(fout);
2597}
2598
2599/**Function********************************************************************
2600
2601  Synopsis    [Make interface files for CAPO]
2602
2603  Description [Make interface files for CAPO]
2604
2605  SideEffects []
2606
2607  SeeAlso     []
2608
2609******************************************************************************/
2610static void
2611ImgLinearCAPOInterfaceAux(Relation_t *head, char *baseName)
2612{
2613char filename[1024];
2614FILE *fout;
2615
2616  sprintf(filename, "%s.aux", baseName);
2617  fout = fopen(filename, "w");
2618  fprintf(fout, "RowBasedPlacement : ");
2619  fprintf(fout, "%s.nodes %s.nets %s.pl %s.scl\n", 
2620                baseName, baseName, baseName, baseName);
2621  fclose(fout);
2622}
2623
2624/**Function********************************************************************
2625
2626  Synopsis    [Run batch job of CAPO]
2627
2628  Description [Run batch job of CAPO]
2629
2630  SideEffects []
2631
2632  SeeAlso     []
2633
2634******************************************************************************/
2635static int
2636ImgLinearCAPORun(char *capoExe, char *baseName, int brief)
2637{
2638char logFile[1024];
2639char capoOption[1024];
2640char command[1024];
2641char cpCommand[1024];
2642FILE *fout;
2643int cmdStatus;
2644
2645  fout = fopen("seeds.in", "w");
2646  fprintf(fout, "0\n");
2647  fprintf(fout, "460427264\n");
2648  fclose(fout);
2649
2650
2651  if(brief)     
2652    sprintf(capoOption, "-replaceSmallBlocks Never -noRowIroning -save -saveXorder");
2653  else         
2654    sprintf(capoOption, "-save -saveXorder -clust CutOpt");
2655
2656  sprintf(logFile, "%s.log", baseName);
2657  sprintf(command, "%s -f %s.aux %s > %s", 
2658            capoExe, baseName, capoOption, logFile);
2659  cmdStatus = system(command);
2660  sprintf(cpCommand, "cp left2right.ord %s.ord", baseName);
2661  cmdStatus |= system(cpCommand);
2662
2663  unlink("seeds.out");
2664  unlink("left2right.ord");
2665  return (cmdStatus == 0);
2666}
2667
2668
2669/**Function********************************************************************
2670
2671  Synopsis    [Read result of CAPO]
2672
2673  Description [Read result of CAPO]
2674
2675  SideEffects []
2676
2677  SeeAlso     []
2678
2679******************************************************************************/
2680static void
2681ImgLinearCAPOReadConjunctOrder(Relation_t *head, char *baseName)
2682{
2683char ordFile[1024];
2684char line[1024];
2685int index, id;
2686char *next;
2687FILE *fin;
2688Conjunct_t *conjunct;
2689
2690  sprintf(ordFile, "%s.ord", baseName);
2691  if(!(fin = fopen(ordFile, "r"))) {
2692    fprintf(stdout, "Can't open order file %s\n", ordFile);
2693    exit(0);
2694  }
2695  index = 0;
2696  while(fgets(line, 1024, fin)){
2697    next = strchr(line, 'C');
2698    next++;
2699    sscanf(next, "%d", &id);
2700    if(id == MAXINT) continue;
2701    if(id == MAXINT-1) continue;
2702    conjunct = head->conjunctArray[id];
2703    conjunct->index = index;
2704    index++;
2705  }
2706  fclose(fin);
2707
2708  qsort(head->conjunctArray, head->nSize, sizeof(Conjunct_t *), ImgLinearCompareConjunctIndex);
2709
2710  head->bModified = 1;
2711  head->bRefineVarArray = 1;
2712  ImgLinearRefineRelation(head);
2713}
2714
2715/**Function********************************************************************
2716
2717  Synopsis    [Make interface for variable ordering]
2718
2719  Description [Make interface for variable ordering]
2720
2721  SideEffects []
2722
2723  SeeAlso     []
2724
2725******************************************************************************/
2726static void
2727ImgLinearVariableOrder(Relation_t *head, char *baseName, int includeNS)
2728{
2729  ImgLinearCAPOInterfaceVariableNodes(head, baseName, includeNS);
2730  ImgLinearCAPOInterfaceVariableNet(head, baseName, includeNS);
2731  ImgLinearCAPOInterfaceVariableScl(head, baseName);
2732  ImgLinearCAPOInterfaceVariablePl(head, baseName, includeNS);
2733  ImgLinearCAPOInterfaceAux(head, baseName);
2734  ImgLinearCAPORun("MetaPlacer", baseName, 0);
2735  ImgLinearCAPOReadVariableOrder(head, baseName, includeNS);
2736}
2737
2738/**Function********************************************************************
2739
2740  Synopsis    [Make interface for CAPO]
2741
2742  Description [Make interface for CAPO]
2743
2744  SideEffects []
2745
2746  SeeAlso     []
2747
2748******************************************************************************/
2749void
2750ImgLinearCAPOInterfaceVariableNodes(Relation_t *head, char *baseName, int includeNS)
2751{
2752int i, size;
2753VarLife_t **varArray, *var;
2754int *varType;
2755char filename[1024];
2756FILE *fout;
2757int numUnused;
2758
2759  varArray = head->varArray;
2760  varType = head->varType;
2761  sprintf(filename, "%s.nodes", baseName);
2762  fout = fopen(filename, "w");
2763
2764  fprintf(fout, "UCLA nodes 1.0\n");
2765
2766  size = 0;
2767  if(includeNS) size = head->nVarArray;
2768  else {
2769    for(i=0; i<head->nVarArray; i++) {
2770      if(varType[varArray[i]->id] == 2) continue;
2771      size++;
2772    }
2773  }
2774
2775  numUnused = 0;
2776  for(i=0; i<head->nVar; i++) {
2777    if(varType[i] != 1) continue; /* if it is not domain variable **/
2778    var = head->varArrayMap[i] >=0 ? head->varArray[head->varArrayMap[i]] : 0;
2779    if(var)     continue;
2780    numUnused++;
2781  }
2782  if(includeNS) {
2783    for(i=0; i<head->nVar; i++) {
2784      if(varType[i] != 2)       continue; /* if it is not range variable **/
2785      var = head->varArrayMap[i] >=0 ? head->varArray[head->varArrayMap[i]] : 0;
2786     if(var)    continue;
2787      numUnused++;
2788    }
2789  }
2790 
2791  fprintf(fout, "NumNodes : %d\n", size+numUnused);
2792  fprintf(fout, "NumTerminals : 0\n");
2793  for(i=0; i<head->nVarArray; i++) {
2794    var = varArray[i];
2795    if(includeNS == 0 && varType[var->id] == 2) continue;
2796    fprintf(fout, "C%d 1 1\n", var->id);
2797  }
2798
2799  for(i=0; i<head->nVar; i++) {
2800    if(varType[i] != 1) continue; /* if it is not domain variable **/
2801    var = head->varArrayMap[i] >=0 ? head->varArray[head->varArrayMap[i]] : 0;
2802    if(var)     continue;
2803    fprintf(fout, "C%d 1 1\n", i);
2804  }
2805  if(includeNS) {
2806    for(i=0; i<head->nVar; i++) {
2807      if(varType[i] != 2)       continue; /* if it is not range variable **/
2808      var = head->varArrayMap[i] >=0 ? head->varArray[head->varArrayMap[i]] : 0;
2809     if(var)    continue;
2810      fprintf(fout, "C%d 1 1\n", i);
2811    }
2812  }
2813  fclose(fout);
2814}
2815
2816/**Function********************************************************************
2817
2818  Synopsis    [Make interface for CAPO]
2819
2820  Description [Make interface for CAPO]
2821
2822  SideEffects []
2823
2824  SeeAlso     []
2825
2826******************************************************************************/
2827static void
2828ImgLinearCAPOInterfaceVariableNet(Relation_t *head, 
2829                                  char *baseName, 
2830                                  int includeNS)
2831{
2832int nPin, i, j;
2833int id, size;
2834Conjunct_t *conjunct;
2835bdd_t *relation;
2836int *supList, *varType;
2837char filename[1024];
2838FILE *fout;
2839
2840  nPin = 0;
2841  for(i=0; i<head->nSize; i++) {
2842    conjunct = head->conjunctArray[i];
2843    relation = conjunct->relation;
2844    if(relation == (mdd_t *)(MAXINT-1)) continue;
2845    supList = conjunct->supList;
2846    if(includeNS) {
2847      if(conjunct->nSize == 1)  nPin += 2; 
2848      else                      nPin += conjunct->nSize-conjunct->nRange;
2849    }
2850    else {
2851      if(conjunct->nSize-conjunct->nRange == 1) nPin += 2;
2852      else                                      nPin += conjunct->nSize-conjunct->nRange;
2853    }
2854  }
2855  nPin += head->nDomain;
2856  if(includeNS)
2857    nPin += head->nRange;
2858
2859  varType = head->varType;
2860  sprintf(filename, "%s.nets", baseName);
2861  fout = fopen(filename, "w");
2862  fprintf(fout, "UCLA nets 1.0\n");
2863  fprintf(fout, "#NumNets : %d\n", head->nSize);
2864  fprintf(fout, "NumPins : %d\n", nPin);
2865  for(i=0; i<head->nSize; i++) {
2866    conjunct = head->conjunctArray[i];
2867    relation = conjunct->relation;
2868    if(relation == (mdd_t *)(MAXINT-1)) continue;
2869
2870    supList = conjunct->supList;
2871    if(includeNS)       size = conjunct->nSize;
2872    else                size = conjunct->nSize - conjunct->nRange;
2873
2874    if(size == 1)       fprintf(fout, "NetDegree : %d \n", 2);
2875    else                fprintf(fout, "NetDegree : %d \n", size);
2876
2877    id = 0;
2878    if(includeNS) {
2879      for(j=0; j<conjunct->nSize; j++) {
2880        id = supList[j];
2881        fprintf(fout, "C%d B\n", id);
2882      }
2883    }
2884    else {
2885      for(j=0; j<conjunct->nSize; j++) {
2886        id = supList[j];
2887        if(varType[id] == 2)    continue;
2888        fprintf(fout, "C%d B\n", id);
2889      }
2890    }
2891    if(size == 1)
2892      fprintf(fout, "C%d B\n", id);
2893  }
2894  fprintf(fout, "NetDegree : %d \n", head->nDomain);
2895  for(i=0; i<head->nVar; i++) {
2896    if(varType[i] == 1) 
2897      fprintf(fout, "C%d B\n", i);
2898  }
2899  if(includeNS) {
2900    fprintf(fout, "NetDegree : %d \n", head->nRange);
2901    for(i=0; i<head->nVar; i++) {
2902      if(varType[i] == 2) 
2903        fprintf(fout, "C%d B\n", i);
2904    }
2905  }
2906  fclose(fout);
2907}
2908
2909/**Function********************************************************************
2910
2911  Synopsis    [Make interface for CAPO]
2912
2913  Description [Make interface for CAPO]
2914
2915  SideEffects []
2916
2917  SeeAlso     []
2918
2919******************************************************************************/
2920static void
2921ImgLinearCAPOInterfaceVariableScl(Relation_t *head, char *baseName)
2922{
2923char filename[1024];
2924FILE *fout;
2925
2926  sprintf(filename, "%s.scl", baseName);
2927  fout = fopen(filename, "w");
2928  fprintf(fout, "UCLA scl 1.0\n");
2929  fprintf(fout, "Numrows : 1\n");
2930  fprintf(fout, "CoreRow Horizontal\n");
2931  fprintf(fout, " Coordinate   : 1\n");
2932  fprintf(fout, " Height       : 1\n");
2933  fprintf(fout, " Sitewidth    : 1\n");
2934  fprintf(fout, " Sitespacing  : 1\n");
2935  fprintf(fout, " Siteorient   : N\n");
2936  fprintf(fout, " Sitesymmetry : Y\n");
2937  fprintf(fout, " SubrowOrigin : 0\n");
2938  fprintf(fout, " Numsites     : %d\n", head->nVarArray*2+2);
2939  fprintf(fout, "End\n");
2940  fclose(fout);
2941}
2942
2943
2944/**Function********************************************************************
2945
2946  Synopsis    [Make interface for CAPO]
2947
2948  Description [Make interface for CAPO]
2949
2950  SideEffects []
2951
2952  SeeAlso     []
2953
2954******************************************************************************/
2955static void
2956ImgLinearCAPOInterfaceVariablePl(Relation_t *head, char *baseName, int includeNS)
2957{
2958char filename[1024];
2959FILE *fout;
2960VarLife_t *var, **varArray;
2961int i, index, *varType;
2962
2963  varType = head->varType;
2964  sprintf(filename, "%s.pl", baseName);
2965  fout = fopen(filename, "w");
2966  fprintf(fout, "UCLA pl 1.0\n");
2967  varArray = head->varArray;
2968  for(index=0, i=0; i<head->nVarArray; i++) {
2969    var = varArray[i];
2970    if(includeNS == 0 && varType[var->id] == 2) continue;
2971    fprintf(fout, "C%d %d 1\n", var->id, (index+1)*2+1);
2972    index++;
2973  }
2974  fclose(fout);
2975}
2976
2977
2978
2979/**Function********************************************************************
2980
2981  Synopsis    [Read result of  CAPO]
2982
2983  Description [Read result of CAPO]
2984
2985  SideEffects []
2986
2987  SeeAlso     []
2988
2989******************************************************************************/
2990static void
2991ImgLinearCAPOReadVariableOrder(Relation_t *head, char *baseName, int includeNS)
2992{
2993char ordFile[1024], line[1024];
2994FILE *fin;
2995char *next;
2996int i, id, index, *permutation, *exist;
2997
2998  sprintf(ordFile, "%s.ord", baseName);
2999  if(!(fin = fopen(ordFile, "r"))) {
3000    fprintf(stdout, "Can't open order file %s\n", ordFile);
3001    exit(0);
3002  }
3003
3004  permutation = ALLOC(int, head->nVar);
3005  exist = ALLOC(int, head->nVar);
3006  memset(exist, 0, sizeof(int)*head->nVar);
3007
3008  index = 0;
3009  while(fgets(line, 1024, fin)){
3010    next = strchr(line, 'C');
3011    next++;
3012    sscanf(next, "%d", &id);
3013    permutation[index++] = id;
3014    exist[id] = 1;
3015    if(includeNS == 0 && head->varType[id] == 1) {
3016      permutation[index++] = head->domain2range[id];
3017      exist[head->domain2range[id]] = 1;
3018    }
3019  }
3020  fclose(fin);
3021
3022  for(i=0; i<head->nVar; i++)
3023    if(exist[i] == 0)
3024      permutation[index++] = i;
3025
3026  free(exist);
3027
3028  bdd_shuffle_heap(head->mgr, permutation);
3029
3030  free(permutation);
3031}
3032
3033/**Function********************************************************************
3034
3035  Synopsis    [Print profile of variables]
3036
3037  Description [Print profile of variables]
3038
3039  SideEffects []
3040
3041  SeeAlso     []
3042
3043******************************************************************************/
3044static void
3045ImgLinearPrintVariableProfile(Relation_t *head, char *baseName)
3046{
3047double aal, atl;
3048char filename[1024];
3049FILE *fout;
3050st_table *cutSet;
3051int i, j, nDead, id;
3052int *varType;
3053int *supList;
3054Conjunct_t *conjunct;
3055VarLife_t *var;
3056st_generator *gen;
3057
3058  ImgLinearVariableArrayInit(head);
3059  varType = head->varType;
3060
3061  sprintf(filename, "%s.data", baseName);
3062  fout = fopen(filename, "w");
3063
3064  cutSet = st_init_table(st_numcmp, st_numhash);
3065  for(i=0; i<head->nVar; i++) {
3066    if(varType[i] == 1) 
3067      st_insert(cutSet, (char *)(long)i, (char *)(long)i);
3068  }
3069
3070  for(i=0; i<head->nSize; i++) {
3071    conjunct = head->conjunctArray[i];
3072    supList = conjunct->supList;
3073    for(j=0; j<conjunct->nSize; j++)
3074      st_insert(cutSet, (char *)(long)supList[j], (char *)(long)supList[j]);
3075
3076    nDead = 0;
3077    st_foreach_item(cutSet, gen, &id, &id) {
3078      if(varType[id] == 2) continue;
3079
3080      var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] :
30810;
3082      if(!var) continue;
3083     
3084      if(var->to <= i)  {
3085        nDead++;
3086        st_delete(cutSet, (&id), NULL);
3087      }
3088    }
3089    fprintf(fout, "%d %d %d\n", i, cutSet->num_entries, cutSet->num_entries+nDead);
3090  }
3091  fclose(fout);
3092
3093  ImgLinearComputeLifeTime(head, &aal, &atl);
3094
3095  sprintf(filename, "%s.gnu", baseName);
3096  fout = fopen(filename, "w");
3097  fprintf(fout, "set terminal postscript \n");
3098  fprintf(fout, "set output \"%s.ps\"\n", baseName);
3099  fprintf(fout, "set title \"profile of live variable aal %.3f atl %.3f\"\n",
3100          aal, atl);
3101  fprintf(fout, "plot \"%s.data\" using 1:2 title \"%s\" with lines, \\\n", baseName, "cut");
3102  fprintf(fout, "     \"%s.data\" using 1:3 title \"%s\" with lines\n", baseName, "cut+dead");
3103  fclose(fout);
3104}
3105
3106/**Function********************************************************************
3107
3108  Synopsis    [Print matrix]
3109
3110  Description [Print matrix. Its x axis is varaible and its y axis is relation]
3111
3112  SideEffects [Print matrix. Its x axis is varaible and its y axis is relation]
3113
3114  SeeAlso     []
3115
3116******************************************************************************/
3117void
3118ImgLinearPrintMatrix(Relation_t *head)
3119{
3120int i, j, id, index;
3121int *mapArray;
3122VarLife_t **varArray, *var;
3123VarLife_t **auxArr, **sortArr;
3124int nAuxArr, nSortArr;
3125array_t *smoothVarBddArr, *smoothArray;
3126bdd_t *varBdd;
3127Conjunct_t *conjunct;
3128bdd_t *relation;
3129int *supList, *varType;
3130char *buffer;
3131int maxIndex;
3132
3133  if(head->verbosity < 5)       return;
3134
3135  ImgLinearVariableArrayInit(head);
3136
3137  mapArray = ALLOC(int, head->nVar);
3138  memset(mapArray, -1, sizeof(int)*head->nVar);
3139
3140  varArray = head->varArray;
3141
3142  smoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, 0);
3143  for(index=0, i=0; i<array_n(smoothVarBddArr); i++) {
3144    smoothArray = array_fetch(array_t *, smoothVarBddArr, i);
3145    nAuxArr = 0;
3146    auxArr = ALLOC(VarLife_t *, nAuxArr+1);
3147    for(j=0; j<array_n(smoothArray); j++) {
3148      varBdd = array_fetch(bdd_t *, smoothArray, j);
3149      id = (int)bdd_top_var_id(varBdd);
3150
3151      var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] :
31520;
3153      if(var) {
3154        auxArr[nAuxArr++] = var;
3155        auxArr = REALLOC(VarLife_t *, auxArr, nAuxArr+1);
3156      }
3157    }
3158    qsort(auxArr, nAuxArr, sizeof(VarLife_t *), ImgLinearCompareVarIndex);
3159    for(j=0; j<nAuxArr; j++)
3160      mapArray[auxArr[j]->id] = index++;
3161    free(auxArr);
3162  }
3163
3164  varArray = head->varArray;
3165  nSortArr = 0;
3166  sortArr = ALLOC(VarLife_t *, nSortArr+1);
3167  for(i=0; i<head->nVarArray; i++) {
3168    var = varArray[i];
3169    if(var->stateVar == 2)      continue;
3170    if(mapArray[var->id] >= 0) {
3171      var->index = mapArray[var->id];
3172      sortArr[nSortArr++] = var;
3173      sortArr = REALLOC(VarLife_t *, sortArr, nSortArr+1);
3174    }
3175    else {
3176      var->index = (double)MAXINT;
3177    }
3178  }
3179  qsort(sortArr, nSortArr, sizeof(VarLife_t *), ImgLinearCompareVarIndex);
3180
3181  fprintf(stdout, "     ");
3182  for(i=0; i<nSortArr; i++) fprintf(stdout, "%d", (i/10)%10);
3183  fprintf(stdout, "\n");
3184
3185  fprintf(stdout, "     ");
3186  for(i=0; i<nSortArr; i++) fprintf(stdout, "%d", i%10);
3187  fprintf(stdout, "\n");
3188
3189  buffer = ALLOC(char , nSortArr+1);
3190  for(i=0; i<nSortArr; i++) {
3191    var = sortArr[i];
3192    var->index = (double)i;
3193    if(var->stateVar == 1)      buffer[i] = 'C';
3194    else                        buffer[i] = 'T';
3195  }
3196  buffer[i] = '\0';
3197  free(sortArr);
3198  fprintf(stdout, "     %s\n", buffer);
3199
3200  maxIndex = i;
3201  for(i=0; i<maxIndex; i++)     buffer[i] = '.';
3202  buffer[i] = '\0';
3203
3204  varType = head->varType;
3205  for(index=0,i=head->nSize-1;i>=0; i--) {
3206    conjunct = head->conjunctArray[i];
3207    if(conjunct == 0)   continue;
3208    if(conjunct->relation == 0) continue;
3209    relation = conjunct->relation;
3210    if(relation == (mdd_t *)(MAXINT-1)) continue;
3211    if(relation == 0)                   continue;
3212    supList = conjunct->supList;
3213    for(j=0; j<conjunct->nSize; j++) {
3214      id = supList[j];
3215      if(varType[id] == 2)              continue;
3216      var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] :
32170;
3218      if(!var)  continue;
3219      if((int)var->index == MAXINT)     continue;
3220      buffer[(int)var->index] = '1';
3221    }
3222    index++;
3223    fprintf(stdout, "%4d %s %d %d\n", i, buffer, conjunct->nRange, bdd_size(relation));
3224    fflush(stdout);
3225    for(j=0; j<maxIndex; j++)   buffer[j] = '.';
3226    buffer[j] = '\0';
3227  }
3228  free(buffer);
3229}
3230/**Function********************************************************************
3231
3232  Synopsis    [Print matrix]
3233
3234  Description [Print matrix]
3235
3236  SideEffects []
3237
3238  SeeAlso     []
3239
3240******************************************************************************/
3241void
3242ImgLinearPrintMatrixFull(Relation_t *head, int matrixIndex)
3243{
3244int i, j, id, index;
3245int *mapArray;
3246VarLife_t **varArray, *var;
3247VarLife_t **auxArr, **sortArr;
3248int nAuxArr, nSortArr;
3249array_t *smoothVarBddArr, *smoothArray;
3250FILE *fout;
3251int min, max;
3252bdd_t *varBdd;
3253char filename[1024];
3254Conjunct_t *conjunct;
3255bdd_t *relation;
3256int *supList;
3257
3258  ImgLinearVariableArrayInit(head);
3259
3260  mapArray = ALLOC(int, head->nVar);
3261  memset(mapArray, -1, sizeof(int)*head->nVar);
3262  varArray = head->varArray;
3263
3264  smoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, 0);
3265  for(index=0, i=0; i<array_n(smoothVarBddArr); i++) {
3266    smoothArray = array_fetch(array_t *, smoothVarBddArr, i);
3267    nAuxArr = 0;
3268    auxArr = ALLOC(VarLife_t *, nAuxArr+1);
3269    for(j=0; j<array_n(smoothArray); j++) {
3270      varBdd = array_fetch(bdd_t *, smoothArray, j);
3271      id = (int)bdd_top_var_id(varBdd);
3272
3273      var = head->varArrayMap[id] >=0 ? varArray[head->varArrayMap[id]] : 0;
3274      if(var) {
3275        auxArr[nAuxArr++] = var;
3276        auxArr = REALLOC(VarLife_t *, auxArr, nAuxArr+1);
3277      }
3278    }
3279    qsort(auxArr, nAuxArr, sizeof(VarLife_t *), ImgLinearCompareVarIndex);
3280    for(j=0; j<nAuxArr; j++)
3281      mapArray[auxArr[j]->id] = index++;
3282    free(auxArr);
3283  }
3284
3285  nSortArr = 0;
3286  sortArr = ALLOC(VarLife_t *, nSortArr+1);
3287  for(i=0; i<head->nVarArray; i++) {
3288    var = varArray[i];
3289    if(var->stateVar == 2)      continue;
3290    if(mapArray[var->id] >= 0) {
3291      var->index = mapArray[var->id];
3292      sortArr[nSortArr++] = var;
3293      sortArr = REALLOC(VarLife_t *, sortArr, nSortArr+1);
3294    }
3295    else {
3296      var->index = (double)MAXINT;
3297    }
3298  }
3299
3300  qsort(sortArr, nSortArr, sizeof(VarLife_t *), ImgLinearCompareVarIndex);
3301  free(mapArray);
3302
3303  sprintf(filename, "fullmatrix%d.data", matrixIndex);
3304  fout = fopen(filename, "w");
3305  min = 0;
3306  max = head->nSize+1;
3307  for(i=0; i<nSortArr; i++) {
3308    var = sortArr[i];
3309    if(var->stateVar == 1)
3310      fprintf(fout, "%d %d\n", (int)var->index, min);
3311  }
3312  free(sortArr);
3313
3314  for(index=0, i=0; i<head->nSize; i++) {
3315    conjunct = head->conjunctArray[i];
3316    relation = conjunct->relation;
3317    if(relation == (mdd_t *)(MAXINT-1)) continue;
3318    if(relation == 0)                   continue;
3319    supList = conjunct->supList;
3320    for(j=0; j<conjunct->nSize; j++) {
3321      id = supList[j];
3322      var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0;
3323      if(!var)  continue; 
3324      if(var->stateVar == 2)
3325      if((int)var->index == MAXINT) continue;
3326      fprintf(fout, "%d %d\n", (int)var->index, index+1);
3327    }
3328    index++;
3329  }
3330  fclose(fout);
3331
3332  sprintf(filename, "fullmatrix%d.gnu", matrixIndex);
3333  fout = fopen(filename, "w");
3334  fprintf(fout, "set terminal postscript \n");
3335  fprintf(fout, "set output \"fullmatrix%d.ps\"\n", matrixIndex);
3336  fprintf(fout, "set title \"profile of live variable\"\n");
3337  fprintf(fout, "set yrange [-1:%d]\n", head->nSize+2);
3338  fprintf(fout, "plot \"fullmatrix%d.data\" using 1:2 title \"%d\" with point\n",
3339                  matrixIndex, matrixIndex);
3340  fclose(fout);
3341
3342  ImgLinearFreeSmoothArray(smoothVarBddArr);
3343}
3344
3345/**Function********************************************************************
3346
3347  Synopsis    [Free smooth variable array]
3348
3349  Description [Free smooth variable array]
3350
3351  SideEffects []
3352
3353  SeeAlso     []
3354
3355******************************************************************************/
3356void
3357ImgLinearFreeSmoothArray(array_t *smoothVarBddArray)
3358{
3359int i;
3360array_t *smoothArray;
3361
3362  for(i=0; i<array_n(smoothVarBddArray); i++) {
3363    smoothArray = array_fetch(array_t *, smoothVarBddArray, i);
3364    mdd_array_free(smoothArray);
3365  }
3366  array_free(smoothVarBddArray);
3367}
3368
3369/**Function********************************************************************
3370
3371  Synopsis    [Compute life time of variables]
3372
3373  Description [Compute life time of variables]
3374
3375  SideEffects []
3376
3377  SeeAlso     []
3378
3379******************************************************************************/
3380void
3381ImgLinearComputeLifeTime(Relation_t *head, double *paal, double *patl)
3382{
3383double aal, atl;
3384int i;
3385VarLife_t **varArray, *var;
3386
3387  aal = atl = 0.0;
3388  varArray = head->varArray;
3389  for(i=0; i<head->nVarArray; i++) {
3390    var = varArray[i];
3391    aal += var->effTo - var->effFrom;
3392    if(var->stateVar == 1)      atl += var->to+1;
3393    else if(var->stateVar == 2) atl += head->nSize+1 - var->from;
3394    else                        atl += var->to - var->from;
3395  }
3396  atl = atl / (double)(head->nVarArray * head->nSize);
3397  aal = aal / (double)(head->nVarArray * head->nSize);
3398
3399  *paal = aal;
3400  *patl = atl;
3401}
3402
3403/**Function********************************************************************
3404
3405  Synopsis    [Print transition relation info]
3406
3407  Description [Print transition relation info]
3408
3409  SideEffects []
3410
3411  SeeAlso     []
3412
3413******************************************************************************/
3414static void
3415ImgLinearPrintTransitionInfo(Relation_t *head)
3416{
3417double aal, atl;
3418
3419  fprintf(stdout, "SUMMARY : domain   variables %d -> %d -> %d\n", 
3420          head->nDomain, head->nInitDomain, head->nEffDomain);
3421  fprintf(stdout, "SUMMARY : range    variables %d -> %d -> %d\n", 
3422          head->nRange, head->nInitRange, head->nEffRange);
3423  fprintf(stdout, "SUMMARY : quantify variables %d -> %d -> %d\n", 
3424          head->nQuantify, head->nInitQuantify, head->nEffQuantify);
3425  fprintf(stdout, "SUMMARY : number of transition relation %d\n", 
3426          head->nSize);
3427  ImgLinearComputeLifeTime(head, &aal, &atl);
3428  fprintf(stdout, "Active  Life Time : %g\n", aal);
3429  fprintf(stdout, "Average Life Time : %g\n", atl);
3430}
3431
3432
3433
3434/**Function********************************************************************
3435
3436  Synopsis    [Make the array of smooth variables]
3437
3438  Description [Make the array of smooth variables]
3439
3440  SideEffects []
3441
3442  SeeAlso     []
3443
3444******************************************************************************/
3445array_t *
3446ImgLinearMakeSmoothVarBdd(Relation_t *head, bdd_t **smoothCubeArr)
3447{
3448array_t *smoothVarBddArray;
3449array_t *smoothArray;
3450VarLife_t **varArray;
3451int i, j, id;
3452VarLife_t *var;
3453bdd_t *varBdd, *cube, *newCube;
3454
3455  smoothVarBddArray = array_alloc(array_t *, 0);
3456  for(i=0; i<=head->nSize; i++) {
3457    smoothArray = array_alloc(bdd_t *, 0);
3458    array_insert_last(array_t *, smoothVarBddArray, smoothArray);
3459  } 
3460
3461  varArray = head->varArray;
3462  for(i=0; i<head->nVarArray; i++) {
3463    var = varArray[i];
3464    if(var->stateVar == 2)      continue;
3465    smoothArray = array_fetch(array_t *, smoothVarBddArray, var->to+1);
3466    varBdd = bdd_get_variable(head->mgr, var->id);
3467    array_insert_last(bdd_t *, smoothArray, varBdd);
3468  }
3469
3470  smoothArray = array_fetch(array_t *, smoothVarBddArray, 0);
3471  for(i=0; i<head->nDomain; i++) {
3472    id = head->domainVars[i];
3473    var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0;
3474   if(var)      continue;
3475    varBdd = bdd_get_variable(head->mgr, id);
3476    array_insert_last(bdd_t *, smoothArray, varBdd);
3477  }
3478
3479  if(smoothCubeArr) {
3480    for(i=0; i<=head->nSize; i++) {
3481      smoothArray = array_fetch(array_t *, smoothVarBddArray, i);
3482      cube = bdd_one(head->mgr);
3483      for(j=0; j<array_n(smoothArray); j++) {
3484        varBdd = array_fetch(bdd_t *, smoothArray, j);
3485        newCube = bdd_and(varBdd, cube, 1, 1);
3486        bdd_free(cube);
3487        cube = newCube;
3488      }
3489      smoothCubeArr[i] = cube;
3490    }
3491  }
3492
3493  return(smoothVarBddArray);
3494}
3495
3496/**Function********************************************************************
3497
3498  Synopsis    [Priority function for clutering]
3499
3500  Description [Priority function for clutering]
3501
3502  SideEffects []
3503
3504  SeeAlso     []
3505
3506******************************************************************************/
3507static int
3508ImgLinearCompareVarEffFromSmall(const void *c1, const void *c2)
3509{
3510VarLife_t *con1, *con2;
3511
3512  con1 = *(VarLife_t **)c1;
3513  con2 = *(VarLife_t **)c2;
3514  return(con1->effFrom > con2->effFrom);
3515}
3516
3517/**Function********************************************************************
3518
3519  Synopsis    [Priority function for clutering]
3520
3521  Description [Priority function for clutering]
3522
3523  SideEffects []
3524
3525  SeeAlso     []
3526
3527******************************************************************************/
3528static int
3529ImgLinearCompareVarDummyLarge(const void *c1, const void *c2)
3530{
3531VarLife_t *con1, *con2;
3532
3533  con1 = *(VarLife_t **)c1;
3534  con2 = *(VarLife_t **)c2;
3535  return(con1->dummy < con2->dummy);
3536}
3537
3538/**Function********************************************************************
3539
3540  Synopsis    [Priority function for clutering]
3541
3542  Description [Priority function for clutering]
3543
3544  SideEffects []
3545
3546  SeeAlso     []
3547
3548******************************************************************************/
3549static int
3550ImgLinearCompareVarEffFromLarge(const void *c1, const void *c2)
3551{
3552VarLife_t *con1, *con2;
3553
3554  con1 = *(VarLife_t **)c1;
3555  con2 = *(VarLife_t **)c2;
3556  return(con1->effFrom < con2->effFrom);
3557}
3558
3559/**Function********************************************************************
3560
3561  Synopsis    [Priority function for clutering]
3562
3563  Description [Priority function for clutering]
3564
3565  SideEffects []
3566
3567  SeeAlso     []
3568
3569******************************************************************************/
3570static int
3571ImgLinearCompareVarId(const void *c1, const void *c2)
3572{
3573VarLife_t *con1, *con2;
3574
3575  con1 = *(VarLife_t **)c1;
3576  con2 = *(VarLife_t **)c2;
3577  return(con1->id < con2->id);
3578}
3579
3580/**Function********************************************************************
3581
3582  Synopsis    [Priority function for clutering]
3583
3584  Description [Priority function for clutering]
3585
3586  SideEffects []
3587
3588  SeeAlso     []
3589
3590******************************************************************************/
3591static int
3592ImgLinearCompareVarSize(const void *c1, const void *c2)
3593{
3594VarLife_t *con1, *con2;
3595
3596  con1 = *(VarLife_t **)c1;
3597  con2 = *(VarLife_t **)c2;
3598  return(con1->nSize > con2->nSize);
3599}
3600
3601/**Function********************************************************************
3602
3603  Synopsis    [Priority function for clutering]
3604
3605  Description [Priority function for clutering]
3606
3607  SideEffects []
3608
3609  SeeAlso     []
3610
3611******************************************************************************/
3612static int
3613ImgLinearCompareConjunctRangeMinusDomain(const void *c1, const void *c2)
3614{
3615Conjunct_t *con1, *con2;
3616
3617  con1 = *(Conjunct_t **)c1;
3618  con2 = *(Conjunct_t **)c2;
3619  return(con1->nRange-con1->nDomain > con2->nRange-con2->nDomain);
3620}
3621
3622/**Function********************************************************************
3623
3624  Synopsis    [Priority function for clutering]
3625
3626  Description [Priority function for clutering]
3627
3628  SideEffects []
3629
3630  SeeAlso     []
3631
3632******************************************************************************/
3633static int
3634ImgLinearCompareConjunctDummy(const void *c1, const void *c2)
3635{
3636Conjunct_t *con1, *con2;
3637
3638  con1 = *(Conjunct_t **)c1;
3639  con2 = *(Conjunct_t **)c2;
3640  return(con1->dummy > con2->dummy); 
3641}
3642
3643/**Function********************************************************************
3644
3645  Synopsis    [Priority function for clutering]
3646
3647  Description [Priority function for clutering]
3648
3649  SideEffects []
3650
3651  SeeAlso     []
3652
3653******************************************************************************/
3654static int
3655ImgLinearCompareConjunctIndex(const void *c1, const void *c2)
3656{
3657Conjunct_t *con1, *con2;
3658
3659  con1 = *(Conjunct_t **)c1;
3660  con2 = *(Conjunct_t **)c2;
3661
3662  return(con1->index > con2->index); 
3663}
3664
3665/**Function********************************************************************
3666
3667  Synopsis    [Priority function for clutering]
3668
3669  Description [Priority function for clutering]
3670
3671  SideEffects []
3672
3673  SeeAlso     []
3674
3675******************************************************************************/
3676static int
3677ImgLinearCompareConjunctSize(const void *c1, const void *c2)
3678{
3679Conjunct_t *con1, *con2;
3680
3681  con1 = *(Conjunct_t **)c1;
3682  con2 = *(Conjunct_t **)c2;
3683
3684  if(con1->nSize == con2->nSize)
3685    return(con1->dummy < con2->dummy);
3686  return(con1->nSize < con2->nSize); 
3687}
3688
3689/**Function********************************************************************
3690
3691  Synopsis    [Priority function for clutering]
3692
3693  Description [Priority function for clutering]
3694
3695  SideEffects []
3696
3697  SeeAlso     []
3698
3699******************************************************************************/
3700static int
3701ImgLinearCompareVarIndex(const void *c1, const void *c2)
3702{
3703VarLife_t *v1, *v2;
3704
3705  v1 = *(VarLife_t **)c1;
3706  v2 = *(VarLife_t **)c2;
3707
3708  return(v1->index < v2->index); 
3709}
3710
3711/**Function********************************************************************
3712
3713  Synopsis    [Priority function for clutering]
3714
3715  Description [Priority function for clutering]
3716
3717  SideEffects []
3718
3719  SeeAlso     []
3720
3721******************************************************************************/
3722static int
3723ImgLinearCompareDeadAffinityLive(const void *c1, const void *c2)
3724{
3725Cluster_t *clu1, *clu2;
3726
3727  clu1 = *(Cluster_t **)c1;
3728  clu2 = *(Cluster_t **)c2;
3729  if(clu1->nDead == clu2->nDead) {
3730    if(clu1->nAffinity == clu2->nAffinity) {
3731      return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); 
3732    }
3733    return(clu1->nAffinity < clu2->nAffinity); 
3734  }
3735  return(clu1->nDead < clu2->nDead); 
3736}
3737
3738/**Function********************************************************************
3739
3740  Synopsis    [Priority function for clutering]
3741
3742  Description [Priority function for clutering]
3743
3744  SideEffects []
3745
3746  SeeAlso     []
3747
3748******************************************************************************/
3749static int
3750ImgLinearCompareDeadLiveAffinity(const void *c1, const void *c2)
3751{
3752Cluster_t *clu1, *clu2;
3753
3754  clu1 = *(Cluster_t **)c1;
3755  clu2 = *(Cluster_t **)c2;
3756  if(clu1->nDead == clu2->nDead) {
3757    if(clu1->nVar-clu1->nDead == clu2->nVar-clu2->nDead) {
3758      return(clu1->nAffinity < clu2->nAffinity); 
3759    }
3760    return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); 
3761  }
3762  return(clu1->nDead < clu2->nDead); 
3763}
3764
3765/**Function********************************************************************
3766
3767  Synopsis    [Priority function for clutering]
3768
3769  Description [Priority function for clutering]
3770
3771  SideEffects []
3772
3773  SeeAlso     []
3774
3775******************************************************************************/
3776static int
3777ImgLinearCompareAffinityDeadLive(const void *c1, const void *c2)
3778{
3779Cluster_t *clu1, *clu2;
3780
3781  clu1 = *(Cluster_t **)c1;
3782  clu2 = *(Cluster_t **)c2;
3783  if(clu1->nAffinity == clu2->nAffinity) {
3784    if(clu1->nDead == clu2->nDead) {
3785      return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); 
3786    }
3787    return(clu1->nDead < clu2->nDead); 
3788  }
3789  return(clu1->nAffinity < clu2->nAffinity); 
3790}
3791
3792/**Function********************************************************************
3793
3794  Synopsis    [Priority function for clutering]
3795
3796  Description [Priority function for clutering]
3797
3798  SideEffects []
3799
3800  SeeAlso     []
3801
3802******************************************************************************/
3803static int
3804ImgLinearCompareLiveAffinityDead(const void *c1, const void *c2)
3805{
3806Cluster_t *clu1, *clu2;
3807
3808  clu1 = *(Cluster_t **)c1;
3809  clu2 = *(Cluster_t **)c2;
3810  if(clu1->nVar-clu1->nDead == clu2->nVar-clu2->nDead) {
3811    if(clu1->nAffinity == clu2->nAffinity) {
3812      return(clu1->nDead < clu2->nDead);
3813    }
3814    return(clu1->nAffinity < clu2->nAffinity);
3815  }
3816  return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead);
3817}
3818
3819/**Function********************************************************************
3820
3821  Synopsis    [Priority function for clutering]
3822
3823  Description [Priority function for clutering]
3824
3825  SideEffects []
3826
3827  SeeAlso     []
3828
3829******************************************************************************/
3830static int
3831ImgLinearHeapCompareDeadAffinityLive(const void *c1, const void *c2)
3832{
3833Cluster_t *clu1, *clu2;
3834
3835  clu1 = (Cluster_t *)c1;
3836  clu2 = (Cluster_t *)c2;
3837  if(clu1->nDead == clu2->nDead) {
3838    if(clu1->nAffinity == clu2->nAffinity) {
3839      return((clu1->nVar-clu1->nDead) > (clu2->nVar-clu2->nDead)); 
3840    }
3841    return(clu1->nAffinity < clu2->nAffinity); 
3842  }
3843  return(clu1->nDead < clu2->nDead); 
3844}
3845
3846/**Function********************************************************************
3847
3848  Synopsis    [Priority function for clutering]
3849
3850  Description [Priority function for clutering]
3851
3852  SideEffects []
3853
3854  SeeAlso     []
3855
3856******************************************************************************/
3857static int
3858ImgLinearHeapCompareDeadLiveAffinity(const void *c1, const void *c2)
3859{
3860Cluster_t *clu1, *clu2;
3861
3862  clu1 = (Cluster_t *)c1;
3863  clu2 = (Cluster_t *)c2;
3864  if(clu1->nDead == clu2->nDead) {
3865    if((clu1->nVar-clu1->nDead) == (clu2->nVar-clu2->nDead)) {
3866      return(clu1->nAffinity < clu2->nAffinity); 
3867    }
3868    return((clu1->nVar-clu1->nDead) > (clu2->nVar-clu2->nDead)); 
3869  }
3870  return(clu1->nDead < clu2->nDead); 
3871}
3872
3873/**Function********************************************************************
3874
3875  Synopsis    [Priority function for clutering]
3876
3877  Description [Priority function for clutering]
3878
3879  SideEffects []
3880
3881  SeeAlso     []
3882
3883******************************************************************************/
3884static int
3885ImgLinearHeapCompareAffinityDeadLive(const void *c1, const void *c2)
3886{
3887Cluster_t *clu1, *clu2;
3888
3889  clu1 = (Cluster_t *)c1;
3890  clu2 = (Cluster_t *)c2;
3891  if(clu1->nAffinity == clu2->nAffinity) {
3892    if(clu1->nDead == clu2->nDead) {
3893      return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); 
3894    }
3895    return(clu1->nDead < clu2->nDead); 
3896  }
3897  return(clu1->nAffinity < clu2->nAffinity); 
3898}
3899
3900/**Function********************************************************************
3901
3902  Synopsis    [Priority function for clutering]
3903
3904  Description [Priority function for clutering]
3905
3906  SideEffects []
3907
3908  SeeAlso     []
3909
3910******************************************************************************/
3911static int
3912ImgLinearHeapCompareLiveAffinityDead(const void *c1, const void *c2)
3913{
3914Cluster_t *clu1, *clu2;
3915
3916  clu1 = (Cluster_t *)c1;
3917  clu2 = (Cluster_t *)c2;
3918  if(clu1->nVar-clu1->nDead == clu2->nVar-clu2->nDead) {
3919    if(clu1->nAffinity == clu2->nAffinity) {
3920      return(clu1->nDead < clu2->nDead);
3921    }
3922    return(clu1->nAffinity < clu2->nAffinity);
3923  }
3924  return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead);
3925}
3926
3927/**Function********************************************************************
3928
3929  Synopsis    [Initialize variable array]
3930
3931  Description [Initialize variable array]
3932
3933  SideEffects []
3934
3935  SeeAlso     []
3936
3937******************************************************************************/
3938static void
3939ImgLinearVariableArrayInit(Relation_t *head)
3940{
3941mdd_manager *mgr;
3942Conjunct_t **conjunctArray, *conjunct;
3943Conjunct_t *tConjunct;
3944bdd_t *relation, *bddOne;
3945VarLife_t **varArray;
3946int *supList, listSize;
3947int *varType, *varArrayMap;
3948int i, j, k, id, nVarArray;
3949int nSize, newNum;
3950
3951
3952  if(head->bRefineVarArray) {
3953    ImgLinearVariableArrayQuit(head);
3954  }
3955
3956  if(head->varArray)    return;
3957
3958  mgr = head->mgr;
3959
3960  if(head->nVar != (int)(bdd_num_vars(mgr))) {
3961    newNum = bdd_num_vars(head->mgr);
3962    head->domain2range = REALLOC(int, head->domain2range, newNum);
3963    head->range2domain = REALLOC(int, head->range2domain, newNum);
3964    head->varType = REALLOC(int, head->varType, newNum);
3965    head->varArrayMap = REALLOC(int, head->varArrayMap, newNum);
3966    head->constantCase = REALLOC(bdd_t *, head->constantCase, newNum);
3967    head->quantifyVars = REALLOC(int, head->quantifyVars, newNum);
3968
3969    for(i=head->nVar; i<newNum; i++) {
3970      head->domain2range[i] = -1;
3971      head->range2domain[i] = -1;
3972      head->varType[i] = 0;
3973      head->varArrayMap[i] = -1;
3974      head->constantCase[i] = 0;
3975      head->quantifyVars[i] = 0;
3976    }
3977    head->nVar = bdd_num_vars(head->mgr);
3978  }
3979
3980  nSize = head->nSize;
3981  conjunctArray = head->conjunctArray;
3982  varArrayMap = head->varArrayMap;
3983
3984  id = 0;
3985  nVarArray = 0;
3986  varArray = ALLOC(VarLife_t *, nVarArray+1);
3987  head->varArray = varArray;
3988  head->nVarArray = nVarArray;
3989  bddOne = bdd_one(head->mgr);
3990
3991  varType = head->varType;
3992  for(i=0; i<nSize; i++) {
3993    conjunct = conjunctArray[i];
3994    if(conjunct == 0)   continue;
3995    relation = conjunct->relation;
3996    if(relation == 0)   continue;
3997    if(bdd_equal(bddOne, relation))     continue;
3998    supList = conjunct->supList;
3999    listSize = conjunct->nSize;
4000    for(j=0; j<listSize; j++) {
4001      id = supList[j]; 
4002      ImgLinearUpdateVariableArrayWithId(head, i, id);
4003    }
4004
4005    for(k=0; k<conjunct->nCluster; k++) {
4006      tConjunct = conjunct->clusterArray[k];
4007      supList = tConjunct->supList;
4008      listSize = tConjunct->nSize;
4009      for(j=0; j<listSize; j++) {
4010        ImgLinearUpdateVariableArrayWithId(head, i, id);
4011      }
4012    }
4013  }
4014  bdd_free(bddOne);
4015  head->bRefineVarArray = 0;
4016}
4017
4018/**Function********************************************************************
4019
4020  Synopsis    [Update variable array with id of variable id]
4021
4022  Description [Update variable array with id of variable id]
4023
4024  SideEffects []
4025
4026  SeeAlso     []
4027
4028******************************************************************************/
4029static void
4030ImgLinearUpdateVariableArrayWithId(Relation_t *head, 
4031                                   int cindex, 
4032                                   int id)
4033{
4034VarLife_t *var;
4035int *varType;
4036int *varArrayMap;
4037int nVarArray;
4038VarLife_t **varArray;
4039
4040  varType = head->varType;
4041  varArrayMap = head->varArrayMap;
4042  varArray = head->varArray;
4043  nVarArray = head->nVarArray;
4044
4045  if(varArrayMap[id] == -1) {
4046    var = ALLOC(VarLife_t, 1);
4047    var->id = id;
4048    var->from = cindex;
4049    var->to = cindex;
4050    var->effFrom = cindex;
4051    var->effTo = cindex;
4052    var->stateVar = 0;
4053    var->relArr = ALLOC(int, 1);
4054    var->nSize = 0;
4055    var->index = 0.0;
4056    varArrayMap[id] = nVarArray;
4057    varArray[nVarArray++] = var;
4058    varArray = REALLOC(VarLife_t *, varArray, nVarArray+1);
4059
4060    if(varType[id] == 1) {
4061      var->stateVar = 1;
4062      if(head->includeCS && !head->quantifyCS) { 
4063        var->relArr = REALLOC(int, var->relArr, var->nSize+1);
4064        var->relArr[var->nSize++] = MAXINT-1;
4065        var->from = -1;
4066      }
4067    }
4068    else if(varType[id] == 2) {
4069      var->stateVar = 2;
4070      if(head->includeNS) { 
4071        var->relArr = REALLOC(int, var->relArr, var->nSize+1);
4072        var->relArr[var->nSize++] = MAXINT;
4073        var->to = head->nSize;
4074      }
4075    }
4076  }
4077  else {
4078    var = varArray[varArrayMap[id]];
4079  }
4080 
4081  if(var->to < cindex)          var->to = cindex;
4082  if(var->from > cindex)        var->from = cindex;
4083
4084  if(var->effTo < cindex)       var->effTo = cindex;
4085  if(var->effFrom > cindex)     var->effFrom = cindex;
4086
4087  var->relArr = REALLOC(int, var->relArr, var->nSize+1);
4088  var->relArr[var->nSize++] = cindex;
4089  head->varArray = varArray;
4090  head->nVarArray = nVarArray;
4091}
4092/**Function********************************************************************
4093
4094  Synopsis    [Apply quantification with candidate variables]
4095
4096  Description [Apply quantification with candidate variables]
4097
4098  SideEffects []
4099
4100  SeeAlso     []
4101
4102******************************************************************************/
4103static int
4104ImgLinearQuantifyVariablesFromConjunct(Relation_t *head,
4105                                       Conjunct_t *conjunct, 
4106                                       array_t *smoothVarBddArray,
4107                                       int *bModified)
4108{
4109bdd_t *relation, *simpleRelation;
4110
4111  if(conjunct == 0)     return 1;
4112  relation = conjunct->relation;
4113  if(relation == 0)     return 1;
4114
4115  simpleRelation = bdd_smooth(relation, smoothVarBddArray);
4116  if(bdd_equal(relation, simpleRelation)) {
4117    bdd_free(simpleRelation);
4118    return 0;
4119  }
4120  bdd_free(relation);
4121
4122  (*bModified)++;
4123  conjunct->relation = simpleRelation;
4124  conjunct->bModified = 1;
4125  head->bModified = 1;
4126  head->bRefineVarArray = 1;
4127  ImgLinearConjunctRefine(head, conjunct);
4128  return 1;
4129}
4130
4131/**Function********************************************************************
4132
4133  Synopsis    [Refine conjunction array to fill the empty slot.]
4134
4135  Description [Refine conjunction array to fill the empty slot.]
4136
4137  SideEffects []
4138
4139  SeeAlso     []
4140
4141******************************************************************************/
4142static void
4143ImgLinearConjunctRefine(Relation_t *head, Conjunct_t *conjunct)
4144{
4145int i, id, listSize, *supList;
4146int *varType;
4147
4148  if(conjunct->relation == 0)   {
4149    if(conjunct->supList)       free(conjunct->supList);
4150    conjunct->supList = 0;
4151    return;
4152  }
4153  if(!conjunct->bModified)      return; 
4154
4155  if(conjunct->supList) {
4156    free(conjunct->supList);
4157    conjunct->supList = 0;
4158  }
4159
4160  supList = ImgLinearGetSupportBddId(head->mgr, conjunct->relation, &listSize);
4161  if(listSize == 0) {
4162    conjunct->relation = 0;
4163    if(conjunct->supList) {
4164      free(conjunct->supList);
4165      conjunct->supList = 0;
4166    }
4167    return;
4168  }
4169  else {
4170    varType = head->varType;
4171    conjunct->supList = supList;
4172    conjunct->nSize = listSize;
4173    conjunct->bModified = 0;
4174    conjunct->nDomain = 0;
4175    conjunct->nRange = 0;
4176    conjunct->nQuantify = 0;
4177    conjunct->from = 0;
4178    conjunct->to = 0;
4179    conjunct->dummy = 0;
4180    for(i=0; i<listSize; i++) {
4181      id = supList[i];
4182      if(varType[id] == 1)      conjunct->nDomain++;
4183      else if(varType[id] == 2) conjunct->nRange++;
4184      else if(varType[id] == 3) conjunct->nQuantify++;
4185    }
4186    head->bModified = 1;
4187  }
4188  return;
4189}
4190/**Function********************************************************************
4191
4192  Synopsis    [Refine conjunction array to fill the empty slot.]
4193
4194  Description [Refine conjunction array to fill the empty slot.]
4195
4196  SideEffects []
4197
4198  SeeAlso     []
4199
4200******************************************************************************/
4201static void
4202ImgLinearConjunctArrayRefine(Relation_t *head)
4203{
4204int nSize, i;
4205int index;
4206Conjunct_t **conjunctArray, **newConjunctArray;
4207Conjunct_t *conjunct;
4208
4209  if(head->bModified == 0)      return;
4210
4211  conjunctArray = head->conjunctArray;
4212  newConjunctArray = ALLOC(Conjunct_t *, head->nSize+1);
4213  nSize = head->nSize;
4214  for(index=0, i=0; i<nSize; i++) {
4215    conjunct = conjunctArray[i];
4216    if(conjunct == 0)   {
4217      head->bRefineVarArray = 1;
4218      continue;
4219    }
4220    if(conjunct->relation == 0) {
4221      ImgLinearConjunctQuit(conjunct);
4222      head->bRefineVarArray = 1;
4223      continue;
4224    }
4225
4226    if(conjunct->bModified) {
4227      ImgLinearConjunctRefine(head, conjunct);
4228      head->bRefineVarArray = 1;
4229    }
4230
4231    if(conjunct == 0)   continue;
4232    if(conjunct->relation == 0) {
4233      ImgLinearConjunctQuit(conjunct);
4234      continue;
4235    }
4236
4237    newConjunctArray[index] = conjunct;
4238    conjunct->index = index++;
4239  }
4240  newConjunctArray[index] = 0;
4241  free(conjunctArray);
4242  head->conjunctArray = newConjunctArray;
4243  head->nSize = index;
4244  head->bModified = 0;
4245  return; 
4246}
4247
4248/**Function********************************************************************
4249
4250  Synopsis    [Get the number of state variables after applying optimization]
4251
4252  Description [Get the number of state variables after applying optimization]
4253
4254  SideEffects []
4255
4256  SeeAlso     []
4257
4258******************************************************************************/
4259static void
4260ImgLinearSetEffectiveNumberOfStateVariable(Relation_t *head, 
4261                                            int *rangeId, 
4262                                            int *domainId,
4263                                            int *existStateVariable) 
4264{
4265VarLife_t **varArray, *var;
4266int *varType;
4267int nRange, nDomain, nQuantify;
4268int i;
4269
4270  varArray = head->varArray;
4271  varType = head->varType;
4272  nRange = nDomain = nQuantify = 0;
4273
4274  for(i=0; i<head->nVarArray; i++) {
4275    var = varArray[i];
4276    if(varType[var->id] == 1)   {
4277      if(domainId) domainId[nDomain] = var->id;
4278      nDomain++;
4279      if(existStateVariable) existStateVariable[var->id] = 1;
4280    }
4281    else if(varType[var->id] == 2)      {
4282      if(rangeId) rangeId[nRange] = var->id;
4283      nRange++;
4284      if(existStateVariable) existStateVariable[var->id] = 1;
4285    }
4286    else if(varType[var->id] == 3)      {
4287      nQuantify++;
4288    }
4289    else
4290      nQuantify++;
4291
4292  } 
4293  if(domainId)  domainId[nDomain] = -1;
4294  if(rangeId)   rangeId[nRange] = -1;
4295
4296  head->nEffRange = nRange;
4297  head->nEffDomain = nDomain;
4298  head->nEffQuantify = nQuantify;
4299
4300  if(head->nInitRange == 0 && head->nInitDomain == 0 && head->nInitQuantify == 0) {
4301    head->nInitRange = nRange;
4302    head->nInitDomain = nDomain;
4303    head->nInitQuantify = nQuantify;
4304  }
4305}
4306
4307/**Function********************************************************************
4308
4309  Synopsis    [Find the case that the relation contains only one next state varaible]
4310
4311  Description [Find the case that the relation contains only one next state varaible]
4312
4313  SideEffects []
4314
4315  SeeAlso     []
4316
4317******************************************************************************/
4318static void
4319ImgLinearAddSingletonCase(Relation_t *head)
4320{
4321Conjunct_t **newConjunctArray;
4322Conjunct_t **singletonArray;
4323Conjunct_t *conjunct;
4324int i, j, index;
4325int nSingletonArray;
4326int putFlag;
4327
4328  nSingletonArray = head->nSingletonArray;
4329  singletonArray = head->singletonArray;
4330
4331  if(nSingletonArray == 0)      return;
4332  fprintf(stdout, "NOTICE : %d singleton case will be added\n", nSingletonArray);
4333
4334  qsort(singletonArray, nSingletonArray, sizeof(Conjunct_t *), ImgLinearCompareConjunctRangeMinusDomain);
4335
4336  index = 0;
4337  newConjunctArray = ALLOC(Conjunct_t *, head->nSize + nSingletonArray);
4338  putFlag = 0;
4339  for(i=0; i<nSingletonArray; i++) {
4340    conjunct = singletonArray[i];
4341    if(putFlag == 0 && conjunct->nRange > conjunct->nSize-conjunct->nRange) {
4342      putFlag = 1;
4343      for(j=0; j<head->nSize; j++) 
4344        newConjunctArray[index++] = head->conjunctArray[j];
4345    }
4346    newConjunctArray[index++] = singletonArray[i];
4347  }
4348  if(putFlag == 0) {
4349    for(j=0; j<head->nSize; j++) 
4350      newConjunctArray[index++] = head->conjunctArray[j];
4351  }
4352
4353  head->nSize = index;
4354  head->bModified = 1;
4355  head->bRefineVarArray = 1;
4356  free(head->conjunctArray);
4357  head->conjunctArray = newConjunctArray;
4358  free(singletonArray);
4359  head->singletonArray = 0;
4360  head->nSingletonArray = 0;
4361}
4362
4363
4364/**Function********************************************************************
4365
4366  Synopsis    [Find transtion relations that have smae support set]
4367
4368  Description [Find transtion relations that have smae support set and use this information when finding linear arragement]
4369
4370  SideEffects []
4371
4372  SeeAlso     []
4373
4374******************************************************************************/
4375static void
4376ImgLinearExpandSameSupportSet(Relation_t *head)
4377{
4378int index, i, j;
4379Conjunct_t **newConjunctArray;
4380Conjunct_t *conjunct;
4381
4382  newConjunctArray = ALLOC(Conjunct_t *, head->nSize);
4383  for(index=0, i=0; i<head->nSize; i++) {
4384    if(index >= head->nSize)
4385      newConjunctArray = REALLOC(Conjunct_t *, newConjunctArray, index+1);
4386    conjunct = head->conjunctArray[i];
4387    newConjunctArray[index++] = conjunct;
4388    if(conjunct->nCluster) {
4389      for(j=0; j<conjunct->nCluster; j++) {
4390        if(index >= head->nSize)
4391          newConjunctArray = REALLOC(Conjunct_t *, newConjunctArray, index+1);
4392        newConjunctArray[index++] = conjunct->clusterArray[j];
4393      }
4394      head->bModified = 1;
4395      head->bRefineVarArray = 1;
4396      conjunct->nCluster = 0;
4397      if(conjunct->clusterArray) {
4398        free(conjunct->clusterArray);
4399        conjunct->clusterArray = 0;
4400      }
4401    }
4402  }
4403  free(head->conjunctArray);
4404  head->conjunctArray = newConjunctArray;
4405  head->nSize = index;
4406}
4407
4408
4409/**Function********************************************************************
4410
4411  Synopsis    [Cluster the relation that has same support set]
4412
4413  Description [Cluster the relation that has same support set]
4414
4415  SideEffects []
4416
4417  SeeAlso     []
4418
4419******************************************************************************/
4420static void
4421ImgLinearClusterSameSupportSet(Relation_t *head) 
4422{
4423int i, j, index, id;
4424int *supList;
4425Conjunct_t *conjunct, *base;
4426int *varType;
4427Conjunct_t **conjunctArray, **newConjunctArray;
4428
4429  head->nTotalCluster = 0;
4430  varType = head->varType;
4431  conjunctArray = head->conjunctArray; 
4432
4433  for(i=0; i<head->nSize; i++) {
4434    conjunct = head->conjunctArray[i];
4435    supList = conjunct->supList;
4436    conjunct->dummy = 0;
4437    for(j=0; j<conjunct->nSize; j++) {
4438      id = supList[j];
4439      if(varType[id] == 2)      continue;
4440      conjunct->dummy += id;
4441    }
4442    conjunct->dummy *= (conjunct->nSize-conjunct->nRange);
4443    conjunct->dummy -= conjunct->nDomain;
4444  }
4445  qsort(conjunctArray, head->nSize, sizeof(Conjunct_t *), 
4446                        ImgLinearCompareConjunctDummy);
4447
4448  for(i=0; i<head->nSize; i++) {
4449    base = head->conjunctArray[i];
4450    for(j=i+1; j<head->nSize; j++) {
4451      conjunct = head->conjunctArray[j];
4452      if(base->dummy != conjunct->dummy) {
4453        if(j == i+1)    break;
4454        ImgLinearFindSameSupportConjuncts(head, i, j-1);
4455        i = j-1;
4456        break;
4457      }
4458    }
4459  }
4460
4461  if(head->bModified)   {
4462    conjunctArray = head->conjunctArray;
4463    newConjunctArray = ALLOC(Conjunct_t *, head->nSize);
4464    for(index=0, i=0; i<head->nSize; i++) {
4465      conjunct = conjunctArray[i];
4466      if(conjunct == 0) continue;
4467      newConjunctArray[index++] = conjunct;
4468    }
4469    free(conjunctArray);
4470    head->conjunctArray = newConjunctArray;
4471    head->nSize = index;
4472    head->bModified = 1;
4473    head->bRefineVarArray = 1;
4474  }
4475
4476  conjunctArray = head->conjunctArray;
4477  qsort(conjunctArray, head->nSize, sizeof(Conjunct_t *), ImgLinearCompareConjunctIndex);
4478  if(head->bModified)   {
4479    conjunctArray = head->conjunctArray;
4480    for(i=0; i<head->nSize; i++) {
4481      conjunct = conjunctArray[i];
4482      if(conjunct == 0) continue;
4483      conjunct->index = i;
4484    }
4485  }
4486  fprintf(stdout, "NOTICE : %d conjunct clustered\n", head->nTotalCluster);
4487  head->nTotalCluster = 0;
4488
4489}
4490/**Function********************************************************************
4491
4492  Synopsis    [Find the conjuncts that have same support variables.]
4493
4494  Description [Find the conjuncts that have same support variables.]
4495
4496  SideEffects []
4497
4498  SeeAlso     []
4499
4500******************************************************************************/
4501static void
4502ImgLinearFindSameSupportConjuncts(Relation_t *head, int from, int to)
4503{
4504Conjunct_t *con1, *con2;
4505int i, j;
4506
4507  for(i=from; i<=to; i++) {
4508    con1 = head->conjunctArray[i];
4509    if(con1 == 0)       continue;
4510
4511    for(j=from; j<=to; j++) {
4512      if(i == j)        continue;
4513      con2 = head->conjunctArray[j];
4514      if(con2 == 0)     continue;
4515      if(ImgLinearIsSameConjunct(head, con1, con2)) {
4516        ImgLinearAddConjunctIntoClusterArray(con1, con2);
4517        head->conjunctArray[j] = 0;
4518
4519        head->bModified = 1;
4520        head->bRefineVarArray = 1;
4521        head->nTotalCluster++;
4522      }
4523    }
4524  }
4525}
4526
4527/**Function********************************************************************
4528
4529  Synopsis    [Check if given conjuncts have same support variables]
4530
4531  Description [Check if given conjuncts have same support variables]
4532
4533  SideEffects []
4534
4535  SeeAlso     []
4536
4537******************************************************************************/
4538static int
4539ImgLinearIsSameConjunct(Relation_t *head, Conjunct_t *con1, Conjunct_t *con2)
4540{
4541int i, j;
4542int *sup1, *sup2;
4543int id1, id2;
4544int *varType;
4545
4546  if(con1->nDomain != con2->nDomain)    return(0);
4547  if(con1->nSize-con1->nRange != con2->nSize-con2->nRange)      return(0);
4548  sup1 = con1->supList;
4549  sup2 = con2->supList;
4550
4551  varType = head->varType;
4552
4553  for(j=0, i=0; i<con1->nSize; i++) {
4554    id1 = sup1[i];
4555    if(varType[id1] == 2)continue;
4556    while(1) {
4557      id2 = sup2[j];
4558      if(varType[id2] == 2) {
4559        j++;
4560        continue;
4561      }
4562      if(id1 != id2)    return(0);
4563      j++;
4564      break;
4565    }
4566  }
4567  return(1);
4568}
4569
4570/**Function********************************************************************
4571
4572  Synopsis    [Add conjunct into array]
4573
4574  Description [Add conjunct into array]
4575
4576  SideEffects []
4577
4578  SeeAlso     []
4579
4580******************************************************************************/
4581static Conjunct_t **
4582ImgLinearAddConjunctIntoArray(Conjunct_t **array, int *nArray, Conjunct_t *con)
4583{
4584  if(array)
4585    array = REALLOC(Conjunct_t *, array, (*nArray)+1);
4586  else 
4587    array = ALLOC(Conjunct_t *, (*nArray)+1);
4588  array[(*nArray)++] = con;
4589  return(array);
4590
4591}
4592
4593/**Function********************************************************************
4594
4595  Synopsis    [Free conjunct_t data structure]
4596
4597  Description [Free conjunct_t data structure]
4598
4599  SideEffects []
4600
4601  SeeAlso     []
4602
4603******************************************************************************/
4604static void
4605ImgLinearConjunctQuit(Conjunct_t *conjunct)
4606{
4607  if(conjunct->supList) {
4608    free(conjunct->supList);
4609    conjunct->supList = 0;
4610  }
4611  if(conjunct->relation) {
4612    bdd_free(conjunct->relation);
4613    conjunct->relation = 0;
4614  }
4615  free(conjunct);
4616}
4617
4618
4619/**Function********************************************************************
4620
4621  Synopsis    [Free variable array]
4622
4623  Description [Free variable array]
4624
4625  SideEffects []
4626
4627  SeeAlso     []
4628
4629******************************************************************************/
4630static void
4631ImgLinearVariableArrayQuit(Relation_t *head)
4632{
4633int i;
4634VarLife_t **varArray;
4635
4636
4637  varArray = head->varArray;
4638  for(i=0; i<head->nVarArray; i++)
4639    ImgLinearVariableLifeQuit(varArray[i]);
4640
4641  free(varArray);
4642  head->varArray = 0;
4643  head->nVarArray = 0;
4644  memset(head->varArrayMap, -1, sizeof(int)*head->nVar);
4645}
4646
4647
4648/**Function********************************************************************
4649
4650  Synopsis    [Free variable life array]
4651
4652  Description [Free variable  lifearray]
4653
4654  SideEffects []
4655
4656  SeeAlso     []
4657
4658******************************************************************************/
4659static void
4660ImgLinearVariableLifeQuit(VarLife_t *var) 
4661{
4662   if(var->relArr)      free(var->relArr);
4663   free(var);
4664}
4665
4666/**Function********************************************************************
4667
4668  Synopsis    [Main function of clustering]
4669
4670  Description [Main function of clustering]
4671
4672  SideEffects []
4673
4674  SeeAlso     []
4675
4676******************************************************************************/
4677int
4678ImgLinearClustering(Relation_t *head, Img_OptimizeType optDir)
4679{
4680int andExistLimit;
4681int useFailureHistory;
4682int includeZeroGain;
4683double affinityLimit;
4684int bOptimize;
4685int varLimit;
4686
4687  bOptimize = 0;
4688
4689  affinityLimit = 0.99;
4690  andExistLimit = 10;
4691  varLimit = 200;
4692  fprintf(stdout, "Heap DAL affinity %3f, andExist %d\n", 
4693          affinityLimit, andExistLimit);
4694  bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit,
4695                                varLimit, optDir, 0,
4696                                ImgLinearHeapCompareDeadAffinityLive);
4697  ImgLinearRefineRelation(head);
4698  if(head->verbosity >= 5)
4699    ImgLinearPrintMatrix(head);
4700  ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
4701  ImgLinearPrintTransitionInfo(head);
4702
4703  includeZeroGain = 0;
4704  affinityLimit = 0.3;
4705  andExistLimit = 5000;
4706  varLimit = 50;
4707  useFailureHistory = 0;
4708  if(head->computeRange) {
4709    varLimit = 50;
4710    affinityLimit = 0.8;
4711    andExistLimit = 5000;
4712    fprintf(stdout, "Heap DAL affinity %3f, andExist %d\n", 
4713            affinityLimit, andExistLimit);
4714    bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit,
4715                                  varLimit, optDir, 0,
4716                                ImgLinearHeapCompareDeadAffinityLive);
4717
4718    ImgLinearRefineRelation(head);
4719    ImgLinearExtractNextStateCase(head);
4720    ImgLinearExtractSingletonCase(head);
4721    ImgLinearRefineRelation(head);
4722    ImgLinearAddSingletonCase(head);
4723    ImgLinearRefineRelation(head);
4724    ImgLinearAddNextStateCase(head);
4725    ImgLinearRefineRelation(head);
4726  }
4727  else 
4728  {
4729    fprintf(stdout, "Gain DAL affinity %3f, andExist %d\n", 
4730          affinityLimit, andExistLimit);
4731    bOptimize |= ImgLinearClusteringIteratively(head, affinityLimit,
4732                                andExistLimit, varLimit, 
4733                                includeZeroGain, useFailureHistory, optDir,
4734                                ImgLinearCompareDeadAffinityLive);
4735    ImgLinearRefineRelation(head);
4736    ImgLinearExtractNextStateCase(head);
4737    ImgLinearExtractSingletonCase(head);
4738    ImgLinearRefineRelation(head);
4739    ImgLinearAddSingletonCase(head);
4740    ImgLinearRefineRelation(head);
4741    ImgLinearAddNextStateCase(head);
4742    ImgLinearRefineRelation(head);
4743  }
4744
4745  includeZeroGain = 1;
4746  varLimit = 200;
4747  affinityLimit = 0.7;
4748  andExistLimit = 5000;
4749  fprintf(stdout, "Heap DAL affinity %3f, andExist %d\n", 
4750          affinityLimit, andExistLimit);
4751  bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit,
4752                                varLimit, optDir, 0,
4753                                ImgLinearHeapCompareDeadAffinityLive);
4754
4755  ImgLinearRefineRelation(head);
4756  ImgLinearExtractNextStateCase(head);
4757  ImgLinearExtractSingletonCase(head);
4758  ImgLinearRefineRelation(head);
4759  ImgLinearAddSingletonCase(head);
4760  ImgLinearRefineRelation(head);
4761  ImgLinearAddNextStateCase(head);
4762  ImgLinearRefineRelation(head);
4763
4764  if(head->verbosity >= 5)
4765    ImgLinearPrintMatrix(head);
4766  ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
4767  ImgLinearPrintTransitionInfo(head);
4768
4769  includeZeroGain = 1;
4770  affinityLimit = 0.4;
4771  andExistLimit = 5000;
4772  fprintf(stdout, "Heap DAL affinity %3f, andExist %d\n", 
4773          affinityLimit, andExistLimit);
4774  bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit,
4775                                varLimit, optDir, 0,
4776                                ImgLinearHeapCompareDeadAffinityLive);
4777  ImgLinearRefineRelation(head);
4778  ImgLinearExtractNextStateCase(head);
4779  ImgLinearExtractSingletonCase(head);
4780  ImgLinearRefineRelation(head);
4781  ImgLinearAddSingletonCase(head);
4782  ImgLinearRefineRelation(head);
4783  ImgLinearAddNextStateCase(head);
4784  ImgLinearRefineRelation(head);
4785
4786  if(head->verbosity >= 5)
4787    ImgLinearPrintMatrix(head);
4788  ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
4789  ImgLinearPrintTransitionInfo(head);
4790
4791  affinityLimit = 0.0;
4792  andExistLimit = 5000;
4793  fprintf(stdout, "Heap DLA affinity %3f, andExist %d\n", 
4794          affinityLimit, andExistLimit);
4795  bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit,
4796                                varLimit, optDir, 0,
4797                                ImgLinearHeapCompareDeadLiveAffinity);
4798  ImgLinearRefineRelation(head);
4799  ImgLinearExtractNextStateCase(head);
4800  ImgLinearRefineRelation(head);
4801  ImgLinearAddNextStateCase(head);
4802  ImgLinearRefineRelation(head);
4803  if(head->verbosity >= 5)
4804    ImgLinearPrintMatrix(head);
4805  ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
4806  ImgLinearPrintTransitionInfo(head);
4807
4808  if(head->computeRange) {
4809    includeZeroGain = 0;
4810    affinityLimit = 0.0;
4811    andExistLimit = andExistLimit;
4812    varLimit = MAXINT;
4813    head->bddLimit = head->bddLimit * 2;
4814    fprintf(stdout, "Heap DLA affinity %3f, andExist %d\n", 
4815          affinityLimit, andExistLimit);
4816    while(1) {
4817      bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit,
4818                                varLimit, optDir, 1,
4819                                ImgLinearHeapCompareDeadLiveAffinity);
4820      ImgLinearRefineRelation(head);
4821
4822      if(ImgCheckRangeTestAndOverapproximate(head))     break;
4823    }
4824
4825    ImgCountOnsetDisjunctiveArray(head);
4826    ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
4827    ImgLinearPrintTransitionInfo(head);
4828
4829  }
4830
4831  return(bOptimize);
4832}
4833
4834/**Function********************************************************************
4835
4836  Synopsis    [Count onset of relation array]
4837
4838  Description [Count onset of relation array]
4839
4840  SideEffects []
4841
4842  SeeAlso     []
4843
4844******************************************************************************/
4845static void 
4846ImgCountOnsetDisjunctiveArray(Relation_t *head)
4847{
4848EpDouble tepd;
4849char strValue[1024];
4850bdd_t *varBdd;
4851mdd_manager *mgr;
4852array_t *bddVarArray;
4853Conjunct_t *conjunct;
4854int count, i, j, id;
4855double onSet;
4856
4857  mgr = head->mgr;
4858  count = 0;
4859  EpdConvert((double)1.0, &tepd);
4860  for(i=0; i<head->nSize; i++) {
4861    conjunct = head->conjunctArray[i];
4862    bddVarArray = array_alloc(bdd_t *, 0);
4863    for(j=0; j<conjunct->nSize; j++) {
4864      id = conjunct->supList[j];
4865      varBdd = bdd_get_variable(mgr, id);
4866      array_insert_last(bdd_t *, bddVarArray, varBdd);
4867    }
4868    /**
4869    bdd_epd_count_onset(conjunct->relation, bddVarArray, &epd);
4870    EpdMultiply2(&tepd, &epd);
4871    **/
4872    onSet = bdd_count_onset(conjunct->relation, bddVarArray);
4873    EpdMultiply(&tepd, onSet);
4874    count += conjunct->nSize;
4875    mdd_array_free(bddVarArray);
4876  }
4877
4878  if(count < head->nRange) {
4879    EpdMultiply(&tepd, pow(2, (double)(head->nRange-count)));
4880  }
4881  EpdGetString(&tepd, strValue);
4882  (void) fprintf(vis_stdout, "%-20s%10s\n", "range =", strValue);
4883
4884}
4885
4886/**Function********************************************************************
4887
4888  Synopsis    [Check range of variables]
4889
4890  Description [Check range of variables]
4891
4892  SideEffects []
4893
4894  SeeAlso     []
4895
4896******************************************************************************/
4897static int
4898ImgCheckRangeTestAndOverapproximate(Relation_t *head)
4899{
4900Conjunct_t *conjunct;
4901VarLife_t **varArray, *var;
4902int nVarArray, i, k, count;
4903int index;
4904int *varType;
4905int allRangeFlag;
4906bdd_t *relation, *simpleRelation, *varBdd;
4907
4908
4909  allRangeFlag = 1;
4910  for(i=0; i<head->nSize; i++) {
4911    conjunct = head->conjunctArray[i];
4912    if(conjunct->nRange != conjunct->nSize) {
4913      allRangeFlag = 0;
4914      break;
4915    }
4916  }
4917
4918  if(allRangeFlag == 1) return(1);
4919
4920  varArray = head->varArray;
4921  varType = head->varType;
4922  nVarArray = head->nVarArray;
4923  /**
4924  maxIndex = -1;
4925  maxSize = 0;
4926  for(i=0; i<nVarArray; i++) {
4927    var = varArray[i];
4928    if(varType[var->id] == 2)   continue;
4929    if(var->nSize > maxSize) {
4930      maxIndex = i;
4931      maxSize = var->nSize;
4932    }
4933  }
4934
4935  if(maxIndex == -1)    return(1);
4936  **/
4937  count = head->nEffDomain + head->nEffQuantify;
4938  if(count == 0)        return(1);
4939
4940  varArray = ALLOC(VarLife_t *, head->nVarArray);
4941  memcpy(varArray, head->varArray, sizeof(VarLife_t *)*head->nVarArray);
4942  qsort(varArray, head->nVarArray, sizeof(VarLife_t *), ImgLinearCompareVarSize);
4943
4944  if(count != 0) {
4945    count = (count / 10);
4946    if(count == 0) count = 1;
4947  }
4948  k=0;
4949  index = 0;
4950  while(1) {
4951    if(index >= count)  break;
4952    var = varArray[k++];
4953    if(var->stateVar == 2)      continue;
4954    index++;
4955    varBdd = bdd_get_variable(head->mgr, var->id);
4956    for(i=0; i<var->nSize; i++) {
4957      conjunct = head->conjunctArray[var->relArr[i]];
4958      relation = conjunct->relation;
4959      simpleRelation = bdd_smooth_with_cube(relation, varBdd);
4960      if(bdd_equal(relation, simpleRelation)) {
4961        bdd_free(simpleRelation);
4962        continue;
4963      }
4964      bdd_free(relation);
4965 
4966      conjunct->relation = simpleRelation;
4967      conjunct->bModified = 1;
4968      head->bModified = 1;
4969      head->bRefineVarArray = 1;
4970      ImgLinearConjunctRefine(head, conjunct);
4971    }
4972  }
4973  free(varArray);
4974
4975  ImgLinearRefineRelation(head);
4976  ImgLinearConjunctOrderMainCC(head, 0);
4977  ImgLinearRefineRelation(head);
4978
4979  ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0);
4980  ImgLinearPrintTransitionInfo(head);
4981 
4982  return(0);
4983}
4984
4985/**Function********************************************************************
4986
4987  Synopsis    [Add singleton next state variable case into array]
4988
4989  Description [Add singleton next state variable case into array]
4990
4991  SideEffects []
4992
4993  SeeAlso     []
4994
4995******************************************************************************/
4996static void
4997ImgLinearAddNextStateCase(Relation_t *head)
4998{
4999Conjunct_t **newConjunctArray;
5000int i, j, index;
5001
5002  index = 0;
5003  if(head->nNextStateArray) {
5004    newConjunctArray = ALLOC(Conjunct_t *, head->nSize + head->nNextStateArray);
5005   for(j=0; j<head->nSize; j++) 
5006      newConjunctArray[index++] = head->conjunctArray[j];
5007
5008    for(i=0; i<head->nNextStateArray; i++) 
5009      newConjunctArray[index++] = head->nextStateArray[i];
5010
5011    head->nSize = index;
5012    head->bModified = 1;
5013    head->bRefineVarArray = 1;
5014    free(head->conjunctArray);
5015    head->conjunctArray = newConjunctArray;
5016
5017    if(head->nextStateArray)    free(head->nextStateArray);
5018    head->nextStateArray = 0;
5019  }
5020}
5021
Note: See TracBrowser for help on using the repository browser.