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

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

vis2.3
File size: 119.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [imgTfm.c]
4
5  PackageName [img]
6
7  Synopsis    [Routines for image and preimage computations using transition
8  function method.]
9
10  Description [Transition function method is implemented as a part of the
11  hybrid image computation (refer to "To Split or to Conjoin: The Question
12  in Image Computation", In-Ho Moon et. al. in the proceedings of DAC00.)
13  The hybrid method starts with transition function method based on splitting,
14  then switches to transition relation method based on conjunctions. The
15  decision is based on computing variable lifetimes from dependence matrix
16  dynamically at every recursion.
17 
18  The transition function method itself also can be used as an image_method,
19  however we do not recommend to use this method for general purpose. This
20  method can be used for experimental purpose. However, this method performs
21  quite well for most approximate reachability and some examples on exact
22  reachability.
23
24  There are two image computation methods in transition function method;
25  input splitting (default) and output splitting. Also three preimage
26  computation methods in transition function method are implemented; domain
27  cofactoring (default), sequential substitution, and simultaneous substitution.
28
29  The performance of transition function method is significantly depending on
30  both the choice of splitting variable and the use of image cache. However,
31  the hybrid method does not use image cache by default. Since the recursion
32  depths are bounded (not so deep) in the hybrid method, the cache hit ratio
33  is usually very low.
34
35  The implementation of the transition function method and the hybrid method
36  is very complicate since there are so many options. For details, try
37  print_tfm_options and print_hybrid_options commands in vis, also more
38  detailed descriptions for all options can be read by using help in vis
39  for the two commands.
40 
41  The hybrid method can start with either only function vector or only
42  transition relation, as well as with both function vector and transition
43  relation. In case of starting with only the function vector, when we switch
44  to conjoin, transition relation is built on demand. This method may consume
45  less memory than the others, but it may take more time since it is a big
46  overhead to build transition relation at every conjunction. To reduce this
47  overhead, the hybrid method can start with both function vector and transition
48  relation (default). In the presense of non-determinism, the hybrid mehtod
49  also can start with only transition relation without the function vector.]
50
51  SeeAlso     [imgTfmFwd.c imgTfmBwd.c imgTfmUtil.c imgTfmCache.c]
52
53  Author      [In-Ho Moon]
54
55  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado.
56  All rights reserved.
57
58  Permission is hereby granted, without written agreement and without license
59  or royalty fees, to use, copy, modify, and distribute this software and its
60  documentation for any purpose, provided that the above copyright notice and
61  the following two paragraphs appear in all copies of this software.
62
63  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
64  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
65  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
66  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
67
68  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
69  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
70  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
71  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
72  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
73
74******************************************************************************/
75#include "imgInt.h"
76
77static char rcsid[] UNUSED = "$Id: imgTfm.c,v 1.93 2005/04/23 14:30:54 jinh Exp $";
78
79/*---------------------------------------------------------------------------*/
80/* Constant declarations                                                     */
81/*---------------------------------------------------------------------------*/
82
83/*---------------------------------------------------------------------------*/
84/* Type declarations                                                         */
85/*---------------------------------------------------------------------------*/
86
87/*---------------------------------------------------------------------------*/
88/* Structure declarations                                                    */
89/*---------------------------------------------------------------------------*/
90
91/*---------------------------------------------------------------------------*/
92/* Variable declarations                                                     */
93/*---------------------------------------------------------------------------*/
94
95static  st_table        *HookInfoList; /* adds a hook function to flush image
96                                          cache before veriable reordering */
97static  int             nHookInfoList; /* the number of hook functions */
98
99/*---------------------------------------------------------------------------*/
100/* Macro declarations                                                        */
101/*---------------------------------------------------------------------------*/
102
103
104/**AutomaticStart*************************************************************/
105
106/*---------------------------------------------------------------------------*/
107/* Static function prototypes                                                */
108/*---------------------------------------------------------------------------*/
109
110static ImgTfmInfo_t * TfmInfoStructAlloc(Img_MethodType method);
111static int CompareIndex(const void *e1, const void *e2);
112static int HookInfoFunction(bdd_manager *mgr, char *str, void *method);
113static array_t * ChoosePartialVars(ImgTfmInfo_t *info, array_t *vector, int nPartialVars, int partialMethod);
114static void PrintRecursionStatistics(ImgTfmInfo_t *info, int preFlag);
115static void PrintFoundVariableStatistics(ImgTfmInfo_t *info, int preFlag);
116static void GetRecursionStatistics(ImgTfmInfo_t *info, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp);
117static int ReadSetIntValue(char *string, int l, int u, int defaultValue);
118static boolean ReadSetBooleanValue(char *string, boolean defaultValue);
119static void FindIntermediateVarsRecursively(ImgTfmInfo_t *info, mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *vector, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray);
120static void GetIntermediateRelationsRecursively(mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *relationArray, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray);
121static int CheckNondeterminism(Ntk_Network_t *network);
122static array_t * TfmCreateBitVector(ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars);
123static array_t * TfmCreateBitRelationArray(ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars);
124static void TfmSetupPartialTransitionRelation(ImgTfmInfo_t *info, array_t **partialRelationArray);
125static void TfmBuildRelationArray(ImgTfmInfo_t *info, ImgFunctionData_t *functionData, array_t *bitRelationArray, Img_DirectionType directionType, int writeMatrix);
126static void RebuildTransitionRelation(ImgTfmInfo_t *info, Img_DirectionType directionType);
127static void MinimizeTransitionFunction(array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus);
128static void AddDontCareToTransitionFunction(array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus);
129
130/**AutomaticEnd***************************************************************/
131
132
133/*---------------------------------------------------------------------------*/
134/* Definition of exported functions                                          */
135/*---------------------------------------------------------------------------*/
136
137
138/**Function********************************************************************
139
140  Synopsis    [Gets the statistics of recursions of transition function
141  method.]
142
143  Description [Gets the statistics of recursions of transition function
144  method.]
145
146  SideEffects []
147
148  SeeAlso     []
149
150******************************************************************************/
151int
152Img_TfmGetRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag,
153                              int *nRecurs, int *nLeaves, int *nTurns,
154                              float *averageDepth, int *maxDepth, int *nDecomps,
155                              int *topDecomp, int *maxDecomp,
156                              float *averageDecomp)
157{
158  ImgTfmInfo_t  *info;
159
160  if (imageInfo->methodType != Img_Tfm_c &&
161      imageInfo->methodType != Img_Hybrid_c) {
162    return(0);
163  }
164
165  info = (ImgTfmInfo_t *)imageInfo->methodData;
166  if (preFlag) {
167    *nRecurs = info->nRecursionB;
168    *nLeaves = info->nLeavesB;
169    *nTurns = info->nTurnsB;
170    *averageDepth = info->averageDepthB;
171    *maxDepth = info->maxDepthB;
172    *nDecomps = 0;
173    *topDecomp = 0;
174    *maxDecomp = 0;
175    *averageDecomp = 0.0;
176  } else {
177    *nRecurs = info->nRecursion;
178    *nLeaves = info->nLeaves;
179    *nTurns = info->nTurns;
180    *averageDepth = info->averageDepth;
181    *maxDepth = info->maxDepth;
182    *nDecomps = info->nDecomps;
183    *topDecomp = info->topDecomp;
184    *maxDecomp = info->maxDecomp;
185    *averageDecomp = info->averageDecomp;
186  }
187  return(1);
188}
189
190
191/**Function********************************************************************
192
193  Synopsis    [Prints the statistics of image cache and recursions in
194  in transition function method.]
195
196  Description [Prints the statistics of image cache and recursions in
197  in transition function method.]
198
199  SideEffects []
200
201  SeeAlso     []
202
203******************************************************************************/
204void
205Img_TfmPrintStatistics(Img_ImageInfo_t *imageInfo, Img_DirectionType dir)
206{
207  if (dir == Img_Forward_c || dir == Img_Both_c) {
208    Img_TfmPrintCacheStatistics(imageInfo, 0);
209    Img_TfmPrintRecursionStatistics(imageInfo, 0);
210  }
211  if (dir == Img_Backward_c || dir == Img_Both_c) {
212    Img_TfmPrintCacheStatistics(imageInfo, 1);
213    Img_TfmPrintRecursionStatistics(imageInfo, 1);
214  }
215}
216
217
218/**Function********************************************************************
219
220  Synopsis    [Prints the statistics of recursions for transition function
221  method.]
222
223  Description [Prints the statistics of recursions for transition function
224  method.]
225
226  SideEffects []
227
228  SeeAlso     []
229
230******************************************************************************/
231void
232Img_TfmPrintRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag)
233{
234  float avgDepth, avgDecomp;
235  int   nRecurs, nLeaves, nTurns, nDecomps, topDecomp, maxDecomp;
236  int   maxDepth;
237
238  (void) Img_TfmGetRecursionStatistics(imageInfo, preFlag, &nRecurs, &nLeaves,
239                                &nTurns, &avgDepth, &maxDepth, &nDecomps,
240                                &topDecomp, &maxDecomp, &avgDecomp);
241  if (preFlag)
242    fprintf(vis_stdout, "** recursion statistics of splitting (preImg) **\n");
243  else
244    fprintf(vis_stdout, "** recursion statistics of splitting (img) **\n");
245  fprintf(vis_stdout, "# recursions = %d\n", nRecurs);
246  fprintf(vis_stdout, "# leaves = %d\n", nLeaves);
247  fprintf(vis_stdout, "# turns = %d\n", nTurns);
248  fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n",
249          avgDepth, maxDepth);
250  if (!preFlag) {
251    fprintf(vis_stdout,
252            "# decompositions = %d (top = %d, max = %d, average = %g)\n",
253            nDecomps, topDecomp, maxDecomp, avgDecomp);
254  }
255}
256
257
258/**Function********************************************************************
259
260  Synopsis    [Prints the options for image computation using transition
261  function method.]
262
263  Description [Prints the options for image computation using transition
264  function method.]
265
266  SideEffects []
267
268  SeeAlso     []
269
270******************************************************************************/
271void
272Img_PrintTfmOptions(void)
273{
274  ImgTfmOption_t        *options;
275  Img_MethodType        method;
276  char                  *flagValue, dummy[40];
277
278  flagValue = Cmd_FlagReadByName("image_method");
279  if (flagValue) {
280    if (strcmp(flagValue, "hybrid") == 0)
281      method = Img_Hybrid_c;
282    else
283      method = Img_Tfm_c;
284  } else
285    method = Img_Tfm_c;
286
287  options = ImgTfmGetOptions(method);
288
289  switch (options->splitMethod) {
290  case 0 :
291    sprintf(dummy, "input split");
292    break;
293  case 1 :
294    sprintf(dummy, "output split");
295    break;
296  case 2 :
297    sprintf(dummy, "mixed");
298    break;
299  case 3 :
300    sprintf(dummy, "hybrid");
301    break;
302  default :
303    sprintf(dummy, "invalid");
304    break;
305  }
306  fprintf(vis_stdout, "TFM: tfm_split_method = %d (%s)\n",
307          options->splitMethod, dummy);
308
309  switch (options->inputSplit) {
310  case 0 :
311    sprintf(dummy, "support before splitting");
312    break;
313  case 1 :
314    sprintf(dummy, "support after splitting");
315    break;
316  case 2 :
317    sprintf(dummy, "estimate BDD size after splitting");
318    break;
319  case 3 :
320    sprintf(dummy, "top variable");
321    break;
322  default :
323    sprintf(dummy, "invalid");
324    break;
325  }
326  fprintf(vis_stdout, "TFM: tfm_input_split = %d (%s)\n",
327          options->inputSplit, dummy);
328
329  if (options->piSplitFlag)
330    sprintf(dummy, "yes");
331  else
332    sprintf(dummy, "no");
333  fprintf(vis_stdout, "TFM: tfm_pi_split_flag = %s\n", dummy);
334
335  /* whether to convert image computation to range computation */
336  switch (options->rangeComp) {
337  case 0 :
338    sprintf(dummy, "do not convert");
339    break;
340  case 1 :
341    sprintf(dummy, "convert to range computation");
342    break;
343  case 2 :
344    sprintf(dummy, "convert with threshold");
345    break;
346  default :
347    sprintf(dummy, "invalid");
348    break;
349  }
350  fprintf(vis_stdout, "TFM: tfm_range_comp = %d (%s)\n",
351          options->rangeComp, dummy);
352
353  fprintf(vis_stdout, "TFM: tfm_range_threshold = %d\n",
354          options->rangeThreshold);
355
356  fprintf(vis_stdout, "TFM: tfm_range_try_threshold = %d\n",
357          options->rangeTryThreshold);
358
359  if (options->rangeCheckReorder)
360    sprintf(dummy, "yes");
361  else
362    sprintf(dummy, "no");
363  fprintf(vis_stdout, "TFM: tfm_range_check_reorder = %s\n", dummy);
364
365  switch (options->tieBreakMode) {
366  case 0 :
367    sprintf(dummy, "closest variable to top");
368    break;
369  case 1 :
370    sprintf(dummy, "smallest BDD size after splitting");
371    break;
372  default :
373    sprintf(dummy, "invalid");
374    break;
375  }
376  fprintf(vis_stdout, "TFM: tfm_tie_break_mode = %d (%s)\n",
377          options->tieBreakMode, dummy);
378
379  switch (options->outputSplit) {
380  case 0 :
381    sprintf(dummy, "smallest BDD size");
382    break;
383  case 1 :
384    sprintf(dummy, "largest BDD size");
385    break;
386  case 2 :
387    sprintf(dummy, "top variable");
388    break;
389  default :
390    sprintf(dummy, "invalid");
391    break;
392  }
393  fprintf(vis_stdout, "TFM: tfm_output_split = %d (%s)\n",
394          options->outputSplit, dummy);
395
396  fprintf(vis_stdout, "TFM: tfm_turn_depth = %d\n",
397          options->turnDepth);
398
399  if (options->findDecompVar)
400    sprintf(dummy, "yes");
401  else
402    sprintf(dummy, "no");
403  fprintf(vis_stdout, "TFM: tfm_find_decomp_var = %s\n", dummy);
404
405  if (options->sortVectorFlag)
406    sprintf(dummy, "yes");
407  else
408    sprintf(dummy, "no");
409  fprintf(vis_stdout, "TFM: tfm_sort_vector_flag = %s\n", dummy);
410
411  if (options->printStatistics)
412    sprintf(dummy, "yes");
413  else
414    sprintf(dummy, "no");
415  fprintf(vis_stdout, "TFM: tfm_print_stats = %s\n", dummy);
416
417  if (options->printBddSize)
418    sprintf(dummy, "yes");
419  else
420    sprintf(dummy, "no");
421  fprintf(vis_stdout, "TFM: tfm_print_bdd_size = %s\n", dummy);
422
423  if (options->splitCubeFunc)
424    sprintf(dummy, "yes");
425  else
426    sprintf(dummy, "no");
427  fprintf(vis_stdout, "TFM: tfm_split_cube_func = %s\n", dummy);
428
429  switch (options->findEssential) {
430  case 0 :
431    sprintf(dummy, "off");
432    break;
433  case 1 :
434    sprintf(dummy, "on");
435    break;
436  case 2 :
437    sprintf(dummy, "dynamic");
438    break;
439  default :
440    sprintf(dummy, "invalid");
441    break;
442  }
443  fprintf(vis_stdout, "TFM: tfm_find_essential = %d (%s)\n",
444          options->findEssential, dummy);
445
446  switch (options->printEssential) {
447  case 0 :
448    sprintf(dummy, "off");
449    break;
450  case 1 :
451    sprintf(dummy, "at the end");
452    break;
453  case 2 :
454    sprintf(dummy, "at every image computation");
455    break;
456  default :
457    sprintf(dummy, "invalid");
458    break;
459  }
460  fprintf(vis_stdout, "TFM: tfm_print_essential = %d (%s)\n",
461          options->printEssential, dummy);
462
463  switch (options->useCache) {
464  case 0 :
465    sprintf(dummy, "off");
466    break;
467  case 1 :
468    sprintf(dummy, "on");
469    break;
470  case 2 :
471    sprintf(dummy, "store all intermediate");
472    break;
473  default :
474    sprintf(dummy, "invalid");
475    break;
476  }
477  fprintf(vis_stdout, "TFM: tfm_use_cache = %d (%s)\n",
478          options->useCache, dummy);
479
480  if (options->globalCache)
481    sprintf(dummy, "yes");
482  else
483    sprintf(dummy, "no");
484  fprintf(vis_stdout, "TFM: tfm_global_cache = %s\n", dummy);
485
486  fprintf(vis_stdout, "TFM: tfm_max_chain_length = %d\n",
487          options->maxChainLength);
488
489  fprintf(vis_stdout, "TFM: tfm_init_cache_size = %d\n",
490          options->initCacheSize);
491
492  switch (options->autoFlushCache) {
493  case 0 :
494    sprintf(dummy, "when requested");
495    break;
496  case 1 :
497    sprintf(dummy, "at the end of image computation");
498    break;
499  case 2 :
500    sprintf(dummy, "before reordering");
501    break;
502  default :
503    sprintf(dummy, "invalid");
504    break;
505  }
506  fprintf(vis_stdout, "TFM: tfm_auto_flush_cache = %d (%s)\n",
507          options->autoFlushCache, dummy);
508
509  if (options->composeIntermediateVars)
510    sprintf(dummy, "yes");
511  else
512    sprintf(dummy, "no");
513  fprintf(vis_stdout, "TFM: tfm_compose_intermediate_vars = %s\n", dummy);
514
515  switch (options->preSplitMethod) {
516  case 0 :
517    sprintf(dummy, "input split");
518    break;
519  case 1 :
520    sprintf(dummy, "output split");
521    break;
522  case 2 :
523    sprintf(dummy, "mixed");
524    break;
525  case 3 :
526    sprintf(dummy, "substitution");
527    break;
528  case 4 :
529    sprintf(dummy, "hybrid");
530    break;
531  default :
532    sprintf(dummy, "invalid");
533    break;
534  }
535  fprintf(vis_stdout, "TFM: tfm_pre_split_method = %d (%s)\n",
536          options->preSplitMethod, dummy);
537
538  switch (options->preInputSplit) {
539  case 0 :
540    sprintf(dummy, "support before splitting");
541    break;
542  case 1 :
543    sprintf(dummy, "support after splitting");
544    break;
545  case 2 :
546    sprintf(dummy, "estimate BDD size after splitting");
547    break;
548  case 3 :
549    sprintf(dummy, "top variable");
550    break;
551  default :
552    sprintf(dummy, "invalid");
553    break;
554  }
555  fprintf(vis_stdout, "TFM: tfm_pre_input_split = %d (%s)\n",
556          options->preInputSplit, dummy);
557
558  switch (options->preOutputSplit) {
559  case 0 :
560    sprintf(dummy, "smallest BDD size");
561    break;
562  case 1 :
563    sprintf(dummy, "largest BDD size");
564    break;
565  case 2 :
566    sprintf(dummy, "top variable");
567    break;
568  default :
569    sprintf(dummy, "invalid");
570    break;
571  }
572  fprintf(vis_stdout, "TFM: tfm_pre_output_split = %d (%s)\n",
573          options->preOutputSplit, dummy);
574
575  switch (options->preDcLeafMethod) {
576  case 0 :
577    sprintf(dummy, "substitution");
578    break;
579  case 1 :
580    sprintf(dummy, "constraint cofactoring");
581    break;
582  case 2 :
583    sprintf(dummy, "hybrid");
584    break;
585  default :
586    sprintf(dummy, "invalid");
587    break;
588  }
589  fprintf(vis_stdout, "TFM: tfm_pre_dc_leaf_method = %d (%s)\n",
590          options->preDcLeafMethod, dummy);
591
592  if (options->preMinimize)
593    sprintf(dummy, "yes");
594  else
595    sprintf(dummy, "no");
596  fprintf(vis_stdout, "TFM: tfm_pre_minimize = %s\n", dummy);
597
598  fprintf(vis_stdout, "TFM: tfm_verbosity = %d\n",
599          options->verbosity);
600
601  FREE(options);
602}
603
604
605/*---------------------------------------------------------------------------*/
606/* Definition of internal functions                                          */
607/*---------------------------------------------------------------------------*/
608
609
610/**Function********************************************************************
611
612  Synopsis    [Initializes an image data structure for image
613  computation using transition function method.]
614
615  Description [Initialized an image data structure for image
616  computation using transition function method.]
617
618  SideEffects []
619
620******************************************************************************/
621void *
622ImgImageInfoInitializeTfm(void *methodData, ImgFunctionData_t * functionData,
623                          Img_DirectionType directionType,
624                          Img_MethodType method)
625{
626  int                   i;
627  int                   latches;
628  int                   variables, nVars;
629  array_t               *vector;
630  graph_t               *mddNetwork;
631  mdd_manager           *mddManager;
632  array_t               *rangeVarMddIdArray;
633  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
634  int                   index;
635  mdd_t                 *var;
636  char                  *flagValue;
637  char                  filename[20];
638  int                   composeIntermediateVars, findIntermediateVars;
639  int                   nonDeterministic;
640
641  if (info) {
642    if (info->option->useCache) {
643      if (directionType == Img_Forward_c || directionType == Img_Both_c) {
644        if (!info->imgCache)
645          ImgCacheInitTable(info, info->option->initCacheSize,
646                            info->option->globalCache, FALSE);
647      }
648      if (directionType == Img_Backward_c || directionType == Img_Both_c) {
649        if (!info->preCache)
650          ImgCacheInitTable(info, info->option->initCacheSize,
651                            info->option->globalCache, TRUE);
652      }
653    }
654    if (info->buildTR &&
655        (((directionType == Img_Forward_c || directionType == Img_Both_c) &&
656          !info->fwdClusteredRelationArray) ||
657         ((directionType == Img_Backward_c || directionType == Img_Both_c) &&
658          !info->bwdClusteredRelationArray))) {
659      TfmBuildRelationArray(info, functionData, NIL(array_t), directionType, 0);
660    }
661    return((void *)info);
662  }
663
664  mddNetwork = functionData->mddNetwork;
665  mddManager = Part_PartitionReadMddManager(mddNetwork);
666  rangeVarMddIdArray = functionData->rangeVars;
667
668  nonDeterministic = CheckNondeterminism(functionData->network);
669  if (nonDeterministic)
670    info = TfmInfoStructAlloc(Img_Hybrid_c);
671  else
672    info = TfmInfoStructAlloc(method);
673  info->nonDeterministic = nonDeterministic;
674  info->functionData = functionData;
675  info->quantifyVarsTable = st_init_table(st_numcmp, st_numhash);
676  for (i = 0; i < array_n(functionData->quantifyBddVars); i++) {
677    var = array_fetch(mdd_t *, functionData->quantifyBddVars, i);
678    index = (int)bdd_top_var_id(var);
679    st_insert(info->quantifyVarsTable, (char *)(long)index, NIL(char));
680  }
681  info->rangeVarsTable = st_init_table(st_numcmp, st_numhash);
682  for (i = 0; i < array_n(functionData->rangeBddVars); i++) {
683    var = array_fetch(mdd_t *, functionData->rangeBddVars, i);
684    index = (int)bdd_top_var_id(var);
685    st_insert(info->rangeVarsTable, (char *)(long)index, NIL(char));
686  }
687
688  latches = 2 * mdd_get_number_of_bdd_vars(mddManager, rangeVarMddIdArray);
689  nVars = latches + mdd_get_number_of_bdd_vars(mddManager,
690                                                functionData->quantifyVars);
691  variables = bdd_num_vars(mddManager); /* real number of variables */
692  info->nRealVars = nVars;
693  info->nVars = variables;
694
695  if (info->nonDeterministic) {
696    if (method == Img_Tfm_c) {
697      fprintf(vis_stdout,
698        "** tfm warning: The circuit may have nondeterminism.\n");
699      fprintf(vis_stdout, "\tautomatically switched to hybrid mode = 2.\n");
700      info->method = Img_Hybrid_c;
701    } else {
702      if (info->option->hybridMode == 2) {
703        if (info->option->buildPartialTR) {
704          fprintf(vis_stdout,
705                "** hyb warning: The circuit may have nondeterminism.\n");
706          fprintf(vis_stdout,
707                "\tdid not use partial transition relation.\n");
708        } else {
709          fprintf(vis_stdout,
710                "** hyb info: The circuit may have nondeterminism.\n");
711        }
712      } else {
713        fprintf(vis_stdout,
714                "** hyb warning: The circuit may have nondeterminism.\n");
715        fprintf(vis_stdout, "\tautomatically switched to hybrid mode = 2.\n");
716      }
717    }
718  }
719  if (info->nonDeterministic ||
720      (info->option->hybridMode > 0 &&
721       (info->option->splitMethod == 3 || info->option->preSplitMethod == 4))) {
722    if (info->option->hybridMode == 2 || info->nonDeterministic)
723      info->buildTR = 2;
724    else
725      info->buildTR = 1;
726  }
727  if (info->buildTR == 2 &&
728      info->option->buildPartialTR &&
729      info->nonDeterministic == 0 &&
730      info->option->useCache == 0) {
731    info->buildPartialTR = TRUE;
732  }
733
734  info->imgKeepPiInTr = info->option->imgKeepPiInTr;
735  if (info->option->useCache)
736    info->preKeepPiInTr = TRUE;
737  else
738    info->preKeepPiInTr = info->option->preKeepPiInTr;
739
740  if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c &&
741      nVars != variables) {
742    if (info->option->composeIntermediateVars) {
743      composeIntermediateVars = 1;
744      findIntermediateVars = 0;
745    } else {
746      composeIntermediateVars = 0;
747      findIntermediateVars = 1;
748    }
749  } else {
750    composeIntermediateVars = 0;
751    findIntermediateVars = 0;
752  }
753
754  if (info->buildTR != 2 || info->buildPartialTR) { /* deterministic */
755    vector = TfmCreateBitVector(info, composeIntermediateVars,
756                                findIntermediateVars);
757  } else
758    vector = NIL(array_t);
759
760  info->manager = mddManager;
761  if (info->buildPartialTR)
762    info->fullVector = vector;
763  else
764    info->vector = vector;
765  if (info->buildTR == 2)
766    info->useConstraint = 1;
767  else if (info->option->splitMethod == 1)
768    info->useConstraint = 0;
769  else {
770    if (info->option->rangeComp == 2)
771      info->useConstraint = 2;
772    else if (info->option->rangeComp == 0)
773      info->useConstraint = 1;
774    else
775      info->useConstraint = 0;
776  }
777  if (info->option->useCache) {
778    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
779      ImgCacheInitTable(info, info->option->initCacheSize,
780                        info->option->globalCache, FALSE);
781    }
782    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
783      ImgCacheInitTable(info, info->option->initCacheSize,
784                        info->option->globalCache, TRUE);
785    }
786    if (info->option->autoFlushCache == 2) {
787      if (nHookInfoList == 0) {
788        HookInfoList = st_init_table(st_ptrcmp, st_ptrhash);
789        bdd_add_hook(info->manager, HookInfoFunction, BDD_PRE_REORDERING_HOOK);
790        st_insert(HookInfoList, (char *)info, NIL(char));
791      } else {
792        if (info->option->globalCache == 0)
793          st_insert(HookInfoList, (char *)info, NIL(char));
794      }
795      nHookInfoList++;
796    }
797  }
798
799  info->trmOption = ImgGetTrmOptions();
800  info->domainVarBddArray = functionData->domainBddVars;
801  info->quantifyVarBddArray = functionData->quantifyBddVars;
802  info->rangeVarBddArray = functionData->rangeBddVars;
803
804  if (info->vector && info->option->sortVectorFlag && info->option->useCache)
805    array_sort(info->vector, CompareIndex);
806  if (info->buildPartialTR)
807    TfmSetupPartialTransitionRelation(info, NIL(array_t *));
808  if (info->buildTR)
809    TfmBuildRelationArray(info, functionData, NIL(array_t), directionType, 1);
810  if (info->buildTR == 1) {
811    ImgPrintVectorDependency(info, info->vector, info->option->verbosity);
812    if (info->option->writeSupportMatrix == 1) {
813      sprintf(filename, "support%d.mat", info->option->supportFileCount++);
814      ImgWriteSupportMatrix(info, info->vector, NIL(array_t), filename);
815    }
816  }
817  if (info->option->writeSupportMatrixAndStop)
818    exit(0);
819
820  flagValue = Cmd_FlagReadByName("image_eliminate_depend_vars");
821  if (flagValue == NIL(char))
822    info->eliminateDepend = 0; /* the default value */
823  else
824    info->eliminateDepend = atoi(flagValue);
825  if (info->eliminateDepend && bdd_get_package_name() != CUDD) {
826    fprintf(vis_stderr,
827    "** tfm error : image_eliminate_depend_vars is available for only CUDD.\n");
828    info->eliminateDepend = 0;
829  }
830  info->nPrevEliminatedFwd = -1;
831
832  flagValue = Cmd_FlagReadByName("image_verbosity");
833  if (flagValue)
834    info->imageVerbosity = atoi(flagValue);
835
836  if (info->option->printEssential) {
837    info->foundEssentials = ALLOC(int, IMG_TF_MAX_PRINT_DEPTH);
838    memset(info->foundEssentials, 0, sizeof(int) * IMG_TF_MAX_PRINT_DEPTH);
839  }
840  if (info->option->debug)
841    info->debugCareSet = bdd_one(mddManager);
842  else
843    info->debugCareSet = NIL(mdd_t);
844  return((void *)info);
845}
846
847
848/**Function********************************************************************
849
850  Synopsis    [Computes the forward image of a set of states.]
851
852  Description [Computes the forward image of a set of states.]
853
854  SideEffects []
855
856  SeeAlso     [ImgImageInfoComputeFwdWithDomainVarsTfm]
857
858******************************************************************************/
859mdd_t *
860ImgImageInfoComputeFwdTfm(ImgFunctionData_t *functionData,
861                          Img_ImageInfo_t *imageInfo,
862                          mdd_t *fromLowerBound,
863                          mdd_t *fromUpperBound,
864                          array_t *toCareSetArray)
865{
866  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)imageInfo->methodData;
867  mdd_t         *image, *domainSubset;
868
869  if (info->vector == NIL(array_t) &&
870      !(info->buildTR == 2 && info->fwdClusteredRelationArray)) {
871    fprintf(vis_stderr, "** img error: The data structure has not been ");
872    fprintf(vis_stderr, "initialized for image computation\n");
873    return(NIL(mdd_t));
874  }
875
876  info->updatedFlag = FALSE;
877  domainSubset = bdd_between(fromLowerBound, fromUpperBound);
878
879  image = ImgTfmImage(info, domainSubset);
880
881  mdd_free(domainSubset);
882  return(image);
883}
884
885
886/**Function********************************************************************
887
888  Synopsis    [Computes the forward image of a set of states in terms
889  of domain variables.]
890
891  Description [Identical to ImgImageInfoComputeFwdTfm.]
892
893  SideEffects []
894
895  SeeAlso     [ImgImageInfoComputeFwdTfm]
896
897******************************************************************************/
898mdd_t *
899ImgImageInfoComputeFwdWithDomainVarsTfm(ImgFunctionData_t *functionData,
900                                        Img_ImageInfo_t *imageInfo,
901                                        mdd_t *fromLowerBound,
902                                        mdd_t *fromUpperBound,
903                                        array_t *toCareSetArray)
904{
905  mdd_t *image;
906
907  image = ImgImageInfoComputeFwdTfm(functionData,
908                imageInfo , fromLowerBound, fromUpperBound, toCareSetArray);
909  return(image);
910}
911
912
913/**Function********************************************************************
914
915  Synopsis    [Computes the backward image of domainSubset.]
916
917  Description [Computes the backward image of domainSubset.]
918
919  SideEffects []
920
921  SeeAlso     [ImgImageInfoComputeBwdWithDomainVarsTfm]
922
923******************************************************************************/
924mdd_t *
925ImgImageInfoComputeBwdTfm(ImgFunctionData_t *functionData,
926                          Img_ImageInfo_t *imageInfo,
927                          mdd_t *fromLowerBound,
928                          mdd_t *fromUpperBound,
929                          array_t *toCareSetArray)
930{
931  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)imageInfo->methodData;
932  mdd_t         *image, *domainSubset, *simplifiedImage;
933  array_t       *replace;
934
935  if (info->vector == NIL(array_t) &&
936      !(info->buildTR == 2 && info->bwdClusteredRelationArray)) {
937    fprintf(vis_stderr, "** img error: The data structure has not been ");
938    fprintf(vis_stderr, "initialized for backward image computation\n");
939    return(NIL(mdd_t));
940  }
941
942  info->updatedFlag = FALSE;
943  domainSubset = bdd_between(fromLowerBound, fromUpperBound);
944
945  if (info->toCareSetArray)
946    replace = info->toCareSetArray;
947  else {
948    replace = NIL(array_t);
949    info->toCareSetArray = toCareSetArray;
950  }
951  image = ImgTfmPreImage(info, domainSubset);
952  info->toCareSetArray = replace;
953
954  mdd_free(domainSubset);
955  simplifiedImage = bdd_minimize_array(image, toCareSetArray);
956  bdd_free(image);
957  return(simplifiedImage);
958}
959
960
961/**Function********************************************************************
962
963  Synopsis    [Computes the backward image of a set of states.]
964
965  Description [Identical to ImgImageInfoComputeBwdTfm.]
966
967  SideEffects []
968
969  SeeAlso     [ImgImageInfoComputeBwdTfm]
970
971******************************************************************************/
972mdd_t *
973ImgImageInfoComputeBwdWithDomainVarsTfm(ImgFunctionData_t *functionData,
974                                           Img_ImageInfo_t *imageInfo,
975                                           mdd_t *fromLowerBound,
976                                           mdd_t *fromUpperBound,
977                                           array_t *toCareSetArray)
978{
979  mdd_t *image;
980
981  image = ImgImageInfoComputeBwdTfm(functionData,
982                imageInfo, fromLowerBound, fromUpperBound, toCareSetArray);
983  return(image);
984}
985
986
987/**Function********************************************************************
988
989  Synopsis    [Frees the memory associated with imageInfo.]
990
991  Description [Frees the memory associated with imageInfo.]
992
993  SideEffects []
994
995******************************************************************************/
996void
997ImgImageInfoFreeTfm(void *methodData)
998{
999  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)methodData;
1000
1001  if (info == NIL(ImgTfmInfo_t)) {
1002    fprintf(vis_stderr, "** img error: Trying to free the NULL image info\n");
1003    return;
1004  }
1005  if (info->option->printStatistics) {
1006    if (info->nRecursion) {
1007      if (info->imgCache)
1008        ImgPrintCacheStatistics(info->imgCache);
1009      PrintRecursionStatistics(info, 0);
1010      PrintFoundVariableStatistics(info, 0);
1011    }
1012    if (info->nRecursionB) {
1013      if (info->preCache)
1014        ImgPrintCacheStatistics(info->preCache);
1015      PrintRecursionStatistics(info, 1);
1016      PrintFoundVariableStatistics(info, 1);
1017    }
1018  }
1019  if (info->vector != NIL(array_t))
1020    ImgVectorFree(info->vector);
1021  if (info->toCareSetArray != NIL(array_t))
1022    mdd_array_free(info->toCareSetArray);
1023  if (info->imgCache)
1024    ImgCacheDestroyTable(info->imgCache, info->option->globalCache);
1025  if (info->preCache)
1026    ImgCacheDestroyTable(info->preCache, info->option->globalCache);
1027  st_free_table(info->quantifyVarsTable);
1028  st_free_table(info->rangeVarsTable);
1029  if (info->intermediateVarsTable) {
1030    st_free_table(info->intermediateVarsTable);
1031    info->intermediateVarsTable = NIL(st_table);
1032  }
1033  if (info->intermediateBddVars) {
1034    mdd_array_free(info->intermediateBddVars);
1035    info->intermediateBddVars= NIL(array_t);
1036  }
1037  if (info->newQuantifyBddVars) {
1038    mdd_array_free(info->newQuantifyBddVars);
1039    info->newQuantifyBddVars = NIL(array_t);
1040  }
1041
1042  if (info->option->useCache) {
1043    if (info->option->autoFlushCache == 2) {
1044      nHookInfoList--;
1045      st_delete(HookInfoList, &info, NULL);
1046      if (nHookInfoList == 0) {
1047        st_free_table(HookInfoList);
1048        bdd_remove_hook(info->manager, HookInfoFunction,
1049                        BDD_PRE_REORDERING_HOOK);
1050      }
1051    }
1052  }
1053  if (info->option != NULL)
1054    FREE(info->option);
1055
1056  if (info->fwdClusteredRelationArray)
1057    mdd_array_free(info->fwdClusteredRelationArray);
1058  if (info->bwdClusteredRelationArray)
1059    mdd_array_free(info->bwdClusteredRelationArray);
1060  if (info->fwdArraySmoothVarBddArray)
1061    mdd_array_array_free(info->fwdArraySmoothVarBddArray);
1062  if (info->bwdArraySmoothVarBddArray)
1063    mdd_array_array_free(info->bwdArraySmoothVarBddArray);
1064  if (info->fwdSmoothVarCubeArray)
1065    mdd_array_free(info->fwdSmoothVarCubeArray);
1066  if (info->bwdSmoothVarCubeArray)
1067    mdd_array_free(info->bwdSmoothVarCubeArray);
1068  if (info->trmOption)
1069    ImgFreeTrmOptions(info->trmOption);
1070  if (info->partialBddVars)
1071    mdd_array_free(info->partialBddVars);
1072  if (info->partialVarFlag)
1073    FREE(info->partialVarFlag);
1074  if (info->fullVector != NIL(array_t))
1075    ImgVectorFree(info->fullVector);
1076
1077  if (info->foundEssentials)
1078    FREE(info->foundEssentials);
1079  if (info->debugCareSet)
1080    mdd_free(info->debugCareSet);
1081
1082  if (info->savedArraySmoothVarBddArray != NIL(array_t))
1083    mdd_array_array_free(info->savedArraySmoothVarBddArray);
1084  if (info->savedSmoothVarCubeArray != NIL(array_t))
1085    mdd_array_free(info->savedSmoothVarCubeArray);
1086  FREE(info);
1087}
1088
1089
1090/**Function********************************************************************
1091
1092  Synopsis    [Prints information about the transition function method.]
1093
1094  Description [This function is used to obtain the information about
1095  the parameters used to initialize the imageInfo.]
1096
1097  SideEffects []
1098
1099******************************************************************************/
1100void
1101ImgImageInfoPrintMethodParamsTfm(void *methodData, FILE *fp)
1102{
1103  ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData;
1104
1105  if (fp == NULL)
1106    return;
1107  if (info->vector)
1108    ImgPrintVectorDependency(info, info->vector, 1);
1109  if (info->method == Img_Tfm_c) {
1110    fprintf(vis_stdout,
1111            "For the options in tfm method, try print_tfm_options.\n");
1112    return;
1113  }
1114  if (info->fwdClusteredRelationArray != NIL(array_t)) {
1115    fprintf(fp, "Shared size of transition relation for forward image");
1116    fprintf(fp, " computation is %10ld BDD nodes (%-4d components)\n",
1117            bdd_size_multiple(info->fwdClusteredRelationArray),
1118            array_n(info->fwdClusteredRelationArray));
1119  }
1120  if (info->bwdClusteredRelationArray != NIL(array_t)) {
1121    fprintf(fp, "Shared size of transition relation for backward image");
1122    fprintf(fp, " computation is %10ld BDD nodes (%-4d components)\n",
1123            bdd_size_multiple(info->bwdClusteredRelationArray),
1124            array_n(info->bwdClusteredRelationArray));
1125  }
1126  fprintf(vis_stdout, "For the options in hybrid method,");
1127  fprintf(vis_stdout, " try print_hybrid_options and print_tfm_options.\n");
1128}
1129
1130
1131/**Function********************************************************************
1132
1133  Synopsis    [Restores original transition function from saved.]
1134
1135  Description [Restores original transition function from saved.]
1136
1137  SideEffects []
1138
1139******************************************************************************/
1140void
1141ImgRestoreTransitionFunction(Img_ImageInfo_t *imageInfo,
1142        Img_DirectionType directionType)
1143{
1144  ImgTfmInfo_t  *tfmInfo = (ImgTfmInfo_t *)imageInfo->methodData;
1145
1146  if (tfmInfo->vector) {
1147    ImgVectorFree(tfmInfo->vector);
1148    tfmInfo->vector = (array_t *)imageInfo->savedRelation;
1149    imageInfo->savedRelation = NIL(void);
1150  }
1151  if (tfmInfo->fwdClusteredRelationArray) {
1152    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
1153      mdd_array_free(tfmInfo->fwdClusteredRelationArray);
1154      tfmInfo->fwdClusteredRelationArray = tfmInfo->fwdSavedRelation;
1155      tfmInfo->fwdSavedRelation = NIL(array_t);
1156    }
1157  }
1158  if (tfmInfo->bwdClusteredRelationArray) {
1159    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
1160      mdd_array_free(tfmInfo->bwdClusteredRelationArray);
1161      tfmInfo->bwdClusteredRelationArray = tfmInfo->bwdSavedRelation;
1162      tfmInfo->bwdSavedRelation = NIL(array_t);
1163    }
1164  }
1165}
1166
1167
1168/**Function********************************************************************
1169
1170  Synopsis    [Duplicates transition function.]
1171
1172  Description [Duplicates transition function.]
1173
1174  SideEffects []
1175
1176******************************************************************************/
1177void
1178ImgDuplicateTransitionFunction(Img_ImageInfo_t *imageInfo,
1179                                Img_DirectionType directionType)
1180{
1181  array_t       *copiedVector;
1182  array_t       *copiedRelation;
1183  ImgTfmInfo_t  *tfmInfo = (ImgTfmInfo_t *)imageInfo->methodData;
1184
1185  if (tfmInfo->vector) {
1186    copiedVector = ImgVectorCopy(tfmInfo, tfmInfo->vector);
1187    assert(!imageInfo->savedRelation);
1188    imageInfo->savedRelation = (void *)tfmInfo->vector;
1189    tfmInfo->vector = copiedVector;
1190  }
1191  if (tfmInfo->fwdClusteredRelationArray) {
1192    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
1193      copiedRelation = mdd_array_duplicate(tfmInfo->fwdClusteredRelationArray);
1194      tfmInfo->fwdSavedRelation = tfmInfo->fwdClusteredRelationArray;
1195      tfmInfo->fwdClusteredRelationArray = copiedRelation;
1196    }
1197  }
1198  if (tfmInfo->bwdClusteredRelationArray) {
1199    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
1200      copiedRelation = mdd_array_duplicate(tfmInfo->bwdClusteredRelationArray);
1201      tfmInfo->bwdSavedRelation = tfmInfo->bwdClusteredRelationArray;
1202      tfmInfo->bwdClusteredRelationArray = copiedRelation;
1203    }
1204  }
1205}
1206
1207
1208/**Function********************************************************************
1209
1210  Synopsis    [Minimizes transition function with given set of constraints.]
1211
1212  Description [Minimizes transition function with given set of constraints.]
1213
1214  SideEffects []
1215
1216******************************************************************************/
1217void
1218ImgMinimizeTransitionFunction(void *methodData,
1219                    array_t *constrainArray, Img_MinimizeType minimizeMethod,
1220                    Img_DirectionType directionType, int printStatus)
1221{
1222  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
1223  int                   i, j;
1224  bdd_t                 *function, *simplifiedFunction;
1225  bdd_t                 *constrain;
1226  bdd_t                 *relation, *simplifiedRelation;
1227  int                   size = 0;
1228  long                  sizeConstrain;
1229  ImgComponent_t        *comp;
1230
1231  if (printStatus)
1232    sizeConstrain = bdd_size_multiple(constrainArray);
1233  else
1234    sizeConstrain = 0;
1235
1236  if (info->vector) {
1237    if (printStatus)
1238      size = ImgVectorBddSize(info->vector);
1239
1240    arrayForEachItem(ImgComponent_t *, info->vector, i, comp) {
1241      function = mdd_dup(comp->func);
1242      arrayForEachItem(bdd_t *, constrainArray, j, constrain) {
1243        if (bdd_is_tautology(constrain, 1))
1244          continue;
1245        simplifiedFunction = Img_MinimizeImage(function, constrain,
1246                                               minimizeMethod, TRUE);
1247        if (printStatus == 2) {
1248          (void) fprintf(vis_stdout,
1249              "IMG Info: minimized function %d | %d => %d in component %d\n",
1250                          bdd_size(function), bdd_size(constrain),
1251                          bdd_size(simplifiedFunction), i);
1252        }
1253        mdd_free(function);
1254        function = simplifiedFunction;
1255      }
1256      if (mdd_equal(function, comp->func))
1257        mdd_free(function);
1258      else {
1259        mdd_free(comp->func);
1260        comp->func = function;
1261        ImgSupportClear(info, comp->support);
1262        ImgComponentGetSupport(comp);
1263      }
1264    }
1265
1266    if (printStatus) {
1267      (void) fprintf(vis_stdout,
1268        "IMG Info: minimized function [%d | %ld => %ld] with %d components\n",
1269                   size, sizeConstrain,
1270                   ImgVectorBddSize(info->vector), array_n(info->vector));
1271    }
1272  }
1273
1274  if (info->buildTR == 0)
1275    return;
1276  else if (info->buildTR == 1 && info->option->synchronizeTr) {
1277    if (info->fwdClusteredRelationArray &&
1278        (directionType == Img_Forward_c || directionType == Img_Both_c)) {
1279      RebuildTransitionRelation(info, Img_Forward_c);
1280    }
1281    if (info->bwdClusteredRelationArray &&
1282        (directionType == Img_Backward_c || directionType == Img_Both_c)) {
1283      RebuildTransitionRelation(info, Img_Backward_c);
1284    }
1285    return;
1286  }
1287
1288  if (info->fwdClusteredRelationArray &&
1289      (directionType == Img_Forward_c || directionType == Img_Both_c)) {
1290    if (printStatus)
1291      size = bdd_size_multiple(info->fwdClusteredRelationArray);
1292    arrayForEachItem(bdd_t *, constrainArray, i, constrain) {
1293      if (bdd_is_tautology(constrain, 1))
1294        continue;
1295
1296      arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, j, relation) {
1297        simplifiedRelation = Img_MinimizeImage(relation, constrain,
1298                                                 minimizeMethod, TRUE);
1299        if (printStatus == 2) {
1300          (void) fprintf(vis_stdout,
1301            "IMG Info: minimized fwd relation %d | %d => %d in component %d\n",
1302                         bdd_size(relation), bdd_size(constrain),
1303                         bdd_size(simplifiedRelation), j);
1304        }
1305        mdd_free(relation);
1306        array_insert(bdd_t*, info->fwdClusteredRelationArray, j,
1307                     simplifiedRelation);
1308      }
1309    }
1310    if (printStatus) {
1311      (void) fprintf(vis_stdout,
1312     "IMG Info: minimized fwd relation [%d | %ld => %ld] with %d components\n",
1313                     size, sizeConstrain,
1314                     bdd_size_multiple(info->fwdClusteredRelationArray),
1315                     array_n(info->fwdClusteredRelationArray));
1316    }
1317  }
1318  if (info->bwdClusteredRelationArray &&
1319      (directionType == Img_Backward_c || directionType == Img_Both_c)) {
1320    if (printStatus)
1321      size = bdd_size_multiple(info->bwdClusteredRelationArray);
1322    arrayForEachItem(bdd_t *, constrainArray, i, constrain) {
1323      if (bdd_is_tautology(constrain, 1))
1324        continue;
1325
1326      arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, j, relation) {
1327        simplifiedRelation = Img_MinimizeImage(relation, constrain,
1328                                                 minimizeMethod, TRUE);
1329        if (printStatus == 2) {
1330          (void) fprintf(vis_stdout,
1331            "IMG Info: minimized bwd relation %d | %d => %d in component %d\n",
1332                         bdd_size(relation), bdd_size(constrain),
1333                         bdd_size(simplifiedRelation), j);
1334        }
1335        mdd_free(relation);
1336        array_insert(bdd_t*, info->bwdClusteredRelationArray, j,
1337                     simplifiedRelation);
1338      }
1339    }
1340    if (printStatus) {
1341      (void) fprintf(vis_stdout,
1342     "IMG Info: minimized bwd relation [%d | %ld => %ld] with %d components\n",
1343                     size, sizeConstrain,
1344                     bdd_size_multiple(info->bwdClusteredRelationArray),
1345                     array_n(info->bwdClusteredRelationArray));
1346    }
1347  }
1348}
1349
1350
1351/**Function********************************************************************
1352
1353  Synopsis    [Adds a dont care set to the transition function and relation.]
1354
1355  Description [Adds a dont care set to the transition function and relation.
1356  This function is called during guided search.]
1357
1358  SideEffects []
1359
1360******************************************************************************/
1361void
1362ImgAddDontCareToTransitionFunction(void *methodData,
1363                                   array_t *constrainArray,
1364                                   Img_MinimizeType minimizeMethod,
1365                                   Img_DirectionType directionType,
1366                                   int printStatus)
1367{
1368  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
1369  int                   i, j;
1370  bdd_t                 *function, *simplifiedFunction;
1371  bdd_t                 *constrain;
1372  bdd_t                 *relation, *simplifiedRelation;
1373  int                   size = 0;
1374  long                  sizeConstrain;
1375  ImgComponent_t        *comp;
1376
1377  if (printStatus)
1378    sizeConstrain = bdd_size_multiple(constrainArray);
1379  else
1380    sizeConstrain = 0;
1381
1382  if (info->vector) {
1383    if (printStatus)
1384      size = ImgVectorBddSize(info->vector);
1385
1386    arrayForEachItem(ImgComponent_t *, info->vector, i, comp) {
1387      function = mdd_dup(comp->func);
1388      arrayForEachItem(bdd_t *, constrainArray, j, constrain) {
1389        if (bdd_is_tautology(constrain, 1))
1390          continue;
1391        simplifiedFunction = Img_AddDontCareToImage(function, constrain,
1392                                                    minimizeMethod);
1393        if (printStatus == 2) {
1394          (void) fprintf(vis_stdout,
1395              "IMG Info: minimized function %d | %d => %d in component %d\n",
1396                          bdd_size(function), bdd_size(constrain),
1397                          bdd_size(simplifiedFunction), i);
1398        }
1399        mdd_free(function);
1400        function = simplifiedFunction;
1401      }
1402      if (mdd_equal(function, comp->func))
1403        mdd_free(function);
1404      else {
1405        mdd_free(comp->func);
1406        comp->func = function;
1407        ImgSupportClear(info, comp->support);
1408        ImgComponentGetSupport(comp);
1409      }
1410    }
1411
1412    if (printStatus) {
1413      (void) fprintf(vis_stdout,
1414        "IMG Info: minimized function [%d | %ld => %ld] with %d components\n",
1415                   size, sizeConstrain,
1416                   ImgVectorBddSize(info->vector), array_n(info->vector));
1417    }
1418  }
1419
1420  if (info->buildTR == 0)
1421    return;
1422  else if (info->buildTR == 1 && info->option->synchronizeTr) {
1423    if (info->fwdClusteredRelationArray &&
1424        (directionType == Img_Forward_c || directionType == Img_Both_c)) {
1425      RebuildTransitionRelation(info, Img_Forward_c);
1426    }
1427    if (info->bwdClusteredRelationArray &&
1428        (directionType == Img_Backward_c || directionType == Img_Both_c)) {
1429      RebuildTransitionRelation(info, Img_Backward_c);
1430    }
1431    return;
1432  }
1433
1434  if (info->fwdClusteredRelationArray &&
1435      (directionType == Img_Forward_c || directionType == Img_Both_c)) {
1436    if (printStatus)
1437      size = bdd_size_multiple(info->fwdClusteredRelationArray);
1438    arrayForEachItem(bdd_t *, constrainArray, i, constrain) {
1439      if (bdd_is_tautology(constrain, 1))
1440        continue;
1441
1442      arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, j, relation) {
1443        simplifiedRelation = Img_AddDontCareToImage(relation, constrain,
1444                                                    minimizeMethod);
1445        if (printStatus == 2) {
1446          (void) fprintf(vis_stdout,
1447            "IMG Info: minimized fwd relation %d | %d => %d in component %d\n",
1448                         bdd_size(relation), bdd_size(constrain),
1449                         bdd_size(simplifiedRelation), j);
1450        }
1451        mdd_free(relation);
1452        array_insert(bdd_t*, info->fwdClusteredRelationArray, j,
1453                     simplifiedRelation);
1454      }
1455    }
1456    if (printStatus) {
1457      (void) fprintf(vis_stdout,
1458     "IMG Info: minimized fwd relation [%d | %ld => %ld] with %d components\n",
1459                     size, sizeConstrain,
1460                     bdd_size_multiple(info->fwdClusteredRelationArray),
1461                     array_n(info->fwdClusteredRelationArray));
1462    }
1463  }
1464  if (info->bwdClusteredRelationArray &&
1465      (directionType == Img_Backward_c || directionType == Img_Both_c)) {
1466    if (printStatus)
1467      size = bdd_size_multiple(info->bwdClusteredRelationArray);
1468    arrayForEachItem(bdd_t *, constrainArray, i, constrain) {
1469      if (bdd_is_tautology(constrain, 1))
1470        continue;
1471
1472      arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, j, relation) {
1473        simplifiedRelation = Img_AddDontCareToImage(relation, constrain,
1474                                                    minimizeMethod);
1475        if (printStatus == 2) {
1476          (void) fprintf(vis_stdout,
1477            "IMG Info: minimized bwd relation %d | %d => %d in component %d\n",
1478                         bdd_size(relation), bdd_size(constrain),
1479                         bdd_size(simplifiedRelation), j);
1480        }
1481        mdd_free(relation);
1482        array_insert(bdd_t*, info->bwdClusteredRelationArray, j,
1483                     simplifiedRelation);
1484      }
1485    }
1486    if (printStatus) {
1487      (void) fprintf(vis_stdout,
1488     "IMG Info: minimized bwd relation [%d | %ld => %ld] with %d components\n",
1489                     size, sizeConstrain,
1490                     bdd_size_multiple(info->bwdClusteredRelationArray),
1491                     array_n(info->bwdClusteredRelationArray));
1492    }
1493  }
1494}
1495
1496
1497/**Function********************************************************************
1498
1499  Synopsis    [Abstracts out given variables from transition function.]
1500
1501  Description [Abstracts out given variables from transition function.
1502  abstractVars should be an array of bdd variables.]
1503
1504  SideEffects []
1505
1506******************************************************************************/
1507void
1508ImgAbstractTransitionFunction(Img_ImageInfo_t *imageInfo,
1509                array_t *abstractVars, mdd_t *abstractCube,
1510                Img_DirectionType directionType, int printStatus)
1511{
1512  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)imageInfo->methodData;
1513  int                   i, size = 0;
1514  bdd_t                 *abstractedFunction;
1515  ImgComponent_t        *comp;
1516  array_t               *vector;
1517  int                   flag = 0;
1518  int                   fwd_size = 0, bwd_size = 0;
1519  bdd_t                 *relation, *abstractedRelation;
1520
1521  if (!abstractVars || array_n(abstractVars) == 0)
1522    return;
1523
1524  if (info->vector) {
1525    if (printStatus)
1526      size = ImgVectorBddSize(info->vector);
1527
1528    arrayForEachItem(ImgComponent_t *, info->vector, i, comp) {
1529      if (bdd_is_tautology(comp->func, 1))
1530        continue;
1531      if (abstractCube)
1532        abstractedFunction = bdd_smooth_with_cube(comp->func, abstractCube);
1533      else
1534        abstractedFunction = bdd_smooth(comp->func, abstractVars);
1535      if (bdd_is_tautology(abstractedFunction, 1)) {
1536        comp->flag = 1;
1537        flag = 1;
1538        continue;
1539      }
1540      if (mdd_equal(abstractedFunction, comp->func))
1541        mdd_free(abstractedFunction);
1542      else {
1543        if (printStatus == 2) {
1544          (void) fprintf(vis_stdout,
1545              "IMG Info: abstracted function %d => %d in component %d\n",
1546                         bdd_size(comp->func), bdd_size(abstractedFunction), i);
1547        }
1548        mdd_free(comp->func);
1549        comp->func = abstractedFunction;
1550        ImgSupportClear(info, comp->support);
1551        ImgComponentGetSupport(comp);
1552      }
1553    }
1554
1555    if (flag) {
1556      vector = info->vector;
1557      info->vector = array_alloc(ImgComponent_t *, 0);
1558      arrayForEachItem(ImgComponent_t *, vector, i, comp) {
1559        if (comp->flag) {
1560          ImgComponentFree(comp);
1561          continue;
1562        }
1563        array_insert_last(ImgComponent_t *, info->vector, comp);
1564      }
1565      array_free(vector);
1566    }
1567
1568    if (printStatus) {
1569      (void) fprintf(vis_stdout,
1570       "IMG Info: abstracted function [%d => %ld] with %d components\n",
1571                     size, ImgVectorBddSize(info->vector),
1572                     array_n(info->vector));
1573    }
1574  }
1575
1576  if (info->buildTR == 0)
1577    return;
1578  else if (info->buildTR == 1 && info->option->synchronizeTr) {
1579    if (info->fwdClusteredRelationArray &&
1580        (directionType == Img_Forward_c || directionType == Img_Both_c)) {
1581      RebuildTransitionRelation(info, Img_Forward_c);
1582    }
1583    if (info->bwdClusteredRelationArray &&
1584        (directionType == Img_Backward_c || directionType == Img_Both_c)) {
1585      RebuildTransitionRelation(info, Img_Backward_c);
1586    }
1587    return;
1588  }
1589
1590  if (printStatus) {
1591    if (directionType == Img_Forward_c || directionType == Img_Both_c)
1592      fwd_size = bdd_size_multiple(info->fwdClusteredRelationArray);
1593    if (directionType == Img_Backward_c || directionType == Img_Both_c)
1594      bwd_size = bdd_size_multiple(info->bwdClusteredRelationArray);
1595  }
1596  if (info->fwdClusteredRelationArray &&
1597      (directionType == Img_Forward_c || directionType == Img_Both_c)) {
1598    arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) {
1599      if (abstractCube)
1600        abstractedRelation = bdd_smooth_with_cube(relation, abstractCube);
1601      else
1602        abstractedRelation = bdd_smooth(relation, abstractVars);
1603      if (printStatus == 2) {
1604        (void) fprintf(vis_stdout,
1605          "IMG Info: abstracted fwd relation %d => %d in component %d\n",
1606                         bdd_size(relation), bdd_size(abstractedRelation), i);
1607      }
1608      mdd_free(relation);
1609      array_insert(bdd_t*, info->fwdClusteredRelationArray, i,
1610                   abstractedRelation);
1611    }
1612  }
1613  if (info->bwdClusteredRelationArray &&
1614      (directionType == Img_Backward_c || directionType == Img_Both_c)) {
1615    arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) {
1616      if (abstractCube)
1617        abstractedRelation = bdd_smooth_with_cube(relation, abstractCube);
1618      else
1619        abstractedRelation = bdd_smooth(relation, abstractVars);
1620      if (printStatus == 2) {
1621        (void) fprintf(vis_stdout,
1622          "IMG Info: abstracted bwd relation %d => %d in component %d\n",
1623                         bdd_size(relation), bdd_size(abstractedRelation), i);
1624      }
1625      mdd_free(relation);
1626      array_insert(bdd_t*, info->bwdClusteredRelationArray, i,
1627                   abstractedRelation);
1628    }
1629  }
1630  if (printStatus) {
1631    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
1632      (void) fprintf(vis_stdout,
1633     "IMG Info: abstracted fwd relation [%d => %ld] with %d components\n",
1634                     fwd_size,
1635                     bdd_size_multiple(info->fwdClusteredRelationArray),
1636                     array_n(info->fwdClusteredRelationArray));
1637    }
1638    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
1639      (void) fprintf(vis_stdout,
1640     "IMG Info: abstracted bwd relation [%d => %ld] with %d components\n",
1641                     bwd_size,
1642                     bdd_size_multiple(info->bwdClusteredRelationArray),
1643                     array_n(info->bwdClusteredRelationArray));
1644    }
1645  }
1646}
1647
1648
1649/**Function********************************************************************
1650
1651  Synopsis    [Approximate transition function.]
1652
1653  Description [Approximate transition function.]
1654
1655  SideEffects []
1656
1657******************************************************************************/
1658int
1659ImgApproximateTransitionFunction(mdd_manager *mgr,
1660                void *methodData, bdd_approx_dir_t approxDir,
1661                bdd_approx_type_t approxMethod, int approxThreshold,
1662                double approxQuality, double approxQualityBias,
1663                Img_DirectionType directionType, mdd_t *bias)
1664{
1665  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
1666  int                   i;
1667  bdd_t                 *approxFunction;
1668  int                   unchanged = 0;
1669  ImgComponent_t        *comp;
1670  bdd_t                 *relation, *approxRelation;
1671
1672  if (info->vector) {
1673    arrayForEachItem(ImgComponent_t *, info->vector, i, comp) {
1674      approxFunction = Img_ApproximateImage(mgr, comp->func,
1675                                            approxDir, approxMethod,
1676                                            approxThreshold, approxQuality,
1677                                            approxQualityBias, bias);
1678      if (bdd_is_tautology(approxFunction, 1)) {
1679        fprintf(vis_stdout,
1680                  "** img warning : bdd_one from subsetting in [%d].\n", i);
1681        mdd_free(approxFunction);
1682        unchanged++;
1683      } else if (bdd_is_tautology(approxFunction, 0)) {
1684        fprintf(vis_stdout,
1685                  "** img warning : bdd_zero from subsetting in [%d].\n", i);
1686        mdd_free(approxFunction);
1687        unchanged++;
1688      } else if (mdd_equal(approxFunction, comp->func)) {
1689        mdd_free(approxFunction);
1690        unchanged++;
1691      } else {
1692        mdd_free(comp->func);
1693        comp->func = approxFunction;
1694        ImgSupportClear(info, comp->support);
1695        ImgComponentGetSupport(comp);
1696      }
1697    }
1698  }
1699
1700  if (info->buildTR == 0)
1701    return(unchanged);
1702  else if (info->buildTR == 1 && info->option->synchronizeTr) {
1703    if (info->fwdClusteredRelationArray &&
1704        (directionType == Img_Forward_c || directionType == Img_Both_c)) {
1705      RebuildTransitionRelation(info, Img_Forward_c);
1706    }
1707    if (info->bwdClusteredRelationArray &&
1708        (directionType == Img_Backward_c || directionType == Img_Both_c)) {
1709      RebuildTransitionRelation(info, Img_Backward_c);
1710    }
1711    return(unchanged);
1712  }
1713
1714  if (info->fwdClusteredRelationArray &&
1715      (directionType == Img_Forward_c || directionType == Img_Both_c)) {
1716    arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) {
1717      approxRelation = Img_ApproximateImage(mgr, relation,
1718                                            approxDir, approxMethod,
1719                                            approxThreshold, approxQuality,
1720                                            approxQualityBias, bias);
1721      if (bdd_is_tautology(approxRelation, 1)) {
1722        fprintf(vis_stdout,
1723                "** img warning : bdd_one from subsetting in fwd[%d].\n", i);
1724        mdd_free(approxRelation);
1725        unchanged++;
1726      } else if (bdd_is_tautology(approxRelation, 0)) {
1727        fprintf(vis_stdout,
1728                "** img warning : bdd_zero from subsetting in fwd[%d].\n", i);
1729        mdd_free(approxRelation);
1730        unchanged++;
1731      } else if (mdd_equal(approxRelation, relation)) {
1732        mdd_free(approxRelation);
1733        unchanged++;
1734      } else {
1735        mdd_free(relation);
1736        array_insert(bdd_t*, info->fwdClusteredRelationArray, i,
1737                     approxRelation);
1738      }
1739    }
1740  }
1741  if (info->bwdClusteredRelationArray &&
1742      (directionType == Img_Backward_c || directionType == Img_Both_c)) {
1743    arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) {
1744      approxRelation = Img_ApproximateImage(mgr, relation,
1745                                            approxDir, approxMethod,
1746                                            approxThreshold, approxQuality,
1747                                            approxQualityBias, bias);
1748      if (bdd_is_tautology(approxRelation, 1)) {
1749        fprintf(vis_stdout,
1750                "** img warning : bdd_one from subsetting in bwd[%d].\n", i);
1751        mdd_free(approxRelation);
1752        unchanged++;
1753      } else if (bdd_is_tautology(approxRelation, 0)) {
1754        fprintf(vis_stdout,
1755                "** img warning : bdd_zero from subsetting in bwd[%d].\n", i);
1756        mdd_free(approxRelation);
1757        unchanged++;
1758      } else if (mdd_equal(approxRelation, relation)) {
1759        mdd_free(approxRelation);
1760        unchanged++;
1761      } else {
1762        mdd_free(relation);
1763        array_insert(bdd_t*, info->bwdClusteredRelationArray, i,
1764                     approxRelation);
1765      }
1766    }
1767  }
1768  return(unchanged);
1769}
1770
1771
1772/**Function********************************************************************
1773
1774  Synopsis    [Returns current transition function.]
1775
1776  Description [Returns current transition function.]
1777
1778  SideEffects []
1779
1780******************************************************************************/
1781array_t *
1782ImgGetTransitionFunction(void *methodData, Img_DirectionType directionType)
1783{
1784  ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)methodData;
1785  if (tfmInfo->vector)
1786    return(tfmInfo->vector);
1787  if (directionType == Img_Forward_c)
1788    return(tfmInfo->fwdClusteredRelationArray);
1789  return(tfmInfo->bwdClusteredRelationArray);
1790}
1791
1792
1793/**Function********************************************************************
1794
1795  Synopsis    [Overwrites transition function with given.]
1796
1797  Description [Overwrites transition function with given.]
1798
1799  SideEffects []
1800
1801******************************************************************************/
1802void
1803ImgUpdateTransitionFunction(void *methodData, array_t *vector,
1804                            Img_DirectionType directionType)
1805{
1806  ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)methodData;
1807  if (tfmInfo->vector)
1808    tfmInfo->vector = vector;
1809  else if (directionType == Img_Forward_c)
1810    tfmInfo->fwdClusteredRelationArray = vector;
1811  else
1812    tfmInfo->bwdClusteredRelationArray = vector;
1813}
1814
1815
1816/**Function********************************************************************
1817
1818  Synopsis    [Replace ith transition function.]
1819
1820  Description [Replace ith transition function.]
1821
1822  SideEffects []
1823
1824******************************************************************************/
1825void
1826ImgReplaceIthTransitionFunction(void *methodData, int i, mdd_t *function,
1827                                Img_DirectionType directionType)
1828{
1829  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)methodData;
1830  array_t               *relationArray;
1831  ImgComponent_t        *comp;
1832  mdd_t                 *old;
1833
1834  if (info->vector) {
1835    comp = array_fetch(ImgComponent_t *, info->vector, i);
1836    mdd_free(comp->func);
1837    comp->func = function;
1838    ImgSupportClear(info, comp->support);
1839    ImgComponentGetSupport(comp);
1840    return;
1841  }
1842
1843  if (directionType == Img_Forward_c)
1844    relationArray = info->fwdClusteredRelationArray;
1845  else
1846    relationArray = info->bwdClusteredRelationArray;
1847
1848  old = array_fetch(mdd_t *, relationArray, i);
1849  mdd_free(old);
1850  array_insert(mdd_t *, relationArray, i, function);
1851}
1852
1853
1854/**Function********************************************************************
1855
1856  Synopsis    [Gets the necessary options for computing the image and returns
1857               in the option structure.]
1858
1859  Description [Gets the necessary options for computing the image and returns
1860               in the option structure.]
1861
1862  SideEffects []
1863
1864******************************************************************************/
1865ImgTfmOption_t *
1866ImgTfmGetOptions(Img_MethodType method)
1867{
1868  char                  *flagValue;
1869  ImgTfmOption_t        *option;
1870
1871  option = ALLOC(ImgTfmOption_t, 1);
1872  memset(option, 0, sizeof(ImgTfmOption_t));
1873
1874  option->debug = ReadSetBooleanValue("tfm_debug", FALSE);
1875  option->checkEquivalence = ReadSetBooleanValue("tfm_check_equivalence",
1876                                                 FALSE);
1877  option->writeSupportMatrix = ReadSetIntValue("tfm_write_support_matrix",
1878                                                0, 2, 0);
1879  option->writeSupportMatrixWithYvars =
1880    ReadSetBooleanValue("tfm_write_support_matrix_with_y", FALSE);
1881  option->writeSupportMatrixAndStop =
1882    ReadSetBooleanValue("tfm_write_support_matrix_and_stop", FALSE);
1883  option->writeSupportMatrixReverseRow =
1884    ReadSetBooleanValue("tfm_write_support_matrix_reverse_row", TRUE);
1885  option->writeSupportMatrixReverseCol =
1886    ReadSetBooleanValue("tfm_write_support_matrix_reverse_col", TRUE);
1887
1888  option->verbosity = ReadSetIntValue("tfm_verbosity", 0, 2, 0);
1889  if (method == Img_Tfm_c)
1890    option->splitMethod = ReadSetIntValue("tfm_split_method", 0, 3, 0);
1891  else
1892    option->splitMethod = 3; /* the default value */
1893  option->inputSplit = ReadSetIntValue("tfm_input_split", 0, 3, 0);
1894  option->piSplitFlag = ReadSetBooleanValue("tfm_pi_split_flag", TRUE);
1895  if (method == Img_Tfm_c)
1896    option->rangeComp = ReadSetIntValue("tfm_range_comp", 0, 2, 1);
1897  else
1898    option->rangeComp = ReadSetIntValue("tfm_range_comp", 0, 2, 2);
1899
1900  flagValue = Cmd_FlagReadByName("tfm_range_threshold");
1901  if (flagValue == NIL(char))
1902    option->rangeThreshold = 10; /* the default value */
1903  else
1904    option->rangeThreshold = atoi(flagValue);
1905
1906  flagValue = Cmd_FlagReadByName("tfm_range_try_threshold");
1907  if (flagValue == NIL(char))
1908    option->rangeTryThreshold = 2; /* the default value */
1909  else
1910    option->rangeTryThreshold = atoi(flagValue);
1911
1912  option->rangeCheckReorder =
1913    ReadSetBooleanValue("tfm_range_check_reorder", FALSE);
1914  option->tieBreakMode = ReadSetIntValue("tfm_tie_break", 0, 1, 0);
1915
1916  option->outputSplit = ReadSetIntValue("tfm_output_split", 0, 2, 0);
1917
1918  flagValue = Cmd_FlagReadByName("tfm_turn_depth");
1919  if (flagValue == NIL(char)) {
1920    if (method == Img_Tfm_c)
1921      option->turnDepth = 5; /* the default for tfm */
1922    else
1923      option->turnDepth = -1; /* the default for hybrid */
1924  } else
1925    option->turnDepth = atoi(flagValue);
1926
1927  option->findDecompVar = ReadSetBooleanValue("tfm_find_decomp_var", FALSE);
1928  option->globalCache = ReadSetBooleanValue("tfm_global_cache", TRUE);
1929
1930  flagValue = Cmd_FlagReadByName("tfm_use_cache");
1931  if (flagValue == NIL(char)) {
1932    if (method == Img_Tfm_c)
1933      option->useCache = 1;
1934    else
1935      option->useCache = 0;
1936  } else
1937    option->useCache = atoi(flagValue);
1938
1939  flagValue = Cmd_FlagReadByName("tfm_max_chain_length");
1940  if (flagValue == NIL(char))
1941    option->maxChainLength = 2; /* the default value */
1942  else
1943    option->maxChainLength = atoi(flagValue);
1944
1945  flagValue = Cmd_FlagReadByName("tfm_init_cache_size");
1946  if (flagValue == NIL(char))
1947    option->initCacheSize = 1001; /* the default value */
1948  else
1949    option->initCacheSize = atoi(flagValue);
1950
1951  option->autoFlushCache = ReadSetIntValue("tfm_auto_flush_cache", 0, 2, 1);
1952  if (method == Img_Tfm_c)
1953    option->sortVectorFlag = ReadSetBooleanValue("tfm_sort_vector", TRUE);
1954  else
1955    option->sortVectorFlag = ReadSetBooleanValue("tfm_sort_vector", FALSE);
1956  option->printStatistics = ReadSetBooleanValue("tfm_print_stats", FALSE);
1957  option->printBddSize = ReadSetBooleanValue("tfm_print_bdd_size", FALSE);
1958
1959  flagValue = Cmd_FlagReadByName("tfm_max_essential_depth");
1960  if (flagValue == NIL(char))
1961    option->maxEssentialDepth = 5; /* the default value */
1962  else
1963    option->maxEssentialDepth = atoi(flagValue);
1964
1965  option->findEssential = ReadSetIntValue("tfm_find_essential", 0, 2, 0);
1966  if (option->findEssential && bdd_get_package_name() != CUDD) {
1967    fprintf(vis_stderr,
1968            "** tfm error: tfm_find_essential is available for only CUDD.\n");
1969    option->findEssential = 0; 
1970  }
1971  option->printEssential = ReadSetIntValue("tfm_print_essential", 0, 2, 0);
1972  option->splitCubeFunc = ReadSetBooleanValue("tfm_split_cube_func", FALSE);
1973  option->composeIntermediateVars =
1974        ReadSetBooleanValue("tfm_compose_intermediate_vars", FALSE);
1975
1976  if (method == Img_Tfm_c)
1977    option->preSplitMethod = ReadSetIntValue("tfm_pre_split_method", 0, 4, 0);
1978  else
1979    option->preSplitMethod = 4;
1980  option->preInputSplit = ReadSetIntValue("tfm_pre_input_split", 0, 3, 0);
1981  option->preOutputSplit = ReadSetIntValue("tfm_pre_output_split", 0, 2, 0);
1982  option->preDcLeafMethod = ReadSetIntValue("tfm_pre_dc_leaf_method", 0, 2, 0);
1983  option->preMinimize = ReadSetBooleanValue("tfm_pre_minimize", FALSE);
1984
1985  option->trSplitMethod = ReadSetIntValue("hybrid_tr_split_method", 0, 1, 0);
1986
1987  option->hybridMode = ReadSetIntValue("hybrid_mode", 0, 2, 1);
1988  option->buildPartialTR =
1989    ReadSetBooleanValue("hybrid_build_partial_tr", FALSE);
1990
1991  flagValue = Cmd_FlagReadByName("hybrid_partial_num_vars");
1992  if (flagValue == NIL(char))
1993    option->nPartialVars = 8; /* the default value */
1994  else
1995    option->nPartialVars = atoi(flagValue);
1996
1997  option->partialMethod = ReadSetIntValue("hybrid_partial_method", 0, 1, 0);
1998
1999  option->delayedSplit = ReadSetBooleanValue("hybrid_delayed_split", FALSE);
2000
2001  flagValue = Cmd_FlagReadByName("hybrid_split_min_depth");
2002  if (flagValue == NIL(char))
2003    option->splitMinDepth = 1; /* the default value */
2004  else
2005    option->splitMinDepth = atoi(flagValue);
2006
2007  flagValue = Cmd_FlagReadByName("hybrid_split_max_depth");
2008  if (flagValue == NIL(char))
2009    option->splitMaxDepth = 5; /* the default value */
2010  else
2011    option->splitMaxDepth = atoi(flagValue);
2012
2013  flagValue = Cmd_FlagReadByName("hybrid_pre_split_min_depth");
2014  if (flagValue == NIL(char))
2015    option->preSplitMinDepth = 0; /* the default value */
2016  else
2017    option->preSplitMinDepth = atoi(flagValue);
2018
2019  flagValue = Cmd_FlagReadByName("hybrid_pre_split_max_depth");
2020  if (flagValue == NIL(char))
2021    option->preSplitMaxDepth = 4; /* the default value */
2022  else
2023    option->preSplitMaxDepth = atoi(flagValue);
2024
2025  flagValue = Cmd_FlagReadByName("hybrid_lambda_threshold");
2026  if (flagValue == NIL(char))
2027    option->lambdaThreshold = 0.6; /* the default value */
2028  else
2029    sscanf(flagValue, "%f", &option->lambdaThreshold);
2030
2031  flagValue = Cmd_FlagReadByName("hybrid_pre_lambda_threshold");
2032  if (flagValue == NIL(char))
2033    option->preLambdaThreshold = 0.65; /* the default value */
2034  else
2035    sscanf(flagValue, "%f", &option->preLambdaThreshold);
2036
2037  flagValue = Cmd_FlagReadByName("hybrid_conjoin_vector_size");
2038  if (flagValue == NIL(char))
2039    option->conjoinVectorSize = 10; /* the default value */
2040  else
2041    option->conjoinVectorSize = atoi(flagValue);
2042
2043  flagValue = Cmd_FlagReadByName("hybrid_conjoin_relation_size");
2044  if (flagValue == NIL(char))
2045    option->conjoinRelationSize = 1; /* the default value */
2046  else
2047    option->conjoinRelationSize = atoi(flagValue);
2048
2049  flagValue = Cmd_FlagReadByName("hybrid_conjoin_relation_bdd_size");
2050  if (flagValue == NIL(char))
2051    option->conjoinRelationBddSize = 200; /* the default value */
2052  else
2053    option->conjoinRelationBddSize = atoi(flagValue);
2054
2055  flagValue = Cmd_FlagReadByName("hybrid_improve_lambda");
2056  if (flagValue == NIL(char))
2057    option->improveLambda = 0.1; /* the default value */
2058  else
2059    sscanf(flagValue, "%f", &option->improveLambda);
2060
2061  flagValue = Cmd_FlagReadByName("hybrid_improve_vector_size");
2062  if (flagValue == NIL(char))
2063    option->improveVectorSize = 3; /* the default value */
2064  else
2065    option->improveVectorSize = atoi(flagValue);
2066
2067  flagValue = Cmd_FlagReadByName("hybrid_improve_vector_bdd_size");
2068  if (flagValue == NIL(char))
2069    option->improveVectorBddSize = 30.0; /* the default value */
2070  else
2071    sscanf(flagValue, "%f", &option->improveVectorBddSize);
2072
2073  option->decideMode = ReadSetIntValue("hybrid_decide_mode", 0, 3, 3);
2074
2075  option->reorderWithFrom =
2076    ReadSetBooleanValue("hybrid_reorder_with_from", TRUE);
2077  option->preReorderWithFrom =
2078    ReadSetBooleanValue("hybrid_pre_reorder_with_from", FALSE);
2079
2080  option->lambdaMode = ReadSetIntValue("hybrid_lambda_mode", 0, 2, 0);
2081  option->preLambdaMode = ReadSetIntValue("hybrid_pre_lambda_mode", 0, 3, 2);
2082  option->lambdaWithFrom = ReadSetBooleanValue("hybrid_lambda_with_from", TRUE);
2083  option->lambdaWithTr = ReadSetBooleanValue("hybrid_lambda_with_tr", TRUE);
2084  option->lambdaWithClustering =
2085    ReadSetBooleanValue("hybrid_lambda_with_clustering", FALSE);
2086
2087  option->synchronizeTr = ReadSetBooleanValue("hybrid_synchronize_tr", FALSE);
2088  option->imgKeepPiInTr = ReadSetBooleanValue("hybrid_img_keep_pi", FALSE);
2089  option->preKeepPiInTr = ReadSetBooleanValue("hybrid_pre_keep_pi", FALSE);
2090
2091  flagValue = Cmd_FlagReadByName("hybrid_tr_method");
2092  if (flagValue == NIL(char))
2093    option->trMethod = Img_Iwls95_c; /* the default value */
2094  else {
2095    if (strcmp(flagValue, "iwls95") == 0)
2096      option->trMethod = Img_Iwls95_c;
2097    else if (strcmp(flagValue, "mlp") == 0)
2098      option->trMethod = Img_Mlp_c;
2099    else {
2100      fprintf(vis_stderr,
2101                "** tfm error : invalid value %s for hybrid_tr_method\n",
2102                flagValue);
2103      option->trMethod = Img_Iwls95_c;
2104    }
2105  }
2106  option->preCanonical = ReadSetBooleanValue("hybrid_pre_canonical", FALSE);
2107
2108  option->printLambda = ReadSetBooleanValue("hybrid_print_lambda", FALSE);
2109
2110  return(option);
2111}
2112
2113
2114/**Function********************************************************************
2115
2116  Synopsis [Frees current transition function vector and relation for the given
2117  direction.]
2118
2119  Description [Frees current transition function vector and relation for the
2120  given direction.]
2121
2122  SideEffects []
2123
2124******************************************************************************/
2125void
2126ImgImageFreeClusteredTransitionRelationTfm(void *methodData,
2127                                           Img_DirectionType directionType)
2128{
2129  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)methodData;
2130
2131  if (info->vector) {
2132    ImgVectorFree(info->vector);
2133    info->vector = NIL(array_t);
2134  }
2135  if (info->fullVector) {
2136    ImgVectorFree(info->fullVector);
2137    info->fullVector = NIL(array_t);
2138  }
2139  if (info->partialBddVars)
2140    mdd_array_free(info->partialBddVars);
2141  if (info->partialVarFlag)
2142    FREE(info->partialVarFlag);
2143  if (info->fwdClusteredRelationArray != NIL(array_t)) {
2144    mdd_array_free(info->fwdClusteredRelationArray);
2145    info->fwdClusteredRelationArray = NIL(array_t);
2146  }
2147  if (info->bwdClusteredRelationArray != NIL(array_t)) {
2148    mdd_array_free(info->bwdClusteredRelationArray);
2149    info->bwdClusteredRelationArray = NIL(array_t);
2150  }
2151}
2152
2153
2154/**Function********************************************************************
2155
2156  Synopsis [Constrains the bit function and relation and creates a new
2157  transition function vector and relation.]
2158
2159  Description [Constrains the bit function and relation and creates a new
2160  transition function vector and relation. First, the existing transition
2161  function vector and relation is
2162  freed. The bit relation is created if it isnt stored already. The
2163  bit relation is then copied into the Clustered relation of the given
2164  direction and constrained by the given constraint. The bit relation
2165  is clustered. In the case of the backward relation, the clustered
2166  relation is minimized with respect to the care set.]
2167
2168  SideEffects [Frees current transition relation]
2169
2170******************************************************************************/
2171void
2172ImgImageConstrainAndClusterTransitionRelationTfm(Img_ImageInfo_t *imageInfo,
2173                                                Img_DirectionType direction,
2174                                                mdd_t *constrain,
2175                                                Img_MinimizeType minimizeMethod,
2176                                                boolean underApprox,
2177                                                boolean cleanUp,
2178                                                boolean forceReorder,
2179                                                int printStatus)
2180{
2181  ImgFunctionData_t     *functionData = &(imageInfo->functionData);
2182  ImgTfmInfo_t          *info = (ImgTfmInfo_t *)imageInfo->methodData;
2183  graph_t               *mddNetwork;
2184  mdd_manager           *mddManager = Part_PartitionReadMddManager(
2185                                        functionData->mddNetwork);
2186  int                   composeIntermediateVars, findIntermediateVars;
2187  array_t               *relationArray;
2188
2189  /* free existing function vector and/or relation */
2190  ImgImageFreeClusteredTransitionRelationTfm(imageInfo->methodData, direction);
2191  if (forceReorder)
2192    bdd_reorder(mddManager);
2193
2194  mddNetwork = functionData->mddNetwork;
2195
2196  /* create function vector or bit relation */
2197  if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c &&
2198      info->nVars != info->nRealVars) {
2199    if (info->option->composeIntermediateVars) {
2200      composeIntermediateVars = 1;
2201      findIntermediateVars = 0;
2202    } else {
2203      composeIntermediateVars = 0;
2204      findIntermediateVars = 1;
2205    }
2206  } else {
2207    composeIntermediateVars = 0;
2208    findIntermediateVars = 0;
2209  }
2210
2211  if (info->buildTR == 2) { /* non-deterministic */
2212    if (info->buildPartialTR) {
2213      info->fullVector = TfmCreateBitVector(info, composeIntermediateVars,
2214                                            findIntermediateVars);
2215      TfmSetupPartialTransitionRelation(info, &relationArray);
2216    } else {
2217      info->vector = NIL(array_t);
2218      relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars,
2219                                                findIntermediateVars);
2220    }
2221  } else {
2222    info->vector = TfmCreateBitVector(info, composeIntermediateVars,
2223                                        findIntermediateVars);
2224    if (info->buildTR == 0 || info->option->synchronizeTr)
2225      relationArray = NIL(array_t);
2226    else {
2227      relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars,
2228                                                findIntermediateVars);
2229    }
2230  }
2231
2232  /* apply the constrain to the bit relation */
2233  if (constrain) {
2234    if (underApprox) {
2235      MinimizeTransitionFunction(info->vector, relationArray,
2236                                 constrain, minimizeMethod, printStatus);
2237    } else {
2238      AddDontCareToTransitionFunction(info->vector, relationArray,
2239                                      constrain, minimizeMethod, printStatus);
2240    }
2241  }
2242
2243  if (info->vector && info->option->sortVectorFlag && info->option->useCache)
2244    array_sort(info->vector, CompareIndex);
2245  if (info->buildTR) {
2246    TfmBuildRelationArray(info, functionData, relationArray, direction, 0);
2247    if (relationArray)
2248      mdd_array_free(relationArray);
2249  }
2250
2251  /* Print information */
2252  if (info->option->verbosity > 0){
2253    if (info->method == Img_Tfm_c)
2254      fprintf(vis_stdout,"Computing Image Using tfm technique.\n");
2255    else
2256      fprintf(vis_stdout,"Computing Image Using hybrid technique.\n");
2257    fprintf(vis_stdout,"Total # of domain binary variables = %3d\n",
2258            array_n(functionData->domainBddVars));
2259    fprintf(vis_stdout,"Total # of range binary variables = %3d\n",
2260            array_n(functionData->rangeBddVars));
2261    fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n",
2262            array_n(functionData->quantifyBddVars));
2263    if (info->vector) {
2264      (void) fprintf(vis_stdout,
2265                     "Shared size of transition function vector for image ");
2266      (void) fprintf(vis_stdout,
2267                     "computation is %10ld BDD nodes (%-4d components)\n",
2268                     ImgVectorBddSize(info->vector), array_n(info->vector));
2269    }
2270    if (((direction == Img_Forward_c) || (direction == Img_Both_c)) &&
2271        (info->fwdClusteredRelationArray != NIL(array_t))) {
2272      (void) fprintf(vis_stdout,
2273                     "Shared size of transition relation for forward image ");
2274      (void) fprintf(vis_stdout,
2275                     "computation is %10ld BDD nodes (%-4d components)\n",
2276                     bdd_size_multiple(info->fwdClusteredRelationArray),
2277                     array_n(info->fwdClusteredRelationArray));
2278    }
2279    if (((direction == Img_Backward_c) || (direction == Img_Both_c)) &&
2280      (info->bwdClusteredRelationArray != NIL(array_t))) {
2281      (void) fprintf(vis_stdout,
2282                     "Shared size of transition relation for backward image ");
2283      (void) fprintf(vis_stdout,
2284                     "computation is %10ld BDD nodes (%-4d components)\n",
2285                     bdd_size_multiple(info->bwdClusteredRelationArray),
2286                     array_n(info->bwdClusteredRelationArray));
2287    }
2288  }
2289}
2290
2291
2292/**Function********************************************************************
2293
2294  Synopsis    [Check whether transition relation is built in hybrid.]
2295
2296  Description [Check whether transition relation is built in hybrid.]
2297
2298  SideEffects []
2299
2300******************************************************************************/
2301int
2302ImgIsPartitionedTransitionRelationTfm(Img_ImageInfo_t *imageInfo)
2303{
2304  ImgTfmInfo_t  *info = (ImgTfmInfo_t *)imageInfo->methodData;
2305
2306  if (info->buildTR)
2307    return(1);
2308  else
2309    return(0);
2310}
2311
2312
2313/*---------------------------------------------------------------------------*/
2314/* Definition of static functions                                            */
2315/*---------------------------------------------------------------------------*/
2316
2317
2318/**Function********************************************************************
2319
2320  Synopsis    [Allocates and initializes the info structure for
2321  transition function method.]
2322
2323  Description [Allocates and initializes the info structure for
2324  transition function method.]
2325
2326  SideEffects []
2327
2328******************************************************************************/
2329static ImgTfmInfo_t *
2330TfmInfoStructAlloc(Img_MethodType method)
2331{
2332  ImgTfmInfo_t  *info;
2333
2334  info = ALLOC(ImgTfmInfo_t, 1);
2335  memset(info, 0, sizeof(ImgTfmInfo_t));
2336  info->method = method;
2337  info->option = ImgTfmGetOptions(method);
2338  return(info);
2339}
2340
2341
2342/**Function********************************************************************
2343
2344  Synopsis    [Compares two variable indices of components.]
2345
2346  Description [Compares two variable indices of components.]
2347
2348  SideEffects []
2349
2350******************************************************************************/
2351static int
2352CompareIndex(const void *e1, const void *e2)
2353{
2354  ImgComponent_t        *c1, *c2;
2355  int                   id1, id2;
2356
2357  c1 = *((ImgComponent_t **)e1);
2358  c2 = *((ImgComponent_t **)e2);
2359
2360  id1 = (int)bdd_top_var_id(c1->var);
2361  id2 = (int)bdd_top_var_id(c2->var);
2362
2363  if (id1 > id2)
2364    return(1);
2365  else if (id1 < id2)
2366    return(-1);
2367  else
2368    return(0);
2369}
2370
2371
2372/**Function********************************************************************
2373
2374  Synopsis    [Flushes cache entries in a list.]
2375
2376  Description [Flushes cache entries in a list.]
2377
2378  SideEffects []
2379
2380******************************************************************************/
2381static int
2382HookInfoFunction(bdd_manager *mgr, char *str, void *method)
2383{
2384  ImgTfmInfo_t  *info;
2385  st_generator  *stGen;
2386
2387  if (HookInfoList) {
2388    st_foreach_item(HookInfoList, stGen, &info, NULL) {
2389      if (info->imgCache)
2390        ImgFlushCache(info->imgCache);
2391      if (info->preCache)
2392        ImgFlushCache(info->preCache);
2393    }
2394  }
2395  return(0);
2396}
2397
2398
2399/**Function********************************************************************
2400
2401  Synopsis    [Chooses variables for static splitting.]
2402
2403  Description [Chooses variables for static splitting. partialMethod is set
2404  by hybrid_partial_method. Refer to print_hybrid_options command.]
2405
2406  SideEffects []
2407
2408******************************************************************************/
2409static array_t *
2410ChoosePartialVars(ImgTfmInfo_t *info, array_t *vector, int nPartialVars,
2411                  int partialMethod)
2412{
2413  int                   i, j, nVars;
2414  ImgComponent_t        *comp;
2415  char                  *support;
2416  int                   *varCost;
2417  int                   big, small, nChosen, insert, id;
2418  mdd_t                 *var;
2419  int                   *partialVars = ALLOC(int, nPartialVars);
2420  array_t               *partialBddVars = array_alloc(mdd_t *, 0);
2421
2422  nVars = info->nVars;
2423  varCost = ALLOC(int, nVars);
2424  memset(varCost, 0, sizeof(int) * nVars);
2425
2426  if (partialMethod == 0) {
2427    /* chooses the variable whose function has the largest bdd size */
2428    for (i = 0; i < array_n(vector); i++) {
2429      comp = array_fetch(ImgComponent_t *, vector, i);
2430      id = (int)bdd_top_var_id(comp->var);
2431      varCost[id] = bdd_size(comp->func);
2432    }
2433  } else {
2434    /* chooses the variable that appears the most frequently */
2435    for (i = 0; i < array_n(vector); i++) {
2436      comp = array_fetch(ImgComponent_t *, vector, i);
2437      support = comp->support;
2438      for (j = 0; j < nVars; j++) {
2439        if (support[j])
2440          varCost[j]++;
2441      }
2442    }
2443  }
2444
2445  nChosen = 0;
2446  big = small = -1;
2447  for (i = 0; i < nVars; i++) {
2448    if (varCost[i] == 0)
2449      continue;
2450    if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
2451      continue;
2452    if (info->intermediateVarsTable &&
2453        st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) {
2454      continue;
2455    }
2456    if (nChosen == 0) {
2457      partialVars[0] = i;
2458      nChosen = 1;
2459      big = small = varCost[i];
2460    } else if (varCost[i] < small) {
2461      if (nChosen < nPartialVars) {
2462        partialVars[nChosen] = i;
2463        nChosen++;
2464        small = varCost[i];
2465      } else
2466        continue;
2467    } else if (varCost[i] > big) {
2468      if (nChosen < nPartialVars) {
2469        for (j = nChosen; j > 0; j--)
2470          partialVars[j] = partialVars[j - 1];
2471        partialVars[0] = i;
2472        nChosen++;
2473        big = varCost[i];
2474      } else {
2475        for (j = nPartialVars - 1; j > 0; j--)
2476          partialVars[j] = partialVars[j - 1];
2477        partialVars[0] = i;
2478        big = varCost[i];
2479        small = varCost[partialVars[nPartialVars - 1]];
2480      }
2481    } else {
2482      insert = nChosen;
2483      for (j = 0; j < nChosen; j++) {
2484        if (varCost[i] > varCost[partialVars[j]]) {
2485          insert = j;
2486          break;
2487        }
2488      }
2489      if (nChosen < nPartialVars) {
2490        for (j = nChosen; j > insert; j--)
2491          partialVars[j] = partialVars[j - 1];
2492        partialVars[insert] = i;
2493        nChosen++;
2494      } else if (insert < nChosen) {
2495        for (j = nPartialVars - 1; j > insert; j--)
2496          partialVars[j] = partialVars[j - 1];
2497        partialVars[insert] = i;
2498        small = varCost[partialVars[nPartialVars - 1]];
2499      }
2500    }
2501  }
2502  FREE(varCost);
2503
2504  for (i = 0; i < nChosen; i++) {
2505    var = bdd_var_with_index(info->manager, partialVars[i]);
2506    array_insert_last(mdd_t *, partialBddVars, var);
2507  }
2508
2509  FREE(partialVars);
2510  return(partialBddVars);
2511}
2512
2513
2514/**Function********************************************************************
2515
2516  Synopsis    [Prints statistics of recursions for transition function method.]
2517
2518  Description [Prints statistics of recursions for transition function method.]
2519
2520  SideEffects []
2521
2522  SeeAlso     []
2523
2524******************************************************************************/
2525static void
2526PrintRecursionStatistics(ImgTfmInfo_t *info, int preFlag)
2527{
2528  float avgDepth, avgDecomp;
2529  int   nRecurs, nLeaves, nTurns, nDecomps, topDecomp, maxDecomp, maxDepth;
2530
2531  GetRecursionStatistics(info, preFlag, &nRecurs, &nLeaves, &nTurns, &avgDepth,
2532                 &maxDepth, &nDecomps, &topDecomp, &maxDecomp, &avgDecomp);
2533  if (preFlag)
2534    fprintf(vis_stdout, "** recursion statistics of splitting (preImg) **\n");
2535  else
2536    fprintf(vis_stdout, "** recursion statistics of splitting (img) **\n");
2537  fprintf(vis_stdout, "# recursions = %d\n", nRecurs);
2538  fprintf(vis_stdout, "# leaves = %d\n", nLeaves);
2539  fprintf(vis_stdout, "# turns = %d\n", nTurns);
2540  fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n",
2541          avgDepth, maxDepth);
2542  if (!preFlag) {
2543    fprintf(vis_stdout,
2544            "# decompositions = %d (top = %d, max = %d, average = %g)\n",
2545            nDecomps, topDecomp, maxDecomp, avgDecomp);
2546  }
2547}
2548
2549
2550/**Function********************************************************************
2551
2552  Synopsis    [Prints statistics of finding essential and dependent variables.]
2553
2554  Description [Prints statistics of finding essential and dependent variables.]
2555
2556  SideEffects []
2557
2558  SeeAlso     []
2559
2560******************************************************************************/
2561static void
2562PrintFoundVariableStatistics(ImgTfmInfo_t *info, int preFlag)
2563{
2564  int   i, maxDepth;
2565
2566  if (preFlag) {
2567    fprintf(vis_stdout, "# split = %d, conjoin = %d\n",
2568            info->nSplitsB, info->nConjoinsB);
2569    return;
2570  }
2571
2572  fprintf(vis_stdout,
2573    "# found essential vars = %d (top = %d, average = %g, averageDepth = %g)\n",
2574          info->nFoundEssentials, info->topFoundEssentialDepth,
2575          info->averageFoundEssential, info->averageFoundEssentialDepth);
2576  if (info->option->printEssential == 1) {
2577    maxDepth = info->maxDepth < IMG_TF_MAX_PRINT_DEPTH ?
2578                info->maxDepth : IMG_TF_MAX_PRINT_DEPTH;
2579    fprintf(vis_stdout, "foundEssential:");
2580    for (i = 0; i < maxDepth; i++)
2581      fprintf(vis_stdout, " [%d]%d", i, info->foundEssentials[i]);
2582    fprintf(vis_stdout, "\n");
2583  }
2584  if (info->useConstraint == 2)
2585    fprintf(vis_stdout, "# range computations = %d\n", info->nRangeComps);
2586  fprintf(vis_stdout,
2587          "# found dependent vars = %d (average = %g)\n",
2588          info->nFoundDependVars, info->averageFoundDependVars);
2589  fprintf(vis_stdout, "# tautologous subimage = %d\n", info->nEmptySubImage);
2590  fprintf(vis_stdout, "# split = %d, conjoin = %d, cubeSplit = %d\n",
2591          info->nSplits, info->nConjoins, info->nCubeSplits);
2592}
2593
2594
2595/**Function********************************************************************
2596
2597  Synopsis    [Returns the statistics of recursions of transition function
2598  method.]
2599
2600  Description [Returns the statistics of recursions of transition function
2601  method.]
2602
2603  SideEffects []
2604
2605  SeeAlso     []
2606
2607******************************************************************************/
2608static void
2609GetRecursionStatistics(ImgTfmInfo_t *info, int preFlag, int *nRecurs,
2610                        int *nLeaves, int *nTurns, float *averageDepth,
2611                        int *maxDepth, int *nDecomps, int *topDecomp,
2612                        int *maxDecomp, float *averageDecomp)
2613{
2614  if (preFlag) {
2615    *nRecurs = info->nRecursionB;
2616    *nLeaves = info->nLeavesB;
2617    *nTurns = info->nTurnsB;
2618    *averageDepth = info->averageDepthB;
2619    *maxDepth = info->maxDepthB;
2620    *nDecomps = 0;
2621    *topDecomp = 0;
2622    *maxDecomp = 0;
2623    *averageDecomp = 0.0;
2624  } else {
2625    *nRecurs = info->nRecursion;
2626    *nLeaves = info->nLeaves;
2627    *nTurns = info->nTurns;
2628    *averageDepth = info->averageDepth;
2629    *maxDepth = info->maxDepth;
2630    *nDecomps = info->nDecomps;
2631    *topDecomp = info->topDecomp;
2632    *maxDecomp = info->maxDecomp;
2633    *averageDecomp = info->averageDecomp;
2634  }
2635}
2636
2637
2638/**Function********************************************************************
2639
2640  Synopsis    [Reads a set integer value.]
2641
2642  Description [Reads a set integer value.]
2643
2644  SideEffects []
2645
2646  SeeAlso     []
2647
2648******************************************************************************/
2649static int
2650ReadSetIntValue(char *string, int l, int u, int defaultValue)
2651{
2652  char  *flagValue;
2653  int   tmp;
2654  int   value = defaultValue;
2655
2656  flagValue = Cmd_FlagReadByName(string);
2657  if (flagValue != NIL(char)) {
2658    sscanf(flagValue, "%d", &tmp);
2659    if (tmp >= l && (tmp <= u || u == 0))
2660      value = tmp;
2661    else {
2662      fprintf(vis_stderr,
2663        "** tfm error: invalid value %d for %s[%d-%d]. **\n", tmp, string,
2664              l, u);
2665    }
2666  }
2667
2668  return(value);
2669}
2670
2671
2672/**Function********************************************************************
2673
2674  Synopsis    [Reads a set Boolean value.]
2675
2676  Description [Reads a set Boolean value.]
2677
2678  SideEffects []
2679
2680  SeeAlso     []
2681
2682******************************************************************************/
2683static boolean
2684ReadSetBooleanValue(char *string, boolean defaultValue)
2685{
2686  char          *flagValue;
2687  boolean       value = defaultValue;
2688
2689  flagValue = Cmd_FlagReadByName(string);
2690  if (flagValue != NIL(char)) {
2691    if (strcmp(flagValue, "yes") == 0)
2692      value = TRUE;
2693    else if (strcmp(flagValue, "no") == 0)
2694      value = FALSE;
2695    else {
2696      fprintf(vis_stderr,
2697              "** tfm error: invalid value %s for %s[yes/no]. **\n",
2698              flagValue, string);
2699    }
2700  }
2701
2702  return(value);
2703}
2704
2705
2706/**Function********************************************************************
2707
2708  Synopsis    [Traverses the partition recursively, creating the
2709  functions for the intermediate vertices.]
2710
2711  Description [Traverses the partition recursively, creating the
2712  functions for the intermediate vertices. This function is originated from
2713  PartitionTraverseRecursively in imgIwls95.c]
2714
2715  SideEffects []
2716
2717******************************************************************************/
2718static void
2719FindIntermediateVarsRecursively(ImgTfmInfo_t *info, mdd_manager *mddManager,
2720                                vertex_t *vertex, int mddId,
2721                                st_table *vertexTable, array_t *vector,
2722                                st_table *domainQuantifyVarMddIdTable,
2723                                array_t *intermediateVarMddIdArray)
2724{
2725  Mvf_Function_t        *mvf;
2726  lsList                faninEdges;
2727  lsGen                 gen;
2728  vertex_t              *faninVertex;
2729  edge_t                *faninEdge;
2730  array_t               *varBddFunctionArray, *bddArray;
2731  int                   i;
2732  mdd_t                 *var, *func;
2733  ImgComponent_t        *comp;
2734
2735  if (st_is_member(vertexTable, (char *)vertex))
2736    return;
2737  st_insert(vertexTable, (char *)vertex, NIL(char));
2738  if (mddId != -1) { /* This is not the next state function node */
2739    /* There is an mdd variable associated with this vertex */
2740    array_insert_last(int, intermediateVarMddIdArray, mddId);
2741    mvf = Part_VertexReadFunction(vertex);
2742    varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager, mddId, mvf);
2743    bddArray = mdd_id_to_bdd_array(mddManager, mddId);
2744    assert(array_n(varBddFunctionArray) == array_n(bddArray));
2745    for (i = 0; i < array_n(bddArray); i++) {
2746      var = array_fetch(mdd_t *, bddArray, i);
2747      func = array_fetch(mdd_t *, varBddFunctionArray, i);
2748      comp = ImgComponentAlloc(info);
2749      comp->var = var;
2750      comp->func = func;
2751      comp->intermediate = 1;
2752      ImgComponentGetSupport(comp);
2753      array_insert_last(ImgComponent_t *, vector, comp);
2754    }
2755    array_free(varBddFunctionArray);
2756    array_free(bddArray);
2757  }
2758  faninEdges = g_get_in_edges(vertex);
2759  if (lsLength(faninEdges) == 0)
2760    return;
2761  lsForEachItem(faninEdges, gen, faninEdge) {
2762    faninVertex = g_e_source(faninEdge);
2763    mddId = Part_VertexReadMddId(faninVertex);
2764    if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) {
2765      /* This is either domain var or quantify var */
2766      continue;
2767    }
2768    FindIntermediateVarsRecursively(info, mddManager, faninVertex, mddId,
2769                                    vertexTable, vector,
2770                                    domainQuantifyVarMddIdTable,
2771                                    intermediateVarMddIdArray);
2772  }
2773}
2774
2775
2776/**Function********************************************************************
2777
2778  Synopsis    [Traverses the partition recursively, creating the
2779  relations for the intermediate vertices.]
2780
2781  Description [Traverses the partition recursively, creating the
2782  relations for the intermediate vertices. This function is a copy of
2783  PartitionTraverseRecursively from imgIwls95.c.]
2784
2785  SideEffects []
2786
2787******************************************************************************/
2788static void
2789GetIntermediateRelationsRecursively(mdd_manager *mddManager, vertex_t *vertex,
2790                                    int mddId, st_table *vertexTable,
2791                                    array_t *relationArray,
2792                                    st_table *domainQuantifyVarMddIdTable,
2793                                    array_t *intermediateVarMddIdArray)
2794{
2795  Mvf_Function_t        *mvf;
2796  lsList                faninEdges;
2797  lsGen                 gen;
2798  vertex_t              *faninVertex;
2799  edge_t                *faninEdge;
2800  array_t               *varBddRelationArray;
2801
2802  if (st_is_member(vertexTable, (char *)vertex))
2803    return;
2804  st_insert(vertexTable, (char *)vertex, NIL(char));
2805  if (mddId != -1) { /* This is not the next state function node */
2806    /* There is an mdd variable associated with this vertex */
2807    array_insert_last(int, intermediateVarMddIdArray, mddId);
2808    mvf = Part_VertexReadFunction(vertex);
2809    varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf);
2810    array_append(relationArray, varBddRelationArray);
2811    array_free(varBddRelationArray);
2812  }
2813  faninEdges = g_get_in_edges(vertex);
2814  if (lsLength(faninEdges) == 0)
2815    return;
2816  lsForEachItem(faninEdges, gen, faninEdge) {
2817    faninVertex = g_e_source(faninEdge);
2818    mddId = Part_VertexReadMddId(faninVertex);
2819    if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) {
2820      /* This is either domain var or quantify var */
2821      continue;
2822    }
2823    GetIntermediateRelationsRecursively(mddManager, faninVertex, mddId,
2824                                        vertexTable, relationArray,
2825                                        domainQuantifyVarMddIdTable,
2826                                        intermediateVarMddIdArray);
2827  }
2828}
2829
2830
2831/**Function********************************************************************
2832
2833  Synopsis    [Checks whether the network is nondeterministic.]
2834
2835  Description [Checks whether the network is nondeterministic. However,
2836  current implementatin is just checking whether the network has multi-valued
2837  variables.]
2838
2839  SideEffects []
2840
2841  SeeAlso     []
2842
2843******************************************************************************/
2844static int
2845CheckNondeterminism(Ntk_Network_t *network)
2846{
2847  Ntk_Node_t            *node;
2848  lsGen                 gen;
2849  Var_Variable_t        *var;
2850  int                   numValues;
2851
2852  Ntk_NetworkForEachNode(network, gen, node) {
2853    var = Ntk_NodeReadVariable(node);
2854    numValues = Var_VariableReadNumValues(var);
2855    if (numValues > 2) {
2856      lsFinish(gen);
2857      return 1;
2858    }
2859  }
2860  return 0;
2861}
2862
2863
2864/**Function********************************************************************
2865
2866  Synopsis [Creates function vector.]
2867
2868  Description [Creates function vector.]
2869 
2870  SideEffects []
2871 
2872  SeeAlso [ImgImageInfoInitializeTfm]
2873 
2874******************************************************************************/
2875static array_t *
2876TfmCreateBitVector(ImgTfmInfo_t *info,
2877                   int composeIntermediateVars, int findIntermediateVars)
2878{
2879  int                   i, j;
2880  array_t               *vector;
2881  graph_t               *mddNetwork;
2882  mdd_manager           *mddManager;
2883  array_t               *roots;
2884  array_t               *rangeVarMddIdArray;
2885  int                   index;
2886  mdd_t                 *var;
2887  ImgComponent_t        *comp;
2888  st_table              *vertexTable;
2889  st_table              *domainQuantifyVarMddIdTable;
2890  array_t               *intermediateVarMddIdArray, *intermediateBddVars;
2891  int                   mddId;
2892  ImgFunctionData_t     *functionData = info->functionData;
2893
2894  mddNetwork = functionData->mddNetwork;
2895  mddManager = Part_PartitionReadMddManager(mddNetwork);
2896  roots = functionData->roots;
2897  rangeVarMddIdArray = functionData->rangeVars;
2898
2899  if (findIntermediateVars) {
2900    vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
2901    domainQuantifyVarMddIdTable = st_init_table(st_numcmp, st_numhash);
2902    intermediateVarMddIdArray = array_alloc(int, 0);
2903    arrayForEachItem(int, functionData->domainVars, i, mddId) {
2904      st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
2905    }
2906    arrayForEachItem(int, functionData->quantifyVars, i, mddId) {
2907      st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
2908    }
2909  } else {
2910    vertexTable = NIL(st_table);
2911    domainQuantifyVarMddIdTable = NIL(st_table);
2912    intermediateVarMddIdArray = NIL(array_t);
2913  }
2914
2915  vector = array_alloc(ImgComponent_t *, 0);
2916  /*
2917   * Iterate over the function of all the root nodes.
2918   */
2919  for (i = 0; i < array_n(roots); i++) {
2920    mdd_t *func;
2921    char *nodeName = array_fetch(char*, roots, i);
2922    vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName);
2923    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
2924    int mddId = array_fetch(int, rangeVarMddIdArray, i);
2925    array_t *varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager,
2926                                                                mddId, mvf);
2927    array_t *bddArray = mdd_id_to_bdd_array(mddManager, mddId);
2928
2929    assert(array_n(varBddFunctionArray) == array_n(bddArray));
2930    if (info->option->debug) {
2931      mdd_t *rel1, *rel2;
2932      array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager,
2933                                                                   mddId,
2934                                                                   mvf);
2935      for (j = 0; j < array_n(bddArray); j++) {
2936        var = array_fetch(mdd_t *, bddArray, j);
2937        func = array_fetch(mdd_t *, varBddFunctionArray, j);
2938        rel1 = array_fetch(mdd_t *, varBddRelationArray, j);
2939        rel2 = mdd_xnor(var, func);
2940        if (!mdd_equal(rel1, rel2)) {
2941          if (mdd_lequal(rel1, rel2, 1, 1))
2942            fprintf(vis_stdout, "** %d(%d): rel < funcRel\n", i, j);
2943          else if (mdd_lequal(rel2, rel1, 1, 1))
2944            fprintf(vis_stdout, "** %d(%d): rel > funcRel\n", i, j);
2945          else
2946            fprintf(vis_stdout, "** %d(%d): rel != funcRel\n", i, j);
2947        }
2948        mdd_free(rel1);
2949        mdd_free(rel2);
2950      }
2951
2952      array_free(varBddRelationArray);
2953    }
2954    for (j = 0; j < array_n(bddArray); j++) {
2955      var = array_fetch(mdd_t *, bddArray, j);
2956      func = array_fetch(mdd_t *, varBddFunctionArray, j);
2957      if (array_n(bddArray) == 1 && bdd_is_tautology(func, 1)) {
2958        array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager,
2959                                                                mddId, mvf);
2960        mdd_t *relation = array_fetch(mdd_t *, varBddRelationArray, 0);
2961        /* non-deterministic constant */
2962        if (bdd_is_tautology(relation, 1)) {
2963          mdd_array_free(varBddRelationArray);
2964          mdd_free(func);
2965          break;
2966        }
2967        mdd_array_free(varBddRelationArray);
2968      }
2969      comp = ImgComponentAlloc(info);
2970      comp->var = ImgSubstitute(var, functionData, Img_R2D_c);
2971      if (composeIntermediateVars) {
2972        comp->func = Img_ComposeIntermediateNodes(functionData->mddNetwork,
2973                  func, functionData->domainVars, functionData->rangeVars,
2974                  functionData->quantifyVars);
2975        mdd_free(func);
2976      } else
2977        comp->func = func;
2978      ImgComponentGetSupport(comp);
2979      array_insert_last(ImgComponent_t *, vector, comp);
2980    }
2981    if (findIntermediateVars) {
2982      int       n1, n2;
2983
2984      n1 = array_n(vector);
2985      FindIntermediateVarsRecursively(info, mddManager, vertex, -1,
2986                                        vertexTable, vector,
2987                                        domainQuantifyVarMddIdTable,
2988                                        intermediateVarMddIdArray);
2989      n2 = array_n(vector);
2990      info->nIntermediateVars += n2 - n1;
2991    }
2992    array_free(varBddFunctionArray);
2993    mdd_array_free(bddArray);
2994  }
2995  if (findIntermediateVars) {
2996    int nonExistFlag;
2997
2998    /* checks whether intermediate variables are already found */
2999    if (info->intermediateVarsTable && info->intermediateBddVars &&
3000        info->newQuantifyBddVars) {
3001      nonExistFlag = 0;
3002    } else {
3003      assert(!info->intermediateVarsTable);
3004      assert(!info->intermediateBddVars);
3005      assert(!info->newQuantifyBddVars);
3006      nonExistFlag = 1;
3007    }
3008
3009    if (info->option->verbosity) {
3010      (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n",
3011              info->nIntermediateVars);
3012    }
3013    st_free_table(vertexTable);
3014    st_free_table(domainQuantifyVarMddIdTable);
3015    if (nonExistFlag) {
3016      intermediateBddVars = mdd_id_array_to_bdd_array(mddManager,
3017                                                intermediateVarMddIdArray);
3018    } else
3019      intermediateBddVars = NIL(array_t);
3020    array_free(intermediateVarMddIdArray);
3021    if (nonExistFlag) {
3022      info->intermediateVarsTable = st_init_table(st_numcmp, st_numhash);
3023      for (i = 0; i < array_n(intermediateBddVars); i++) {
3024        var = array_fetch(mdd_t *, intermediateBddVars, i);
3025        index = (int)bdd_top_var_id(var);
3026        st_insert(info->intermediateVarsTable, (char *)(long)index, NIL(char));
3027      }
3028      info->newQuantifyBddVars = mdd_array_duplicate(
3029                                        functionData->quantifyBddVars);
3030      for (i = 0; i < array_n(intermediateBddVars); i++) {
3031        var = array_fetch(mdd_t *, intermediateBddVars, i);
3032        array_insert_last(mdd_t *, info->newQuantifyBddVars, mdd_dup(var));
3033      }
3034      info->intermediateBddVars = intermediateBddVars;
3035    }
3036  }
3037
3038  return(vector);
3039}
3040
3041
3042/**Function********************************************************************
3043
3044  Synopsis [Creates the bit relations.]
3045
3046  Description [Creates the bit relations.]
3047 
3048  SideEffects []
3049 
3050  SeeAlso [ImgImageInfoInitializeTfm]
3051 
3052******************************************************************************/
3053static array_t *
3054TfmCreateBitRelationArray(ImgTfmInfo_t *info,
3055                          int composeIntermediateVars, int findIntermediateVars)
3056{
3057  array_t               *bddRelationArray = array_alloc(mdd_t*, 0);
3058  ImgFunctionData_t     *functionData = info->functionData;
3059  array_t               *domainVarMddIdArray = functionData->domainVars;
3060  array_t               *rangeVarMddIdArray = functionData->rangeVars;
3061  array_t               *quantifyVarMddIdArray = functionData->quantifyVars;
3062  graph_t               *mddNetwork = functionData->mddNetwork;
3063  array_t               *roots = functionData->roots;
3064  int                   i, j, n1, n2, mddId, nIntermediateVars = 0;
3065  mdd_manager           *mddManager = Part_PartitionReadMddManager(mddNetwork);
3066  st_table              *vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
3067  st_table              *domainQuantifyVarMddIdTable =
3068                                st_init_table(st_numcmp, st_numhash);
3069  char                  *nodeName;
3070  mdd_t                 *relation, *composedRelation;
3071  array_t               *intermediateVarMddIdArray, *intermediateBddVars;
3072  int                   index;
3073  mdd_t                 *var;
3074
3075  if (findIntermediateVars)
3076    intermediateVarMddIdArray = array_alloc(int, 0);
3077  else
3078    intermediateVarMddIdArray = NIL(array_t);
3079
3080  arrayForEachItem(int, domainVarMddIdArray, i, mddId) {
3081    st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
3082  }
3083  arrayForEachItem(int, quantifyVarMddIdArray, i, mddId) {
3084    st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char));
3085  }
3086 
3087  arrayForEachItem(char *, roots, i, nodeName) {
3088    vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName);
3089    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
3090    int mddId = array_fetch(int, rangeVarMddIdArray, i);
3091   
3092    array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager,
3093                                                                 mddId, mvf);
3094    if (composeIntermediateVars) {
3095      for (j = 0; j < array_n(varBddRelationArray); j++) {
3096        relation = array_fetch(mdd_t *, varBddRelationArray, j);
3097        composedRelation = Img_ComposeIntermediateNodes(
3098                functionData->mddNetwork, relation, functionData->domainVars,
3099                functionData->rangeVars, functionData->quantifyVars);
3100        mdd_free(relation);
3101        array_insert(mdd_t *, varBddRelationArray, j, composedRelation);
3102      }
3103
3104      array_append(bddRelationArray, varBddRelationArray);
3105      array_free(varBddRelationArray);
3106    } else {
3107      array_append(bddRelationArray, varBddRelationArray);
3108      array_free(varBddRelationArray);
3109
3110      if (findIntermediateVars) {
3111        if (info->option->verbosity)
3112          n1 = array_n(bddRelationArray);
3113        GetIntermediateRelationsRecursively(mddManager, vertex, -1, vertexTable,
3114                                            bddRelationArray,
3115                                            domainQuantifyVarMddIdTable,
3116                                            intermediateVarMddIdArray);
3117        if (info->option->verbosity) {
3118          n2 = array_n(bddRelationArray);
3119          nIntermediateVars += n2 - n1;
3120        }
3121      }
3122    }
3123  }
3124
3125  st_free_table(vertexTable);
3126  st_free_table(domainQuantifyVarMddIdTable);
3127  if (findIntermediateVars) {
3128    int nonExistFlag;
3129
3130    /* checks whether intermediate variables are already found */
3131    if (info->intermediateVarsTable && info->intermediateBddVars &&
3132        info->newQuantifyBddVars) {
3133      nonExistFlag = 0;
3134    } else {
3135      assert(!info->intermediateVarsTable);
3136      assert(!info->intermediateBddVars);
3137      assert(!info->newQuantifyBddVars);
3138      nonExistFlag = 1;
3139    }
3140
3141    if (info->option->verbosity) {
3142      (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n",
3143              info->nIntermediateVars);
3144    }
3145    if (nonExistFlag) {
3146      intermediateBddVars = mdd_id_array_to_bdd_array(mddManager,
3147                                                intermediateVarMddIdArray);
3148    } else
3149      intermediateBddVars = NIL(array_t);
3150    array_free(intermediateVarMddIdArray);
3151    if (nonExistFlag) {
3152      info->intermediateVarsTable = st_init_table(st_numcmp, st_numhash);
3153      for (i = 0; i < array_n(intermediateBddVars); i++) {
3154        var = array_fetch(mdd_t *, intermediateBddVars, i);
3155        index = (int)bdd_top_var_id(var);
3156        st_insert(info->intermediateVarsTable, (char *)(long)index, NIL(char));
3157      }
3158      info->newQuantifyBddVars = mdd_array_duplicate(
3159                                        functionData->quantifyBddVars);
3160      for (i = 0; i < array_n(intermediateBddVars); i++) {
3161        var = array_fetch(mdd_t *, intermediateBddVars, i);
3162        array_insert_last(mdd_t *, info->newQuantifyBddVars, mdd_dup(var));
3163      }
3164      info->intermediateBddVars = intermediateBddVars;
3165    }
3166  }
3167  return(bddRelationArray);
3168}
3169
3170
3171/**Function********************************************************************
3172
3173  Synopsis [Builds partial vector and relation array.]
3174
3175  Description [Builds partial vector and relation array.]
3176 
3177  SideEffects []
3178 
3179  SeeAlso [ImgImageInfoInitializeTfm]
3180 
3181******************************************************************************/
3182static void
3183TfmSetupPartialTransitionRelation(ImgTfmInfo_t *info,
3184                                  array_t **partialRelationArray)
3185{
3186  int                   i, id;
3187  mdd_t                 *var, *relation;
3188  ImgComponent_t        *comp, *newComp;
3189  array_t               *partialVector;
3190  ImgFunctionData_t     *functionData = info->functionData;
3191
3192  if (!info->buildPartialTR)
3193    return;
3194
3195  info->partialBddVars = ChoosePartialVars(info, info->fullVector,
3196                                           info->option->nPartialVars,
3197                                           info->option->partialMethod);
3198  info->partialVarFlag = ALLOC(char, info->nVars);
3199  memset(info->partialVarFlag, 0, sizeof(char) * info->nVars);
3200  for (i = 0; i < array_n(info->partialBddVars); i++) {
3201    var = array_fetch(mdd_t *, info->partialBddVars, i);
3202    id = (int)bdd_top_var_id(var);
3203    info->partialVarFlag[id] = 1;
3204  }
3205
3206  partialVector = array_alloc(ImgComponent_t *, 0);
3207  if (partialRelationArray)
3208    *partialRelationArray = array_alloc(mdd_t *, 0);
3209
3210  for (i = 0; i < array_n(info->fullVector); i++) {
3211    comp = array_fetch(ImgComponent_t *, info->fullVector, i);
3212    id = (int)bdd_top_var_id(comp->var);
3213    if (info->partialVarFlag[id]) {
3214      newComp = ImgComponentCopy(info, comp);
3215      array_insert_last(ImgComponent_t *, partialVector, newComp);
3216
3217      if (newComp->intermediate)
3218        relation = mdd_xnor(newComp->var, newComp->func);
3219      else {
3220        var = ImgSubstitute(newComp->var, functionData, Img_D2R_c);
3221        relation = mdd_xnor(var, newComp->func);
3222        mdd_free(var);
3223      }
3224      array_insert_last(mdd_t *, *partialRelationArray, relation);
3225    }
3226  }
3227
3228  info->vector = partialVector;
3229}
3230
3231
3232/**Function********************************************************************
3233
3234  Synopsis [Builds relation array from function vector or bit relation.]
3235
3236  Description [Builds relation array from function vector or bit relation.]
3237 
3238  SideEffects []
3239 
3240  SeeAlso [ImgImageInfoInitializeTfm]
3241 
3242******************************************************************************/
3243static void
3244TfmBuildRelationArray(ImgTfmInfo_t *info, ImgFunctionData_t *functionData,
3245                        array_t *bitRelationArray,
3246                        Img_DirectionType directionType, int writeMatrix)
3247{
3248  int                   i;
3249  mdd_t                 *var, *relation;
3250  array_t               *relationArray;
3251  ImgComponent_t        *comp;
3252  int                   id;
3253  array_t               *domainVarBddArray, *quantifyVarBddArray;
3254  mdd_t                 *one, *res1, *res2;
3255  char                  filename[20];
3256  int                   composeIntermediateVars, findIntermediateVars;
3257
3258  if ((info->buildTR == 1 && info->option->synchronizeTr) ||
3259        info->buildPartialTR) {
3260    relationArray = array_alloc(mdd_t *, 0);
3261    if (info->fullVector) {
3262      for (i = 0; i < array_n(info->fullVector); i++) {
3263        comp = array_fetch(ImgComponent_t *, info->fullVector, i);
3264        id = (int)bdd_top_var_id(comp->var);
3265        if (!info->partialVarFlag[id]) {
3266          if (comp->intermediate)
3267            relation = mdd_xnor(comp->var, comp->func);
3268          else {
3269            var = ImgSubstitute(comp->var, functionData, Img_D2R_c);
3270            relation = mdd_xnor(var, comp->func);
3271            mdd_free(var);
3272          }
3273          array_insert_last(mdd_t *, relationArray, relation);
3274        }
3275      }
3276    } else {
3277      for (i = 0; i < array_n(info->vector); i++) {
3278        comp = array_fetch(ImgComponent_t *, info->vector, i);
3279        if (comp->intermediate)
3280          relation = mdd_xnor(comp->var, comp->func);
3281        else {
3282          var = ImgSubstitute(comp->var, functionData, Img_D2R_c);
3283          relation = mdd_xnor(var, comp->func);
3284          mdd_free(var);
3285        }
3286        array_insert_last(mdd_t *, relationArray, relation);
3287      }
3288    }
3289
3290    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
3291      if (info->imgKeepPiInTr) {
3292        if (info->intermediateBddVars)
3293          quantifyVarBddArray = info->intermediateBddVars;
3294        else
3295          quantifyVarBddArray = array_alloc(mdd_t *, 0);
3296        domainVarBddArray = array_join(info->domainVarBddArray,
3297                                        info->quantifyVarBddArray);
3298      } else {
3299        if (info->newQuantifyBddVars)
3300          quantifyVarBddArray = info->newQuantifyBddVars;
3301        else
3302          quantifyVarBddArray = info->quantifyVarBddArray;
3303        domainVarBddArray = info->domainVarBddArray;
3304      }
3305      info->fwdClusteredRelationArray = ImgClusterRelationArray(
3306        info->manager, info->functionData,
3307        info->option->trMethod, Img_Forward_c, info->trmOption,
3308        relationArray, domainVarBddArray, quantifyVarBddArray,
3309        info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray,
3310        &info->fwdSmoothVarCubeArray, 0);
3311      if (writeMatrix && info->option->writeSupportMatrix == 3) {
3312        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
3313        ImgWriteSupportMatrix(info, info->vector,
3314                                info->fwdClusteredRelationArray, filename);
3315      } else if (writeMatrix && info->option->writeSupportMatrix == 2) {
3316        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
3317        ImgWriteSupportMatrix(info, NIL(array_t),
3318                                info->fwdClusteredRelationArray, filename);
3319      }
3320      if (info->imgKeepPiInTr) {
3321        if (!info->intermediateBddVars)
3322          array_free(quantifyVarBddArray);
3323        array_free(domainVarBddArray);
3324      }
3325      if (info->option->checkEquivalence && (!info->fullVector)) {
3326        assert(ImgCheckEquivalence(info, info->vector,
3327                                   info->fwdClusteredRelationArray,
3328                                   NIL(mdd_t), NIL(mdd_t), 0));
3329      }
3330      if (info->option->debug) {
3331        one = mdd_one(info->manager);
3332        if (info->fullVector) {
3333          res1 = ImgImageByHybrid(info, info->fullVector, one);
3334          res2 = ImgImageByHybridWithStaticSplit(info, info->vector, one,
3335                                        info->fwdClusteredRelationArray,
3336                                        NIL(mdd_t), NIL(mdd_t));
3337        } else {
3338          res1 = ImgImageByHybrid(info, info->vector, one);
3339          res2 = ImgImageByHybridWithStaticSplit(info, NIL(array_t), one,
3340                                        info->fwdClusteredRelationArray,
3341                                        NIL(mdd_t), NIL(mdd_t));
3342        }
3343        assert(mdd_equal(res1, res2));
3344        mdd_free(one);
3345        mdd_free(res1);
3346        mdd_free(res2);
3347      }
3348    }
3349    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
3350      if (info->preKeepPiInTr) {
3351        if (info->intermediateBddVars)
3352          quantifyVarBddArray = info->intermediateBddVars;
3353        else
3354          quantifyVarBddArray = array_alloc(mdd_t *, 0);
3355        domainVarBddArray = array_join(info->domainVarBddArray,
3356                                        info->quantifyVarBddArray);
3357      } else {
3358        if (info->newQuantifyBddVars)
3359          quantifyVarBddArray = info->newQuantifyBddVars;
3360        else
3361          quantifyVarBddArray = info->quantifyVarBddArray;
3362        domainVarBddArray = info->domainVarBddArray;
3363      }
3364      info->bwdClusteredRelationArray = ImgClusterRelationArray(
3365        info->manager, info->functionData,
3366        info->option->trMethod, Img_Backward_c, info->trmOption,
3367        relationArray, domainVarBddArray, quantifyVarBddArray,
3368        info->rangeVarBddArray, &info->bwdArraySmoothVarBddArray,
3369        &info->bwdSmoothVarCubeArray, 0);
3370      if (writeMatrix && info->option->writeSupportMatrix == 3) {
3371        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
3372        ImgWriteSupportMatrix(info, info->vector,
3373                                info->bwdClusteredRelationArray, filename);
3374      } else if (writeMatrix && info->option->writeSupportMatrix == 2) {
3375        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
3376        ImgWriteSupportMatrix(info, NIL(array_t),
3377                                info->bwdClusteredRelationArray, filename);
3378      }
3379      if (info->preKeepPiInTr) {
3380        if (!info->intermediateBddVars)
3381          array_free(quantifyVarBddArray);
3382        array_free(domainVarBddArray);
3383      }
3384      if (info->option->checkEquivalence && (!info->fullVector)) {
3385        assert(ImgCheckEquivalence(info, info->vector,
3386                                   info->bwdClusteredRelationArray,
3387                                   NIL(mdd_t), NIL(mdd_t), 1));
3388      }
3389      if (info->option->debug) {
3390        one = mdd_one(info->manager);
3391        if (info->fullVector) {
3392          res1 = ImgImageByHybrid(info, info->fullVector, one);
3393          res2 = ImgImageByHybridWithStaticSplit(info, info->vector, one,
3394                                        info->bwdClusteredRelationArray,
3395                                        NIL(mdd_t), NIL(mdd_t));
3396        } else {
3397          res1 = ImgImageByHybrid(info, info->vector, one);
3398          res2 = ImgImageByHybridWithStaticSplit(info, NIL(array_t), one,
3399                                        info->bwdClusteredRelationArray,
3400                                        NIL(mdd_t), NIL(mdd_t));
3401        }
3402        assert(mdd_equal(res1, res2));
3403        mdd_free(one);
3404        mdd_free(res1);
3405        mdd_free(res2);
3406      }
3407    }
3408
3409    mdd_array_free(relationArray);
3410  } else {
3411    graph_t     *mddNetwork = functionData->mddNetwork;
3412
3413    if (bitRelationArray)
3414      relationArray = bitRelationArray;
3415    else {
3416      if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c &&
3417          info->nVars != info->nRealVars) {
3418        if (info->option->composeIntermediateVars) {
3419          composeIntermediateVars = 1;
3420          findIntermediateVars = 0;
3421        } else {
3422          composeIntermediateVars = 0;
3423          findIntermediateVars = 1;
3424        }
3425      } else {
3426        composeIntermediateVars = 0;
3427        findIntermediateVars = 0;
3428      }
3429
3430      relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars,
3431                                                findIntermediateVars);
3432    }
3433
3434    if (directionType == Img_Forward_c || directionType == Img_Both_c) {
3435      if (info->imgKeepPiInTr) {
3436        if (info->intermediateBddVars)
3437          quantifyVarBddArray = info->intermediateBddVars;
3438        else
3439          quantifyVarBddArray = array_alloc(mdd_t *, 0);
3440        domainVarBddArray = array_join(info->domainVarBddArray,
3441                                        info->quantifyVarBddArray);
3442      } else {
3443        if (info->newQuantifyBddVars)
3444          quantifyVarBddArray = info->newQuantifyBddVars;
3445        else
3446          quantifyVarBddArray = info->quantifyVarBddArray;
3447        domainVarBddArray = info->domainVarBddArray;
3448      }
3449      info->fwdClusteredRelationArray = ImgClusterRelationArray(
3450                info->manager, info->functionData, info->option->trMethod,
3451                Img_Forward_c, info->trmOption, relationArray,
3452                domainVarBddArray, quantifyVarBddArray,
3453                info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray,
3454                &info->fwdSmoothVarCubeArray, 0);
3455      if (writeMatrix && info->option->writeSupportMatrix >= 2) {
3456        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
3457        ImgWriteSupportMatrix(info, NIL(array_t),
3458                                info->fwdClusteredRelationArray, filename);
3459      }
3460      if (info->imgKeepPiInTr) {
3461        if (!info->intermediateBddVars)
3462          array_free(quantifyVarBddArray);
3463        array_free(domainVarBddArray);
3464      }
3465    }
3466    if (directionType == Img_Backward_c || directionType == Img_Both_c) {
3467      if (info->preKeepPiInTr) {
3468        if (info->intermediateBddVars)
3469          quantifyVarBddArray = info->intermediateBddVars;
3470        else
3471          quantifyVarBddArray = array_alloc(mdd_t *, 0);
3472        domainVarBddArray = array_join(info->domainVarBddArray,
3473                                        info->quantifyVarBddArray);
3474      } else {
3475        if (info->newQuantifyBddVars)
3476          quantifyVarBddArray = info->newQuantifyBddVars;
3477        else
3478          quantifyVarBddArray = info->quantifyVarBddArray;
3479        domainVarBddArray = info->domainVarBddArray;
3480      }
3481      info->bwdClusteredRelationArray = ImgClusterRelationArray(
3482        info->manager, info->functionData,
3483        info->option->trMethod, Img_Backward_c, info->trmOption,
3484        relationArray, domainVarBddArray, quantifyVarBddArray,
3485        info->rangeVarBddArray, &info->bwdArraySmoothVarBddArray,
3486        &info->bwdSmoothVarCubeArray, 0);
3487      if (writeMatrix && info->option->writeSupportMatrix >= 2) {
3488        sprintf(filename, "support%d.mat", info->option->supportFileCount++);
3489        ImgWriteSupportMatrix(info, NIL(array_t),
3490                                info->bwdClusteredRelationArray, filename);
3491      }
3492      if (info->preKeepPiInTr) {
3493        if (!info->intermediateBddVars)
3494          array_free(quantifyVarBddArray);
3495        array_free(domainVarBddArray);
3496      }
3497    }
3498
3499    if (!bitRelationArray)
3500      mdd_array_free(relationArray);
3501  }
3502}
3503
3504
3505/**Function********************************************************************
3506
3507  Synopsis [Rebuilds transition relation from function vector.]
3508
3509  Description [Rebuilds transition relation from function vector.]
3510 
3511  SideEffects []
3512 
3513  SeeAlso []
3514 
3515******************************************************************************/
3516static void
3517RebuildTransitionRelation(ImgTfmInfo_t *info, Img_DirectionType directionType)
3518{
3519  int                   i;
3520  mdd_t                 *var, *relation;
3521  ImgComponent_t        *comp;
3522  array_t               *relationArray;
3523  array_t               *quantifyVarBddArray, *domainVarBddArray;
3524
3525  relationArray = array_alloc(mdd_t *, 0);
3526
3527  for (i = 0; i < array_n(info->vector); i++) {
3528    comp = array_fetch(ImgComponent_t *, info->vector, i);
3529    var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
3530    relation = mdd_xnor(var, comp->func);
3531    array_insert_last(mdd_t *, relationArray, relation);
3532    mdd_free(var);
3533  }
3534
3535  if (directionType == Img_Forward_c || directionType == Img_Both_c) {
3536    mdd_array_free(info->fwdClusteredRelationArray);
3537    if (info->imgKeepPiInTr) {
3538      if (info->intermediateBddVars)
3539        quantifyVarBddArray = info->intermediateBddVars;
3540      else
3541        quantifyVarBddArray = array_alloc(mdd_t *, 0);
3542      domainVarBddArray = array_join(info->domainVarBddArray,
3543                                     info->quantifyVarBddArray);
3544    } else {
3545      if (info->newQuantifyBddVars)
3546        quantifyVarBddArray = info->newQuantifyBddVars;
3547      else
3548        quantifyVarBddArray = info->quantifyVarBddArray;
3549      domainVarBddArray = info->domainVarBddArray;
3550    }
3551    info->fwdClusteredRelationArray = ImgClusterRelationArray(
3552        info->manager, info->functionData, info->option->trMethod,
3553        Img_Forward_c, info->trmOption, relationArray,
3554        domainVarBddArray, quantifyVarBddArray,
3555        info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray,
3556        &info->fwdSmoothVarCubeArray, 0);
3557    if (info->imgKeepPiInTr) {
3558      if (!info->intermediateBddVars)
3559        array_free(quantifyVarBddArray);
3560      array_free(domainVarBddArray);
3561    }
3562  }
3563  if (directionType == Img_Backward_c || directionType == Img_Both_c) {
3564    mdd_array_free(info->bwdClusteredRelationArray);
3565    if (info->preKeepPiInTr) {
3566      if (info->intermediateBddVars)
3567        quantifyVarBddArray = info->intermediateBddVars;
3568      else
3569        quantifyVarBddArray = array_alloc(mdd_t *, 0);
3570      domainVarBddArray = array_join(info->domainVarBddArray,
3571                                     info->quantifyVarBddArray);
3572    } else {
3573      if (info->newQuantifyBddVars)
3574        quantifyVarBddArray = info->newQuantifyBddVars;
3575      else
3576        quantifyVarBddArray = info->quantifyVarBddArray;
3577      domainVarBddArray = info->domainVarBddArray;
3578    }
3579    info->bwdClusteredRelationArray = ImgClusterRelationArray(
3580            info->manager, info->functionData,
3581            info->option->trMethod, Img_Backward_c, info->trmOption,
3582            relationArray, domainVarBddArray, quantifyVarBddArray,
3583            info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray,
3584            &info->fwdSmoothVarCubeArray, 0);
3585    if (info->preKeepPiInTr) {
3586      if (!info->intermediateBddVars)
3587        array_free(quantifyVarBddArray);
3588      array_free(domainVarBddArray);
3589    }
3590  }
3591
3592  mdd_array_free(relationArray);
3593}
3594
3595
3596/**Function********************************************************************
3597
3598  Synopsis    [Minimizes function vector or relation with given constraint.]
3599
3600  Description [Minimizes function vector or relation with given constraint.]
3601
3602  SideEffects []
3603
3604******************************************************************************/
3605static void
3606MinimizeTransitionFunction(array_t *vector, array_t *relationArray,
3607                           mdd_t *constrain, Img_MinimizeType minimizeMethod,
3608                           int printStatus)
3609{
3610  int           i;
3611  bdd_t         *relation, *simplifiedRelation, *simplifiedFunc;
3612  long          sizeConstrain = 0, size = 0;
3613  ImgComponent_t *comp;
3614
3615  if (bdd_is_tautology(constrain, 1))
3616    return;
3617
3618  if (vector) {
3619    if (printStatus) {
3620      size = ImgVectorBddSize(vector);
3621      sizeConstrain = bdd_size(constrain);
3622    }
3623
3624    arrayForEachItem(ImgComponent_t *, vector, i, comp) {
3625      simplifiedFunc = Img_MinimizeImage(comp->func, constrain, minimizeMethod,
3626                                         TRUE);
3627      if (printStatus == 2) {
3628        (void)fprintf(vis_stdout,
3629            "IMG Info: minimized function %d | %ld => %d in component %d\n",
3630                      bdd_size(comp->func), sizeConstrain,
3631                      bdd_size(simplifiedFunc), i);
3632      }
3633      mdd_free(comp->func);
3634      comp->func = simplifiedFunc;
3635    }
3636
3637    if (printStatus) {
3638      (void) fprintf(vis_stdout,
3639       "IMG Info: minimized function [%ld | %ld => %ld] with %d components\n",
3640                     size, sizeConstrain,
3641                     ImgVectorBddSize(vector), array_n(vector));
3642    }
3643  }
3644
3645  if (relationArray) {
3646    if (printStatus) {
3647      size = bdd_size_multiple(relationArray);
3648      sizeConstrain = bdd_size(constrain);
3649    }
3650
3651    arrayForEachItem(bdd_t*, relationArray, i, relation) {
3652      simplifiedRelation = Img_MinimizeImage(relation, constrain,
3653                                             minimizeMethod, TRUE);
3654      if (printStatus == 2) {
3655        (void)fprintf(vis_stdout,
3656                "IMG Info: minimized relation %d | %ld => %d in component %d\n",
3657                      bdd_size(relation), sizeConstrain,
3658                      bdd_size(simplifiedRelation), i);
3659      }
3660      mdd_free(relation);
3661      array_insert(bdd_t *, relationArray, i, simplifiedRelation);
3662    }
3663
3664    if (printStatus) {
3665      (void) fprintf(vis_stdout,
3666       "IMG Info: minimized relation [%ld | %ld => %ld] with %d components\n",
3667                     size, sizeConstrain,
3668                     bdd_size_multiple(relationArray), array_n(relationArray));
3669    }
3670  }
3671}
3672
3673
3674/**Function********************************************************************
3675
3676  Synopsis    [Adds dont cares to function vector or relation.]
3677
3678  Description [Adds dont cares to function vector or relation.]
3679
3680  SideEffects []
3681
3682******************************************************************************/
3683static void
3684AddDontCareToTransitionFunction(array_t *vector, array_t *relationArray,
3685                                mdd_t *constrain,
3686                                Img_MinimizeType minimizeMethod,
3687                                int printStatus)
3688{
3689  int                   i;
3690  bdd_t                 *relation, *simplifiedRelation, *simplifiedFunc;
3691  long                  sizeConstrain = 0, size = 0;
3692  ImgComponent_t        *comp;
3693
3694  if (bdd_is_tautology(constrain, 1))
3695    return;
3696
3697  if (vector) {
3698    if (printStatus) {
3699      size = ImgVectorBddSize(vector);
3700      sizeConstrain = bdd_size(constrain);
3701    }
3702
3703    arrayForEachItem(ImgComponent_t *, vector, i, comp) {
3704      simplifiedFunc = Img_AddDontCareToImage(comp->func, constrain,
3705                                              minimizeMethod);
3706      if (printStatus == 2) {
3707        (void)fprintf(vis_stdout,
3708            "IMG Info: minimized function %d | %ld => %d in component %d\n",
3709                      bdd_size(comp->func), sizeConstrain,
3710                      bdd_size(simplifiedFunc), i);
3711      }
3712      mdd_free(comp->func);
3713      comp->func = simplifiedFunc;
3714    }
3715
3716    if (printStatus) {
3717      (void) fprintf(vis_stdout,
3718       "IMG Info: minimized function [%ld | %ld => %ld] with %d components\n",
3719                     size, sizeConstrain,
3720                     ImgVectorBddSize(vector), array_n(vector));
3721    }
3722  }
3723
3724  if (relationArray) {
3725    if (printStatus) {
3726      size = bdd_size_multiple(relationArray);
3727      sizeConstrain = bdd_size(constrain);
3728    }
3729
3730    arrayForEachItem(bdd_t*, relationArray, i, relation) {
3731      simplifiedRelation = Img_AddDontCareToImage(relation, constrain,
3732                                                  minimizeMethod);
3733      if (printStatus == 2) {
3734        (void)fprintf(vis_stdout,
3735                "IMG Info: minimized relation %d | %ld => %d in component %d\n",
3736                      bdd_size(relation), sizeConstrain,
3737                      bdd_size(simplifiedRelation), i);
3738      }
3739      mdd_free(relation);
3740      array_insert(bdd_t *, relationArray, i, simplifiedRelation);
3741    }
3742
3743    if (printStatus) {
3744      (void) fprintf(vis_stdout,
3745       "IMG Info: minimized relation [%ld | %ld => %ld] with %d components\n",
3746                     size, sizeConstrain,
3747                     bdd_size_multiple(relationArray), array_n(relationArray));
3748    }
3749  }
3750}
Note: See TracBrowser for help on using the repository browser.