source: vis_dev/vis-2.3/src/img/imgHybrid.c @ 17

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

vis2.3
File size: 49.1 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [imgHybrid.c]
4
5  PackageName [img]
6
7  Synopsis    [Routines for hybrid image computation.]
8
9  Description [The hybrid image computation method combines transition function
10  and relation methods, in other words, combines splitting and conjunction
11  methods.]
12
13  SeeAlso     []
14
15  Author      [In-Ho Moon]
16
17  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado.
18  All rights reserved.
19
20  Permission is hereby granted, without written agreement and without license
21  or royalty fees, to use, copy, modify, and distribute this software and its
22  documentation for any purpose, provided that the above copyright notice and
23  the following two paragraphs appear in all copies of this software.
24
25  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
26  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
27  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
28  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
29
30  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
31  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
32  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
33  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
34  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
35
36******************************************************************************/
37#include "imgInt.h"
38
39static char rcsid[] UNUSED = "$Id: imgHybrid.c,v 1.27 2008/11/27 02:19:53 fabio Exp $";
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Type declarations                                                         */
47/*---------------------------------------------------------------------------*/
48
49/*---------------------------------------------------------------------------*/
50/* Structure declarations                                                    */
51/*---------------------------------------------------------------------------*/
52
53/*---------------------------------------------------------------------------*/
54/* Variable declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57/*---------------------------------------------------------------------------*/
58/* Macro declarations                                                        */
59/*---------------------------------------------------------------------------*/
60
61/**AutomaticStart*************************************************************/
62
63/*---------------------------------------------------------------------------*/
64/* Static function prototypes                                                */
65/*---------------------------------------------------------------------------*/
66
67static float ComputeSupportLambda(ImgTfmInfo_t *info, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, mdd_t *from, array_t *vector, int newRelationFlag, int preFlag, float *improvedLambda);
68
69/**AutomaticEnd***************************************************************/
70
71
72/*---------------------------------------------------------------------------*/
73/* Definition of exported functions                                          */
74/*---------------------------------------------------------------------------*/
75
76
77/**Function********************************************************************
78
79  Synopsis    [Prints the options for hybrid image computation.]
80
81  Description [Prints the options for hybrid image computation.]
82
83  SideEffects []
84
85  SeeAlso     []
86
87******************************************************************************/
88void
89Img_PrintHybridOptions(void)
90{
91  ImgTfmOption_t        *options;
92  char                  dummy[80];
93
94  options = ImgTfmGetOptions(Img_Hybrid_c);
95
96  switch (options->hybridMode) {
97  case 0 :
98    sprintf(dummy, "with only transition function");
99    break;
100  case 1 :
101    sprintf(dummy, "with both transition function and relation");
102    break;
103  case 2 :
104    sprintf(dummy, "with only transition relation");
105    break;
106  default :
107    sprintf(dummy, "invalid");
108    break;
109  }
110  fprintf(vis_stdout, "HYB: hybrid_mode = %d (%s)\n",
111          options->hybridMode, dummy);
112
113  switch (options->trSplitMethod) {
114  case 0 :
115    sprintf(dummy, "support");
116    break;
117  case 1 :
118    sprintf(dummy, "estimate BDD size");
119    break;
120  default :
121    sprintf(dummy, "invalid");
122    break;
123  }
124  fprintf(vis_stdout, "HYB: hybrid_tr_split_method = %d (%s)\n",
125          options->trSplitMethod, dummy);
126
127  if (options->buildPartialTR)
128    sprintf(dummy, "yes");
129  else
130    sprintf(dummy, "no");
131  fprintf(vis_stdout, "HYB: hybrid_build_partial_tr = %s\n", dummy);
132
133  fprintf(vis_stdout, "HYB: hybrid_partial_num_vars = %d\n",
134          options->nPartialVars);
135
136  switch (options->partialMethod) {
137  case 0 :
138    sprintf(dummy, "BDD size");
139    break;
140  case 1 :
141    sprintf(dummy, "support");
142    break;
143  default :
144    sprintf(dummy, "invalid");
145    break;
146  }
147  fprintf(vis_stdout, "HYB: hybrid_partial_method = %d (%s)\n",
148          options->partialMethod, dummy);
149
150  if (options->delayedSplit)
151    sprintf(dummy, "yes");
152  else
153    sprintf(dummy, "no");
154  fprintf(vis_stdout, "HYB: hybrid_delayed_split = %s\n", dummy);
155
156  fprintf(vis_stdout, "HYB: hybrid_split_min_depth = %d\n",
157          options->splitMinDepth);
158  fprintf(vis_stdout, "HYB: hybrid_split_max_depth = %d\n",
159          options->splitMaxDepth);
160  fprintf(vis_stdout, "HYB: hybrid_pre_split_min_depth = %d\n",
161          options->preSplitMinDepth);
162  fprintf(vis_stdout, "HYB: hybrid_pre_split_max_depth = %d\n",
163          options->preSplitMaxDepth);
164
165  fprintf(vis_stdout, "HYB: hybrid_lambda_threshold = %.2f\n",
166          options->lambdaThreshold);
167  fprintf(vis_stdout, "HYB: hybrid_pre_lambda_threshold = %.2f\n",
168          options->preLambdaThreshold);
169  fprintf(vis_stdout, "HYB: hybrid_conjoin_vector_size = %d\n",
170          options->conjoinVectorSize);
171  fprintf(vis_stdout, "HYB: hybrid_conjoin_relation_size = %d\n",
172          options->conjoinRelationSize);
173  fprintf(vis_stdout, "HYB: hybrid_conjoin_relation_bdd_size = %d\n",
174          options->conjoinRelationBddSize);
175  fprintf(vis_stdout, "HYB: hybrid_improve_lambda = %.2f\n",
176          options->improveLambda);
177  fprintf(vis_stdout, "HYB: hybrid_improve_vector_size = %d\n",
178          options->improveVectorSize);
179  fprintf(vis_stdout, "HYB: hybrid_improve_vector_bdd_size = %.2f\n",
180          options->improveVectorBddSize);
181
182  switch (options->decideMode) {
183  case 0 :
184    sprintf(dummy, "use only lambda");
185    break;
186  case 1 :
187    sprintf(dummy, "lambda + special check");
188    break;
189  case 2 :
190    sprintf(dummy, "lambda + improvement");
191    break;
192  case 3 :
193    sprintf(dummy, "use all");
194    break;
195  default :
196    sprintf(dummy, "invalid");
197    break;
198  }
199  fprintf(vis_stdout, "HYB: hybrid_decide_mode = %d (%s)\n",
200          options->decideMode, dummy);
201
202  if (options->reorderWithFrom)
203    sprintf(dummy, "yes");
204  else
205    sprintf(dummy, "no");
206  fprintf(vis_stdout, "HYB: hybrid_reorder_with_from = %s\n", dummy);
207
208  if (options->preReorderWithFrom)
209    sprintf(dummy, "yes");
210  else
211    sprintf(dummy, "no");
212  fprintf(vis_stdout, "HYB: hybrid_pre_reorder_with_from = %s\n", dummy);
213
214  switch (options->lambdaMode) {
215  case 0 :
216    sprintf(dummy, "total lifetime with ps/pi variables");
217    break;
218  case 1 :
219    sprintf(dummy, "active lifetime with ps/pi variables");
220    break;
221  case 2 :
222    sprintf(dummy, "total lifetime with ps/ns/pi variables");
223    break;
224  default :
225    sprintf(dummy, "invalid");
226    break;
227  }
228  fprintf(vis_stdout, "HYB: hybrid_lambda_mode = %d (%s)\n",
229          options->lambdaMode, dummy);
230
231  switch (options->preLambdaMode) {
232  case 0 :
233    sprintf(dummy, "total lifetime with ns/pi variables");
234    break;
235  case 1 :
236    sprintf(dummy, "active lifetime with ps/pi variables");
237    break;
238  case 2 :
239    sprintf(dummy, "total lifetime with ps/ns/pi variables");
240    break;
241  case 3 :
242    sprintf(dummy, "total lifetime with ps/pi variables");
243    break;
244  default :
245    sprintf(dummy, "invalid");
246    break;
247  }
248  fprintf(vis_stdout, "HYB: hybrid_pre_lambda_mode = %d (%s)\n",
249          options->preLambdaMode, dummy);
250
251  if (options->lambdaWithFrom)
252    sprintf(dummy, "yes");
253  else
254    sprintf(dummy, "no");
255  fprintf(vis_stdout, "HYB: hybrid_lambda_with_from = %s\n", dummy);
256
257  if (options->lambdaWithTr)
258    sprintf(dummy, "yes");
259  else
260    sprintf(dummy, "no");
261  fprintf(vis_stdout, "HYB: hybrid_lambda_with_tr = %s\n", dummy);
262
263  if (options->lambdaWithClustering)
264    sprintf(dummy, "yes");
265  else
266    sprintf(dummy, "no");
267  fprintf(vis_stdout, "HYB: hybrid_lambda_with_clustering = %s\n", dummy);
268
269  if (options->synchronizeTr)
270    sprintf(dummy, "yes");
271  else
272    sprintf(dummy, "no");
273  fprintf(vis_stdout, "HYB: hybrid_synchronize_tr = %s\n", dummy);
274
275  if (options->imgKeepPiInTr)
276    sprintf(dummy, "yes");
277  else
278    sprintf(dummy, "no");
279  fprintf(vis_stdout, "HYB: hybrid_img_keep_pi = %s\n", dummy);
280
281  if (options->preKeepPiInTr)
282    sprintf(dummy, "yes");
283  else
284    sprintf(dummy, "no");
285  fprintf(vis_stdout, "HYB: hybrid_pre_keep_pi = %s\n", dummy);
286
287  if (options->preCanonical)
288    sprintf(dummy, "yes");
289  else
290    sprintf(dummy, "no");
291  fprintf(vis_stdout, "HYB: hybrid_pre_canonical = %s\n", dummy);
292
293  switch (options->trMethod) {
294  case Img_Iwls95_c :
295    sprintf(dummy, "IWLS95");
296    break;
297  case Img_Mlp_c :
298    sprintf(dummy, "MLP");
299    break;
300  default :
301    sprintf(dummy, "invalid");
302    break;
303  }
304  fprintf(vis_stdout, "HYB: hybrid_tr_method = %s\n", dummy);
305
306  FREE(options);
307}
308
309
310/*---------------------------------------------------------------------------*/
311/* Definition of internal functions                                          */
312/*---------------------------------------------------------------------------*/
313
314
315/**Function********************************************************************
316
317  Synopsis    [Decides whether to split or to conjoin.]
318
319  Description [Decides whether to split or to conjoin.]
320
321  SideEffects []
322
323******************************************************************************/
324int
325ImgDecideSplitOrConjoin(ImgTfmInfo_t *info, array_t *vector, mdd_t *from,
326                        int preFlag, array_t *relationArray,
327                        mdd_t *cofactorCube, mdd_t *abstractCube,
328                        int useBothFlag, int depth)
329{
330  int   conjoin = 0;
331  float lambda, improvedLambda;
332  int   vectorBddSize, vectorSize;
333  int   improved;
334  int   minDepth;
335  int   checkSpecialCases;
336  int   checkImprovement;
337  int   relationSize = 0;
338
339  if (!preFlag) {
340    if (vector && array_n(vector) <= 2)
341      return(0); /* terminal case */
342  }
343
344  if (info->option->decideMode == 1 || info->option->decideMode == 3)
345    checkSpecialCases = 1;
346  else
347    checkSpecialCases = 0;
348  if (info->option->decideMode == 2 || info->option->decideMode == 3)
349    checkImprovement = 1;
350  else
351    checkImprovement = 0;
352
353  if (checkSpecialCases) {
354    if (vector && array_n(vector) <= info->option->conjoinVectorSize) {
355      if (preFlag)
356        info->nConjoinsB++;
357      else
358        info->nConjoins++;
359      if (info->option->printLambda) {
360        fprintf(vis_stdout, "%d: conjoin - small vector size (%d)\n",
361                depth, array_n(vector));
362      }
363      return(1);
364    }
365  }
366
367  if (preFlag)
368    minDepth = info->option->preSplitMinDepth;
369  else
370    minDepth = info->option->splitMinDepth;
371
372  if (useBothFlag && relationArray && vector) {
373    lambda = ComputeSupportLambda(info, relationArray, cofactorCube,
374                                  abstractCube, from, vector,
375                                  0, preFlag, &improvedLambda);
376  } else if (relationArray) {
377    if (checkSpecialCases) {
378      if (array_n(relationArray) <= info->option->conjoinRelationSize ||
379          (relationSize = (int)bdd_size_multiple(relationArray)) <=
380                info->option->conjoinRelationBddSize) {
381        if (preFlag)
382          info->nConjoinsB++;
383        else
384          info->nConjoins++;
385        if (info->option->printLambda) {
386          fprintf(vis_stdout, "%d: conjoin - small relation array (%d, %ld)\n",
387                  depth, array_n(relationArray),
388                  bdd_size_multiple(relationArray));
389        }
390        return(1);
391      }
392    }
393
394    lambda = ComputeSupportLambda(info, relationArray, cofactorCube,
395                                  abstractCube, from, NIL(array_t),
396                                  0, preFlag, &improvedLambda);
397  } else {
398    int         i;
399    ImgComponent_t      *comp;
400
401    relationArray = array_alloc(mdd_t *, 0);
402    for (i = 0; i < array_n(vector); i++) {
403      comp = array_fetch(ImgComponent_t *, vector, i);
404      array_insert_last(mdd_t *, relationArray, comp->func);
405    }
406
407    lambda = ComputeSupportLambda(info, relationArray, NIL(mdd_t),
408                                  NIL(mdd_t), from, NIL(array_t),
409                                  1, preFlag, &improvedLambda);
410
411    array_free(relationArray);
412  }
413
414  if ((preFlag == 0 && lambda <= info->option->lambdaThreshold) ||
415      (preFlag == 1 && lambda <= info->option->preLambdaThreshold)) {
416    if (preFlag)
417      info->nConjoinsB++;
418    else
419      info->nConjoins++;
420    if (info->option->printLambda) {
421      fprintf(vis_stdout, "%d: conjoin - small lambda (%.2f)\n",
422              depth, lambda);
423    }
424    conjoin = 1;
425  } else {
426    if (checkImprovement) {
427      if (vector) {
428        vectorBddSize = ImgVectorBddSize(vector);
429        vectorSize = array_n(vector);
430        if (depth == minDepth ||
431            improvedLambda >= info->option->improveLambda ||
432            ((float)vectorBddSize * 100.0 / (float)info->prevVectorBddSize) <=
433                info->option->improveVectorBddSize ||
434            (info->prevVectorSize - vectorSize) >=
435                info->option->improveVectorSize) {
436          improved = 1;
437        } else
438          improved = 0;
439        info->prevVectorBddSize = vectorBddSize;
440        info->prevVectorSize = vectorSize;
441      } else {
442        if (relationSize)
443          vectorBddSize = relationSize;
444        else
445          vectorBddSize = (int)bdd_size_multiple(relationArray);
446        if (depth == minDepth ||
447            improvedLambda >= info->option->improveLambda ||
448            ((float)vectorBddSize * 100.0 / (float)info->prevVectorBddSize) <=
449                info->option->improveVectorBddSize) {
450          improved = 1;
451        } else
452          improved = 0;
453        info->prevVectorBddSize = vectorBddSize;
454      }
455      if (improved) {
456        if (preFlag)
457          info->nSplitsB++;
458        else
459          info->nSplits++;
460        if (info->option->printLambda) {
461          fprintf(vis_stdout, "%d: split - big lambda (%.2f) - improved\n",
462                  depth, lambda);
463        }
464        conjoin = 0;
465      } else {
466        if (preFlag)
467          info->nConjoinsB++;
468        else
469          info->nConjoins++;
470        if (info->option->printLambda) {
471          fprintf(vis_stdout, "%d: conjon - big lambda (%.2f) - not improved\n",
472                  depth, lambda);
473        }
474        conjoin = 1;
475      }
476    } else {
477      if (preFlag)
478        info->nSplitsB++;
479      else
480        info->nSplits++;
481      if (info->option->printLambda) {
482        fprintf(vis_stdout, "%d: split - big lambda (%.2f)\n",
483              depth, lambda);
484      }
485      conjoin = 0;
486    }
487  }
488
489  return(conjoin); /* 0 : split, 1 : conjoin */
490}
491
492
493/**Function********************************************************************
494
495  Synopsis    [Computes an image by transition relation.]
496
497  Description [Computes an image by transition relation.]
498
499  SideEffects []
500
501******************************************************************************/
502mdd_t *
503ImgImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from)
504{
505  int                   i, j, nVars;
506  array_t               *relationArray;
507  mdd_t                 *result, *domain, *relation, *var, *nextVar;
508  ImgComponent_t        *comp;
509  char                  *support;
510  array_t               *smoothVarsBddArray, *introducedVarsBddArray;
511  array_t               *domainVarsBddArray;
512  int                   bddId;
513
514  if (from && bdd_is_tautology(from, 0))
515    return(mdd_zero(info->manager));
516
517  nVars = info->nVars;
518  support = ALLOC(char, sizeof(char) * nVars);
519  memset(support, 0, sizeof(char) * nVars);
520
521  relationArray = array_alloc(mdd_t *, 0);
522  introducedVarsBddArray = array_alloc(mdd_t *, 0);
523
524  for (i = 0; i < array_n(vector); i++) {
525    comp = array_fetch(ImgComponent_t *, vector, i);
526    if (comp->intermediate) {
527      relation = mdd_xnor(comp->var, comp->func);
528      bddId = (int)bdd_top_var_id(comp->var);
529      support[bddId] = 1;
530    } else {
531      nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
532      relation = mdd_xnor(nextVar, comp->func);
533      array_insert_last(mdd_t *, introducedVarsBddArray, nextVar);
534    }
535    array_insert_last(mdd_t *, relationArray, relation);
536 
537    for (j = 0; j < nVars; j++)
538      support[j] = support[j] | comp->support[j];
539  }
540
541  if (from && (!bdd_is_tautology(from, 1))) {
542    if (info->option->reorderWithFrom)
543      array_insert_last(mdd_t *, relationArray, mdd_dup(from));
544
545    comp = ImgComponentAlloc(info);
546    comp->func = from;
547    ImgComponentGetSupport(comp);
548    for (i = 0; i < nVars; i++)
549      support[i] = support[i] | comp->support[i];
550    comp->func = NIL(mdd_t);
551    ImgComponentFree(comp);
552  }
553
554  smoothVarsBddArray = array_alloc(mdd_t *, 0);
555  if (!info->option->reorderWithFrom)
556    domainVarsBddArray = array_alloc(mdd_t *, 0);
557  else
558    domainVarsBddArray = NIL(array_t);
559  for (i = 0; i < nVars; i++) {
560    if (support[i]) {
561      var = bdd_var_with_index(info->manager, i);
562      if ((!from) || info->option->reorderWithFrom)
563        array_insert_last(mdd_t *, smoothVarsBddArray, var);
564      else {
565        if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)) ||
566            (info->intermediateVarsTable &&
567             st_lookup(info->intermediateVarsTable, (char *)(long)i,
568                        NIL(char *)))) {
569          array_insert_last(mdd_t *, smoothVarsBddArray, var);
570        } else {
571          array_insert_last(mdd_t *, domainVarsBddArray, var);
572        }
573      }
574    }
575  }
576  FREE(support);
577
578  if ((!from) || info->option->reorderWithFrom) {
579    result = ImgMultiwayLinearAndSmooth(info->manager,
580                                        relationArray,
581                                        smoothVarsBddArray,
582                                        introducedVarsBddArray,
583                                        info->option->trMethod,
584                                        Img_Forward_c,
585                                        info->trmOption);
586  } else {
587    result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
588                                                relationArray, from,
589                                                smoothVarsBddArray,
590                                                domainVarsBddArray,
591                                                introducedVarsBddArray,
592                                                info->option->trMethod,
593                                                Img_Forward_c,
594                                                info->trmOption);
595    mdd_array_free(domainVarsBddArray);
596  }
597  mdd_array_free(relationArray);
598  mdd_array_free(smoothVarsBddArray);
599  mdd_array_free(introducedVarsBddArray);
600  domain = ImgSubstitute(result, info->functionData, Img_R2D_c);
601  mdd_free(result);
602  return(domain);
603}
604
605
606/**Function********************************************************************
607
608  Synopsis    [Computes an image by transition relation.]
609
610  Description [Computes an image by transition relation.]
611
612  SideEffects []
613
614******************************************************************************/
615mdd_t *
616ImgImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector,
617                                mdd_t *from, array_t *relationArray,
618                                mdd_t *cofactorCube, mdd_t *abstractCube)
619{
620  int                   i, j;
621  array_t               *mergedRelationArray;
622  mdd_t                 *result, *domain, *relation, *var, *nextVar;
623  ImgComponent_t        *comp, *supportComp;
624  int                   nVars;
625  char                  *support;
626  array_t               *smoothVarsBddArray, *introducedVarsBddArray;
627  array_t               *domainVarsBddArray;
628
629  if (from && bdd_is_tautology(from, 0))
630    return(mdd_zero(info->manager));
631
632  if (cofactorCube && abstractCube) {
633    if (!bdd_is_tautology(cofactorCube, 1) &&
634        !bdd_is_tautology(abstractCube, 1)) {
635      mergedRelationArray = ImgGetCofactoredAbstractedRelationArray(
636                                        info->manager, relationArray,
637                                        cofactorCube, abstractCube);
638    } else if (!bdd_is_tautology(cofactorCube, 1)) {
639      mergedRelationArray = ImgGetCofactoredRelationArray(relationArray,
640                                                          cofactorCube);
641    } else if (!bdd_is_tautology(abstractCube, 1)) {
642      mergedRelationArray = ImgGetAbstractedRelationArray(info->manager,
643                                                          relationArray,
644                                                          abstractCube);
645    } else
646      mergedRelationArray = mdd_array_duplicate(relationArray);
647  } else
648    mergedRelationArray = mdd_array_duplicate(relationArray);
649
650  nVars = info->nVars;
651  support = ALLOC(char, sizeof(char) * nVars);
652  memset(support, 0, sizeof(char) * nVars);
653
654  supportComp = ImgComponentAlloc(info);
655  for (i = 0; i < array_n(mergedRelationArray); i++) {
656    supportComp->func = array_fetch(mdd_t *, mergedRelationArray, i);;
657    ImgSupportClear(info, supportComp->support);
658    ImgComponentGetSupport(supportComp);
659    for (j = 0; j < nVars; j++)
660      support[j] = support[j] | supportComp->support[j];
661  }
662
663  if (vector && array_n(vector) > 0) {
664    for (i = 0; i < array_n(vector); i++) {
665      comp = array_fetch(ImgComponent_t *, vector, i);
666      if (comp->intermediate) {
667        relation = mdd_xnor(comp->var, comp->func);
668        support[(int)bdd_top_var_id(comp->var)] = 1;
669      } else {
670        nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
671        relation = mdd_xnor(nextVar, comp->func);
672        support[(int)bdd_top_var_id(nextVar)] = 1;
673        mdd_free(nextVar);
674      }
675      array_insert_last(mdd_t *, mergedRelationArray, relation);
676
677      for (j = 0; j < nVars; j++)
678        support[j] = support[j] | comp->support[j];
679    }
680  }
681
682  if (from) {
683    if ((!bdd_is_tautology(from, 1)) && info->option->reorderWithFrom)
684      array_insert_last(mdd_t *, mergedRelationArray, mdd_dup(from));
685
686    supportComp->func = from;
687    ImgSupportClear(info, supportComp->support);
688    ImgComponentGetSupport(supportComp);
689    for (i = 0; i < nVars; i++)
690      support[i] = support[i] | supportComp->support[i];
691  }
692  supportComp->func = NIL(mdd_t);
693  ImgComponentFree(supportComp);
694
695  smoothVarsBddArray = array_alloc(mdd_t *, 0);
696  introducedVarsBddArray = array_alloc(mdd_t *, 0);
697  if (!info->option->reorderWithFrom)
698    domainVarsBddArray = array_alloc(mdd_t *, 0);
699  else
700    domainVarsBddArray = NIL(array_t);
701  for (i = 0; i < nVars; i++) {
702    if (support[i]) {
703      var = bdd_var_with_index(info->manager, i);
704      if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
705        array_insert_last(mdd_t *, introducedVarsBddArray, var);
706      else if ((!from) || info->option->reorderWithFrom)
707        array_insert_last(mdd_t *, smoothVarsBddArray, var);
708      else {
709        if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)) ||
710            (info->intermediateVarsTable &&
711             st_lookup(info->intermediateVarsTable, (char *)(long)i,
712                        NIL(char *)))) {
713          array_insert_last(mdd_t *, smoothVarsBddArray, var);
714        } else {
715          array_insert_last(mdd_t *, domainVarsBddArray, var);
716        }
717      }
718    }
719  }
720  FREE(support);
721
722  if ((!from) || info->option->reorderWithFrom) {
723    result = ImgMultiwayLinearAndSmooth(info->manager,
724                                        mergedRelationArray,
725                                        smoothVarsBddArray,
726                                        introducedVarsBddArray,
727                                        info->option->trMethod,
728                                        Img_Forward_c,
729                                        info->trmOption);
730  } else {
731    result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
732                                                mergedRelationArray, from,
733                                                smoothVarsBddArray,
734                                                domainVarsBddArray,
735                                                introducedVarsBddArray,
736                                                info->option->trMethod,
737                                                Img_Forward_c,
738                                                info->trmOption);
739    mdd_array_free(domainVarsBddArray);
740  }
741  mdd_array_free(mergedRelationArray);
742  mdd_array_free(smoothVarsBddArray);
743  mdd_array_free(introducedVarsBddArray);
744
745  domain = ImgSubstitute(result, info->functionData, Img_R2D_c);
746  mdd_free(result);
747  return(domain);
748}
749
750
751/**Function********************************************************************
752
753  Synopsis    [Computes a preimage by transition relation.]
754
755  Description [Computes a preimage by transition relation.]
756
757  SideEffects []
758
759******************************************************************************/
760mdd_t *
761ImgPreImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from)
762{
763  int                   i, j, nVars;
764  array_t               *relationArray;
765  mdd_t                 *result, *relation, *var, *nextVar;
766  ImgComponent_t        *comp;
767  char                  *support;
768  array_t               *smoothVarsBddArray, *introducedVarsBddArray;
769  array_t               *rangeVarsBddArray;
770  mdd_t                 *fromRange;
771
772  if (bdd_is_tautology(from, 1))
773    return(mdd_one(info->manager));
774  else if (bdd_is_tautology(from, 0))
775    return(mdd_zero(info->manager));
776
777  nVars = info->nVars;
778  support = ALLOC(char, sizeof(char) * nVars);
779  memset(support, 0, sizeof(char) * nVars);
780
781  relationArray = array_alloc(mdd_t *, 0);
782
783  for (i = 0; i < array_n(vector); i++) {
784    comp = array_fetch(ImgComponent_t *, vector, i);
785    if (comp->intermediate) {
786      relation = mdd_xnor(comp->var, comp->func);
787      support[(int)bdd_top_var_id(comp->var)] = 1;
788    } else {
789      nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
790      relation = mdd_xnor(nextVar, comp->func);
791      support[(int)bdd_top_var_id(nextVar)] = 1;
792      mdd_free(nextVar);
793    }
794    array_insert_last(mdd_t *, relationArray, relation);
795 
796    for (j = 0; j < nVars; j++)
797      support[j] = support[j] | comp->support[j];
798  }
799
800  fromRange = ImgSubstitute(from, info->functionData, Img_D2R_c);
801  comp = ImgComponentAlloc(info);
802  comp->func = fromRange;
803  ImgComponentGetSupport(comp);
804  for (i = 0; i < nVars; i++)
805    support[i] = support[i] | comp->support[i];
806  comp->func = NIL(mdd_t);
807  ImgComponentFree(comp);
808
809  smoothVarsBddArray = array_alloc(mdd_t *, 0);
810  introducedVarsBddArray = array_alloc(mdd_t *, 0);
811  if (!info->option->preReorderWithFrom)
812    rangeVarsBddArray = array_alloc(mdd_t *, 0);
813  else
814    rangeVarsBddArray = NIL(array_t);
815  for (i = 0; i < nVars; i++) {
816    if (support[i]) {
817      var = bdd_var_with_index(info->manager, i);
818      if (info->intermediateVarsTable &&
819          st_lookup(info->intermediateVarsTable, (char *)(long)i,
820                    NIL(char *))) {
821        array_insert_last(mdd_t *, smoothVarsBddArray, var);
822      } else if (st_lookup(info->rangeVarsTable, (char *)(long)i,
823                           NIL(char *))) {
824        if (info->option->preReorderWithFrom)
825          array_insert_last(mdd_t *, smoothVarsBddArray, var);
826        else
827          array_insert_last(mdd_t *, rangeVarsBddArray, var);
828      } else {
829        if (info->preKeepPiInTr)
830          array_insert_last(mdd_t *, introducedVarsBddArray, var);
831        else {
832          if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
833                        NIL(char *))) {
834            array_insert_last(mdd_t *, smoothVarsBddArray, var);
835          } else
836            array_insert_last(mdd_t *, introducedVarsBddArray, var);
837        }
838      }
839    }
840  }
841  FREE(support);
842
843  if (info->option->preReorderWithFrom) {
844    array_insert_last(mdd_t *, relationArray, fromRange);
845    result = ImgMultiwayLinearAndSmooth(info->manager,
846                                        relationArray,
847                                        smoothVarsBddArray,
848                                        introducedVarsBddArray,
849                                        info->option->trMethod,
850                                        Img_Backward_c,
851                                        info->trmOption);
852  } else {
853    result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
854                                                relationArray, fromRange,
855                                                smoothVarsBddArray,
856                                                rangeVarsBddArray,
857                                                introducedVarsBddArray,
858                                                info->option->trMethod,
859                                                Img_Backward_c,
860                                                info->trmOption);
861    mdd_free(fromRange);
862    mdd_array_free(rangeVarsBddArray);
863  }
864  mdd_array_free(relationArray);
865  mdd_array_free(smoothVarsBddArray);
866  mdd_array_free(introducedVarsBddArray);
867  return(result);
868}
869
870
871/**Function********************************************************************
872
873  Synopsis    [Computes a preimage by transition relation.]
874
875  Description [Computes a preimage by transition relation.]
876
877  SideEffects []
878
879******************************************************************************/
880mdd_t *
881ImgPreImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector,
882                                   mdd_t *from, array_t *relationArray,
883                                   mdd_t *cofactorCube, mdd_t *abstractCube)
884{
885  int                   i, j;
886  array_t               *mergedRelationArray;
887  mdd_t                 *result, *relation, *var, *nextVar, *fromRange;
888  ImgComponent_t        *comp, *supportComp;
889  int                   nVars;
890  char                  *support;
891  array_t               *smoothVarsBddArray, *introducedVarsBddArray;
892  array_t               *rangeVarsBddArray;
893
894  if (bdd_is_tautology(from, 1))
895    return(mdd_one(info->manager));
896  if (bdd_is_tautology(from, 0))
897    return(mdd_zero(info->manager));
898
899  if (cofactorCube && abstractCube) {
900    if (!bdd_is_tautology(cofactorCube, 1) &&
901        !bdd_is_tautology(abstractCube, 1)) {
902      mergedRelationArray = ImgGetCofactoredAbstractedRelationArray(
903                                        info->manager, relationArray,
904                                        cofactorCube, abstractCube);
905    } else if (!bdd_is_tautology(cofactorCube, 1)) {
906      mergedRelationArray = ImgGetCofactoredRelationArray(relationArray,
907                                                          cofactorCube);
908    } else if (!bdd_is_tautology(abstractCube, 1)) {
909      mergedRelationArray = ImgGetAbstractedRelationArray(info->manager,
910                                                          relationArray,
911                                                          abstractCube);
912    } else
913      mergedRelationArray = mdd_array_duplicate(relationArray);
914  } else
915    mergedRelationArray = mdd_array_duplicate(relationArray);
916
917  nVars = info->nVars;
918  support = ALLOC(char, sizeof(char) * nVars);
919  memset(support, 0, sizeof(char) * nVars);
920
921  supportComp = ImgComponentAlloc(info);
922  for (i = 0; i < array_n(mergedRelationArray); i++) {
923    supportComp->func = array_fetch(mdd_t *, mergedRelationArray, i);;
924    ImgSupportClear(info, supportComp->support);
925    ImgComponentGetSupport(supportComp);
926    for (j = 0; j < nVars; j++)
927      support[j] = support[j] | supportComp->support[j];
928  }
929
930  if (vector && array_n(vector) > 0) {
931    for (i = 0; i < array_n(vector); i++) {
932      comp = array_fetch(ImgComponent_t *, vector, i);
933      if (comp->intermediate) {
934        relation = mdd_xnor(comp->var, comp->func);
935        support[(int)bdd_top_var_id(comp->var)] = 1;
936      } else {
937        nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
938        relation = mdd_xnor(nextVar, comp->func);
939        support[(int)bdd_top_var_id(nextVar)] = 1;
940        mdd_free(nextVar);
941      }
942      array_insert_last(mdd_t *, mergedRelationArray, relation);
943
944      for (j = 0; j < nVars; j++)
945        support[j] = support[j] | comp->support[j];
946    }
947  }
948
949  fromRange = ImgSubstitute(from, info->functionData, Img_D2R_c);
950  supportComp->func = fromRange;
951  ImgSupportClear(info, supportComp->support);
952  ImgComponentGetSupport(supportComp);
953  for (i = 0; i < nVars; i++)
954    support[i] = support[i] | supportComp->support[i];
955  supportComp->func = NIL(mdd_t);
956  ImgComponentFree(supportComp);
957
958  smoothVarsBddArray = array_alloc(mdd_t *, 0);
959  introducedVarsBddArray = array_alloc(mdd_t *, 0);
960  if (!info->option->preReorderWithFrom)
961    rangeVarsBddArray = array_alloc(mdd_t *, 0);
962  else
963    rangeVarsBddArray = NIL(array_t);
964  for (i = 0; i < nVars; i++) {
965    if (support[i]) {
966      var = bdd_var_with_index(info->manager, i);
967      if (info->intermediateVarsTable &&
968          st_lookup(info->intermediateVarsTable, (char *)(long)i,
969                    NIL(char *))) {
970        array_insert_last(mdd_t *, smoothVarsBddArray, var);
971      } else if (st_lookup(info->rangeVarsTable, (char *)(long)i,
972                           NIL(char *))) {
973        if (info->option->preReorderWithFrom)
974          array_insert_last(mdd_t *, smoothVarsBddArray, var);
975        else
976          array_insert_last(mdd_t *, rangeVarsBddArray, var);
977      } else {
978        if (info->preKeepPiInTr)
979          array_insert_last(mdd_t *, introducedVarsBddArray, var);
980        else {
981          if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
982                        NIL(char *))) {
983            array_insert_last(mdd_t *, smoothVarsBddArray, var);
984          } else
985            array_insert_last(mdd_t *, introducedVarsBddArray, var);
986        }
987      }
988    }
989  }
990  FREE(support);
991
992  if (info->option->preReorderWithFrom) {
993    array_insert_last(mdd_t *, mergedRelationArray, fromRange);
994    result = ImgMultiwayLinearAndSmooth(info->manager,
995                                        mergedRelationArray,
996                                        smoothVarsBddArray,
997                                        introducedVarsBddArray,
998                                        info->option->trMethod,
999                                        Img_Backward_c,
1000                                        info->trmOption);
1001  } else {
1002    result = ImgMultiwayLinearAndSmoothWithFrom(info->manager,
1003                                                mergedRelationArray, fromRange,
1004                                                smoothVarsBddArray,
1005                                                rangeVarsBddArray,
1006                                                introducedVarsBddArray,
1007                                                info->option->trMethod,
1008                                                Img_Backward_c,
1009                                                info->trmOption);
1010    mdd_free(fromRange);
1011    mdd_array_free(rangeVarsBddArray);
1012  }
1013  mdd_array_free(mergedRelationArray);
1014  mdd_array_free(smoothVarsBddArray);
1015  mdd_array_free(introducedVarsBddArray);
1016
1017  return(result);
1018}
1019
1020
1021/**Function********************************************************************
1022
1023  Synopsis    [Checks whether a vector is equivalent to a relation array.]
1024
1025  Description [Checks whether a vector is equivalent to a relation array.]
1026
1027  SideEffects []
1028
1029******************************************************************************/
1030int
1031ImgCheckEquivalence(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray,
1032                    mdd_t *cofactorCube, mdd_t *abstractCube, int preFlag)
1033{
1034  int                   i, equal;
1035  mdd_t                 *product1, *product2;
1036  mdd_t                 *var, *tmp, *relation;
1037  ImgComponent_t        *comp;
1038  array_t               *newRelationArray, *tmpRelationArray;
1039  array_t               *domainVarBddArray, *quantifyVarBddArray;
1040
1041  tmpRelationArray = array_alloc(mdd_t *, 0);
1042  for (i = 0; i < array_n(vector); i++) {
1043    comp = array_fetch(ImgComponent_t *, vector, i);
1044    if (comp->intermediate)
1045      relation = mdd_xnor(comp->var, comp->func);
1046    else {
1047      var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1048      relation = mdd_xnor(var, comp->func);
1049      mdd_free(var);
1050    }
1051    array_insert_last(mdd_t *, tmpRelationArray, relation);
1052  }
1053
1054  if (preFlag) {
1055    if (info->preKeepPiInTr) {
1056      quantifyVarBddArray = array_alloc(mdd_t *, 0);
1057      domainVarBddArray = array_join(info->domainVarBddArray,
1058                                     info->quantifyVarBddArray);
1059    } else {
1060      quantifyVarBddArray = info->quantifyVarBddArray;
1061      domainVarBddArray = info->domainVarBddArray;
1062    }
1063    newRelationArray = ImgClusterRelationArray(info->manager,
1064        info->functionData, info->option->trMethod, Img_Backward_c,
1065        info->trmOption, tmpRelationArray, domainVarBddArray,
1066        quantifyVarBddArray, info->rangeVarBddArray,
1067        NIL(array_t *), NIL(array_t *), 0);
1068    if (info->preKeepPiInTr) {
1069      array_free(quantifyVarBddArray);
1070      array_free(domainVarBddArray);
1071    }
1072  } else {
1073    newRelationArray = ImgClusterRelationArray(info->manager,
1074        info->functionData, info->option->trMethod, Img_Forward_c,
1075        info->trmOption, tmpRelationArray, info->domainVarBddArray,
1076        info->quantifyVarBddArray, info->rangeVarBddArray,
1077        NIL(array_t *), NIL(array_t *), 0);
1078  }
1079  mdd_array_free(tmpRelationArray);
1080
1081  product1 = mdd_one(info->manager);
1082  for (i = 0; i < array_n(newRelationArray); i++) {
1083    relation = array_fetch(mdd_t *, newRelationArray, i);
1084    tmp = product1;
1085    product1 = mdd_and(tmp, relation, 1, 1);
1086    mdd_free(tmp);
1087  }
1088  mdd_array_free(newRelationArray);
1089
1090  if (cofactorCube && abstractCube) {
1091    newRelationArray = ImgGetCofactoredAbstractedRelationArray(info->manager,
1092                                relationArray, cofactorCube, abstractCube);
1093  } else
1094    newRelationArray = relationArray;
1095
1096  product2 = mdd_one(info->manager);
1097  for (i = 0; i < array_n(newRelationArray); i++) {
1098    relation = array_fetch(mdd_t *, newRelationArray, i);
1099    tmp = product2;
1100    product2 = mdd_and(tmp, relation, 1, 1);
1101    mdd_free(tmp);
1102  }
1103
1104  if (newRelationArray != relationArray)
1105    mdd_array_free(newRelationArray);
1106
1107  if (mdd_equal(product1, product2))
1108    equal = 1;
1109  else
1110    equal = 0;
1111
1112  mdd_free(product1);
1113  mdd_free(product2);
1114
1115  return(equal);
1116}
1117
1118
1119/**Function********************************************************************
1120
1121  Synopsis    [Checks whether a vector corresponds to its relation array.]
1122
1123  Description [Checks whether a vector corresponds to its relation array.
1124  This function is used only for debugging with image_cluster_size = 1.
1125  Checks each function vector whether its relation exists in the transition
1126  relation.]
1127
1128  SideEffects []
1129
1130******************************************************************************/
1131int
1132ImgCheckMatching(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray)
1133{
1134  int                   i, equal = 1;
1135  mdd_t                 *var, *relation;
1136  ImgComponent_t        *comp;
1137  st_table              *relationTable;
1138  int                   *ptr;
1139
1140  relationTable = st_init_table(st_ptrcmp, st_ptrhash);
1141
1142  for (i = 0; i < array_n(relationArray); i++) {
1143    relation = array_fetch(mdd_t *, relationArray, i);
1144    ptr = (int *)bdd_pointer(relation);
1145    st_insert(relationTable, (char *)ptr, NULL);
1146  }
1147
1148  for (i = 0; i < array_n(vector); i++) {
1149    comp = array_fetch(ImgComponent_t *, vector, i);
1150    if (comp->intermediate)
1151      relation = mdd_xnor(comp->var, comp->func);
1152    else {
1153      var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1154      relation = mdd_xnor(var, comp->func);
1155      mdd_free(var);
1156    }
1157    ptr = (int *)bdd_pointer(relation);
1158    if (!st_lookup(relationTable, (char *)ptr, NULL)) {
1159      if (comp->intermediate) {
1160        fprintf(vis_stderr,
1161                "Error : relation of varId[%d - intermediate] not found\n",
1162                (int)bdd_top_var_id(comp->var));
1163      } else {
1164        fprintf(vis_stderr, "Error : relation of varId[%d] not found\n",
1165                (int)bdd_top_var_id(comp->var));
1166      }
1167      equal = 0;
1168    }
1169    mdd_free(relation);
1170  }
1171
1172  st_free_table(relationTable);
1173  return(equal);
1174}
1175
1176
1177/*---------------------------------------------------------------------------*/
1178/* Definition of static functions                                            */
1179/*---------------------------------------------------------------------------*/
1180
1181
1182/**Function********************************************************************
1183
1184  Synopsis    [Computes variable lifetime lambda.]
1185
1186  Description [Computes variable lifetime lambda. newRelationFlag is 1 when
1187  relationArray is made from the function vector directly, in other words,
1188  relationArray is an array of next state functions in this case.]
1189
1190  SideEffects []
1191
1192******************************************************************************/
1193static float
1194ComputeSupportLambda(ImgTfmInfo_t *info, array_t *relationArray,
1195                        mdd_t *cofactorCube, mdd_t *abstractCube,
1196                        mdd_t *from, array_t *vector, int newRelationFlag,
1197                        int preFlag, float *improvedLambda)
1198{
1199  array_t               *newRelationArray, *clusteredRelationArray;
1200  ImgComponent_t        *comp;
1201  int                   i, j, nVars, nSupports;
1202  mdd_t                 *newFrom, *var;
1203  char                  *support;
1204  array_t               *smoothVarsBddArray, *introducedVarsBddArray;
1205  array_t               *domainVarsBddArray;
1206  array_t               *smoothSchedule, *smoothVars;
1207  float                 lambda;
1208  int                   size, total, lifetime;
1209  Img_DirectionType     direction;
1210  int                   lambdaWithFrom, prevArea;
1211  array_t               *orderedRelationArray;
1212  int                   nIntroducedVars;
1213  int                   *highest, *lowest;
1214  mdd_t                 *relation;
1215  int                   asIs;
1216
1217  if (cofactorCube && abstractCube) {
1218    newRelationArray = ImgGetCofactoredAbstractedRelationArray(info->manager,
1219                              relationArray, cofactorCube, abstractCube);
1220    if (from && info->option->lambdaWithFrom) {
1221      if (preFlag)
1222        newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
1223      else
1224        newFrom = mdd_dup(from);
1225      array_insert_last(mdd_t *, newRelationArray, newFrom);
1226      lambdaWithFrom = 1;
1227    } else {
1228      lambdaWithFrom = 0;
1229      newFrom = NIL(mdd_t);
1230    }
1231  } else {
1232    if (from && info->option->lambdaWithFrom) {
1233      if (newRelationFlag) {
1234        newRelationArray = relationArray;
1235        if (preFlag)
1236          newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
1237        else
1238          newFrom = from;
1239      } else {
1240        /* We don't want to modify the original relation array */
1241        newRelationArray = mdd_array_duplicate(relationArray);
1242        if (preFlag)
1243          newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c);
1244        else
1245          newFrom = mdd_dup(from);
1246      }
1247      array_insert_last(mdd_t *, newRelationArray, newFrom);
1248      lambdaWithFrom = 1;
1249    } else {
1250      newRelationArray = relationArray;
1251      newFrom = NIL(mdd_t);
1252      lambdaWithFrom = 0;
1253    }
1254  }
1255
1256  if (vector) {
1257    for (i = 0; i < array_n(vector); i++) {
1258      comp = array_fetch(ImgComponent_t *, vector, i);
1259      array_insert_last(mdd_t *, newRelationArray, mdd_dup(comp->func));
1260    }
1261  }
1262
1263  nVars = info->nVars;
1264  support = ALLOC(char, sizeof(char) * nVars);
1265  memset(support, 0, sizeof(char) * nVars);
1266
1267  comp = ImgComponentAlloc(info);
1268  for (i = 0; i < array_n(newRelationArray); i++) {
1269    comp->func = array_fetch(mdd_t *, newRelationArray, i);;
1270    ImgSupportClear(info, comp->support);
1271    ImgComponentGetSupport(comp);
1272    for (j = 0; j < nVars; j++)
1273      support[j] = support[j] | comp->support[j];
1274  }
1275  comp->func = NIL(mdd_t);
1276  ImgComponentFree(comp);
1277
1278  nSupports = 0;
1279  smoothVarsBddArray = array_alloc(mdd_t *, 0);
1280  domainVarsBddArray = array_alloc(mdd_t *, 0);
1281  introducedVarsBddArray = array_alloc(mdd_t *, 0);
1282  for (i = 0; i < nVars; i++) {
1283    if (support[i]) {
1284      var = bdd_var_with_index(info->manager, i);
1285      if (preFlag) {
1286        if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
1287          if (lambdaWithFrom)
1288            array_insert_last(mdd_t *, smoothVarsBddArray, var);
1289          else
1290            array_insert_last(mdd_t *, domainVarsBddArray, var);
1291          if (info->option->preLambdaMode == 0 ||
1292              info->option->preLambdaMode == 2)
1293            nSupports++;
1294        } else {
1295          if (info->preKeepPiInTr) {
1296            if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
1297                        NIL(char *))) {
1298              array_insert_last(mdd_t *, introducedVarsBddArray, var);
1299              nSupports++;
1300            } else if (info->intermediateVarsTable &&
1301                        st_lookup(info->intermediateVarsTable, (char *)(long)i,
1302                                NIL(char *))) {
1303              array_insert_last(mdd_t *, smoothVarsBddArray, var);
1304              nSupports++;
1305            } else { /* ps variables */
1306              array_insert_last(mdd_t *, introducedVarsBddArray, var);
1307              if (info->option->preLambdaMode != 0)
1308                nSupports++;
1309            }
1310          } else {
1311            if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
1312                          NIL(char *)) ||
1313                (info->intermediateVarsTable &&
1314                 st_lookup(info->intermediateVarsTable, (char *)(long)i,
1315                           NIL(char *)))) {
1316              array_insert_last(mdd_t *, smoothVarsBddArray, var);
1317              nSupports++;
1318            } else { /* ps variables */
1319              array_insert_last(mdd_t *, introducedVarsBddArray, var);
1320              if (info->option->preLambdaMode != 0)
1321                nSupports++;
1322            }
1323          }
1324        }
1325      } else { /* image computation */
1326        if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
1327          array_insert_last(mdd_t *, introducedVarsBddArray, var);
1328          if (info->option->lambdaMode == 2)
1329            nSupports++;
1330        } else {
1331          if (lambdaWithFrom)
1332            array_insert_last(mdd_t *, smoothVarsBddArray, var);
1333          else {
1334            if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
1335                          NIL(char *)) ||
1336                (info->intermediateVarsTable &&
1337                 st_lookup(info->intermediateVarsTable, (char *)(long)i,
1338                           NIL(char *)))) {
1339              array_insert_last(mdd_t *, smoothVarsBddArray, var);
1340            } else
1341              array_insert_last(mdd_t *, domainVarsBddArray, var);
1342          }
1343          nSupports++;
1344        }
1345      }
1346    }
1347  }
1348
1349  if (preFlag)
1350    direction = Img_Backward_c;
1351  else
1352    direction = Img_Forward_c;
1353
1354  if (info->option->lambdaFromMlp) {
1355    FREE(support);
1356    if (info->option->lambdaWithClustering) {
1357      ImgMlpClusterRelationArray(info->manager, info->functionData,
1358                        newRelationArray, domainVarsBddArray,
1359                        smoothVarsBddArray, introducedVarsBddArray,
1360                        direction, &clusteredRelationArray, NIL(array_t *),
1361                        info->trmOption);
1362      if (newRelationArray != relationArray)
1363        mdd_array_free(newRelationArray);
1364      newRelationArray = clusteredRelationArray;
1365    }
1366    prevArea = info->prevTotal;
1367    asIs = newRelationFlag ? 0 : 1; /* 0 when relationArray is an array of
1368                                       functions, i.e. without next state
1369                                       variables */
1370    lambda = ImgMlpComputeLambda(info->manager, newRelationArray,
1371                        domainVarsBddArray, smoothVarsBddArray,
1372                        introducedVarsBddArray, direction,
1373                        info->option->lambdaMode, asIs, &prevArea,
1374                        improvedLambda, info->trmOption);
1375    info->prevTotal = prevArea;
1376  } else {
1377    smoothSchedule = ImgGetQuantificationSchedule(info->manager,
1378                        info->functionData, info->option->trMethod,
1379                        direction, info->trmOption, newRelationArray,
1380                        smoothVarsBddArray, domainVarsBddArray,
1381                        introducedVarsBddArray,
1382                        info->option->lambdaWithClustering,
1383                        &orderedRelationArray);
1384
1385    if (direction == Img_Forward_c) {
1386      size = array_n(smoothSchedule);
1387      lifetime = 0;
1388      if (info->option->lambdaMode == 0) { /* total lifetime (lambda) */
1389        for (i = 1; i < size; i++) {
1390          smoothVars = array_fetch(array_t *, smoothSchedule, i);
1391          lifetime += array_n(smoothVars) * i;
1392        }
1393        total = nSupports * (size - 1);
1394      } else if (info->option->lambdaMode == 1) { /* active lifetime (lambda) */
1395        lowest = ALLOC(int, sizeof(int) * nVars);
1396        for (i = 0; i < nVars; i++)
1397          lowest[i] = nVars;
1398        highest = ALLOC(int, sizeof(int) * nVars);
1399        memset(highest, 0, sizeof(int) * nVars);
1400
1401        comp = ImgComponentAlloc(info);
1402        for (i = 0; i < size - 1; i++) {
1403          relation = array_fetch(mdd_t *, orderedRelationArray, i);
1404          comp->func = relation;
1405          ImgSupportClear(info, comp->support);
1406          ImgComponentGetSupport(comp);
1407          for (j = 0; j < nVars; j++) {
1408            if (!comp->support[j])
1409              continue;
1410            if (st_lookup(info->rangeVarsTable, (char *)(long)j, NIL(char *)))
1411              continue;
1412            if (i < lowest[j])
1413              lowest[j] = i;
1414            if (i > highest[j])
1415              highest[j] = i;
1416          }
1417        }
1418        comp->func = NIL(mdd_t);
1419        ImgComponentFree(comp);
1420
1421        for (i = 0; i < nVars; i++) {
1422          if (lowest[i] == nVars)
1423            continue;
1424          if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
1425            continue;
1426          lifetime += highest[i] - lowest[i] + 1;
1427        }
1428
1429        if (newRelationFlag)
1430          lifetime += array_n(newRelationArray);
1431        total = nSupports * (size - 1);
1432
1433        FREE(lowest);
1434        FREE(highest);
1435      } else { /* total lifetime (lambda) with introduced variables */
1436        for (i = 1; i < size; i++) {
1437          smoothVars = array_fetch(array_t *, smoothSchedule, i);
1438          lifetime += array_n(smoothVars) * i;
1439        }
1440
1441        if (newRelationFlag) {
1442          nIntroducedVars = array_n(newRelationArray);
1443          lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
1444        } else {
1445          comp = ImgComponentAlloc(info);
1446          for (i = 0; i < size - 1; i++) {
1447            relation = array_fetch(mdd_t *, orderedRelationArray, i);
1448            comp->func = relation;
1449            ImgSupportClear(info, comp->support);
1450            ImgComponentGetSupport(comp);
1451            nIntroducedVars = 0;
1452            for (j = 0; j < nVars; j++) {
1453              if (!comp->support[j])
1454                continue;
1455              if (st_lookup(info->rangeVarsTable, (char *)(long)j, NIL(char *)))
1456                nIntroducedVars++;
1457            }
1458            lifetime += (size - i - 1) * nIntroducedVars;
1459          }
1460          comp->func = NIL(mdd_t);
1461          ImgComponentFree(comp);
1462        }
1463        total = nSupports * (size - 1);
1464      }
1465      mdd_array_array_free(smoothSchedule);
1466    } else if (info->option->preLambdaMode == 0) { /* total lifetime (lambda) */
1467      /* direction == Img_Backward_c */
1468      size = array_n(smoothSchedule);
1469      lifetime = 0;
1470      for (i = 1; i < size; i++) {
1471        smoothVars = array_fetch(array_t *, smoothSchedule, i);
1472        lifetime += array_n(smoothVars) * i;
1473      }
1474      total = nSupports * (size - 1);
1475      mdd_array_array_free(smoothSchedule);
1476    } else { /* direction == Img_Backward_c */
1477      size = array_n(smoothSchedule);
1478      mdd_array_array_free(smoothSchedule);
1479      lifetime = 0;
1480
1481      lowest = ALLOC(int, sizeof(int) * nVars);
1482      for (i = 0; i < nVars; i++)
1483        lowest[i] = nVars;
1484      highest = ALLOC(int, sizeof(int) * nVars);
1485      memset(highest, 0, sizeof(int) * nVars);
1486
1487      comp = ImgComponentAlloc(info);
1488      for (i = 0; i < size - 1; i++) {
1489        relation = array_fetch(mdd_t *, orderedRelationArray, i);
1490        comp->func = relation;
1491        ImgSupportClear(info, comp->support);
1492        ImgComponentGetSupport(comp);
1493        for (j = 0; j < nVars; j++) {
1494          if (!comp->support[j])
1495            continue;
1496          if (i < lowest[j])
1497            lowest[j] = i;
1498          if (i > highest[j])
1499            highest[j] = i;
1500        }
1501      }
1502      comp->func = NIL(mdd_t);
1503      ImgComponentFree(comp);
1504
1505      if (info->option->preLambdaMode == 1) { /* active lifetime (lambda) */
1506        for (i = 0; i < nVars; i++) {
1507          if (lowest[i] == nVars)
1508            continue;
1509          if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)) ||
1510                st_lookup(info->quantifyVarsTable, (char *)(long)i,
1511                               NIL(char *)) ||
1512                (info->intermediateVarsTable &&
1513                 st_lookup(info->intermediateVarsTable, (char *)(long)i,
1514                               NIL(char *)))) {
1515            lifetime += highest[i] - lowest[i] + 1;
1516          }
1517        }
1518        if (newRelationFlag)
1519          lifetime += array_n(newRelationArray);
1520        total = nSupports * (size - 1);
1521      } else if (info->option->preLambdaMode == 2) {
1522        /* total lifetime (lambda) with introduced variables */
1523        for (i = 0; i < nVars; i++) {
1524          if (lowest[i] == nVars)
1525            continue;
1526          if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)) ||
1527              st_lookup(info->quantifyVarsTable, (char *)(long)i,
1528                        NIL(char *)) ||
1529              (info->intermediateVarsTable &&
1530               st_lookup(info->intermediateVarsTable, (char *)(long)i,
1531                        NIL(char *)))) {
1532            lifetime += highest[i] + 1;
1533          } else {
1534            lifetime += size - lowest[i] - 1;
1535          }
1536        }
1537        if (newRelationFlag) {
1538          nIntroducedVars = array_n(newRelationArray);
1539          lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
1540        }
1541        total = nSupports * (size - 1);
1542      } else { /* total lifetime (lambda) with ps/pi variables */
1543        for (i = 0; i < nVars; i++) {
1544          if (lowest[i] == nVars)
1545            continue;
1546          if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
1547            continue;
1548          if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
1549                        NIL(char *)) ||
1550              (info->intermediateVarsTable &&
1551               st_lookup(info->intermediateVarsTable, (char *)(long)i,
1552                        NIL(char *)))) {
1553            lifetime += highest[i] + 1;
1554          } else {
1555            lifetime += size - lowest[i] - 1;
1556          }
1557        }
1558        if (newRelationFlag) {
1559          nIntroducedVars = array_n(newRelationArray);
1560          lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2;
1561        }
1562        total = nSupports * (size - 1);
1563      }
1564
1565      FREE(lowest);
1566      FREE(highest);
1567    }
1568
1569    FREE(support);
1570    mdd_array_free(orderedRelationArray);
1571
1572    if (total == 0.0) {
1573      lambda = 0.0;
1574      *improvedLambda = 0.0;
1575    } else {
1576      lambda = (float)lifetime / (float)total;
1577      if (info->prevTotal) {
1578        *improvedLambda = info->prevLambda -
1579                          (float)lifetime / (float)info->prevTotal;
1580      } else
1581        *improvedLambda = 0.0;
1582    }
1583    info->prevTotal = total;
1584  }
1585
1586  mdd_array_free(smoothVarsBddArray);
1587  mdd_array_free(domainVarsBddArray);
1588  mdd_array_free(introducedVarsBddArray);
1589  if (newRelationArray != relationArray)
1590    mdd_array_free(newRelationArray);
1591  if (newRelationFlag && from && info->option->lambdaWithFrom &&
1592        newFrom != from) {
1593    mdd_free(newFrom);
1594  }
1595
1596  if (info->option->verbosity >= 2) {
1597    if (preFlag)
1598      fprintf(vis_stdout, "** tfm info: lambda for preimage = %.2f\n", lambda);
1599    else
1600      fprintf(vis_stdout, "** tfm info: lambda for image = %.2f\n", lambda);
1601  }
1602
1603  info->prevLambda = lambda;
1604  return(lambda);
1605}
Note: See TracBrowser for help on using the repository browser.