source: vis_dev/vis-2.3/src/img/imgUtil.c @ 67

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

vis2.3
File size: 81.1 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [imgUtil.c]
4
5  PackageName [img]
6
7  Synopsis    [High-level routines to perform image computations.]
8
9  Description [This file provides the exported interface to the
10  method-specific image computation routines.
11
12  <p> Minimization of the transition relation can be done in three ways (for
13  Iwls95, not so sure about monolithic and hybrid) (RB):
14
15  <ol> <li>You can call MinimizeTR.  This way, you'll loose the old TR, though
16  it could potentially reconstruct it from the bit relations.  This is a good
17  option for (overapproximate) reachability info, since the TR will remain
18  valid.</li>
19
20
21  <li> You can call the triplet Img_DupTransitionRelation to copy the TR,
22  Img_MinimizeTransitionRelation to minimize the TR, and
23  Img_RestoreTransitionRelation to discard the minimized TR and to restore the
24  original. 
25 
26  <li>Finally, if you just want to minimize the TR for a single step,
27  you can pass the care set to the (pre)image computation routine.  This does
28  unfortunately (and queerly) not work for image, but only for preimage.  If
29  you pas a care set, the TR gets minimized, and the minimized relation is kept
30  and reused until you pass a different care set.  Hence, minimizaiton is not
31  done at every preimage computation, but only if you change the care set.
32 
33  </ol>]
34
35  Author      [Rajeev Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon, Kavita Ravi]
36
37  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
38  All rights reserved.
39
40  Permission is hereby granted, without written agreement and without license
41  or royalty fees, to use, copy, modify, and distribute this software and its
42  documentation for any purpose, provided that the above copyright notice and
43  the following two paragraphs appear in all copies of this software.
44
45  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
46  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
47  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
48  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
49
50  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
51  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
52  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
53  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
54  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
55
56******************************************************************************/
57#include "imgInt.h"
58
59static char rcsid[] UNUSED = "$Id: imgUtil.c,v 1.74 2005/05/14 21:08:32 jinh Exp $";
60
61/*---------------------------------------------------------------------------*/
62/* Variable declarations                                                     */
63/*---------------------------------------------------------------------------*/
64
65static  int     nImgComps = 0; /* number of image computations */
66static  int     nPreComps = 0; /* number of pre-image computations */
67
68/**AutomaticStart*************************************************************/
69
70/*---------------------------------------------------------------------------*/
71/* Static function prototypes                                                */
72/*---------------------------------------------------------------------------*/
73
74static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray);
75
76/**AutomaticEnd***************************************************************/
77
78
79/*---------------------------------------------------------------------------*/
80/* Definition of exported functions                                          */
81/*---------------------------------------------------------------------------*/
82Img_OptimizeType Img_ImageInfoObtainOptimizeType(Img_ImageInfo_t * imageInfo);
83void Img_ImageInfoSetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo);
84void Img_ImageInfoResetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo);
85void Img_ImageInfoResetLinearComputeRange(Img_ImageInfo_t * imageInfo);
86void Img_ImageInfoSetLinearComputeRange(Img_ImageInfo_t * imageInfo);
87
88
89/**Function********************************************************************
90
91  Synopsis    [Initialize the image package.]
92
93  SideEffects []
94
95  SeeAlso     [Img_End]
96
97******************************************************************************/
98void
99Img_Init(void)
100{
101  /* Set the default settings. */
102
103}
104
105/**Function********************************************************************
106
107  Synopsis    [End the image package.]
108
109  SideEffects []
110
111  SeeAlso     [Img_Init]
112
113******************************************************************************/
114void
115Img_End(void)
116{
117  /* Do Nothing. */
118}
119
120
121/**Function********************************************************************
122
123  Synopsis    [Return the image method preferred by the user.]
124
125  Description [Returns the method selected by Img_ImageInfoInitialize if
126  Img_Default_c is passed in.  Note that this may change if the user changes
127  the definition of the image_method set flag.]
128 
129  SideEffects []
130
131  SeeAlso     [Img_ImageInfoIninitialize]
132
133******************************************************************************/
134Img_MethodType
135Img_UserSpecifiedMethod(void)
136{
137  char *userSpecifiedMethod;
138 
139  userSpecifiedMethod = Cmd_FlagReadByName("image_method");
140
141  if (userSpecifiedMethod == NIL(char)) 
142    return IMGDEFAULT_METHOD;
143  if (strcmp(userSpecifiedMethod, "monolithic") == 0) 
144    return Img_Monolithic_c;
145  if (strcmp(userSpecifiedMethod, "tfm") == 0) 
146    return Img_Tfm_c;
147  if (strcmp(userSpecifiedMethod, "hybrid") == 0) 
148    return Img_Hybrid_c;
149  if (strcmp(userSpecifiedMethod, "iwls95") == 0)
150    return Img_Iwls95_c;
151  if (strcmp(userSpecifiedMethod, "mlp") == 0)
152    return Img_Mlp_c;
153
154  fprintf(vis_stderr, "** img error: Unrecognized image_method %s",
155                 userSpecifiedMethod);
156  fprintf(vis_stderr,  "using default method.\n");
157
158  return IMGDEFAULT_METHOD;
159}
160
161/**Function********************************************************************
162
163  Synopsis    [Initializes an imageInfo structure for the given method and
164  direction.]
165
166  Description [Initializes an imageInfo structure.  MethodType specifies which
167  image computation method to use.  If methodType is Img_Default_c, then if
168  the user-settable flag "image_method" has been set, then this method is
169  used, otherwise some default is used. DirectionType specifies which types of
170  image computations will be performed (forward, backward, or both).
171  Method-specific initialization takes into account the value of relevant
172  parameters in the global flag table.<p>
173
174  MddNetwork is a graph representing the functions to be used.  Each vertex of
175  the graph contains a multi-valued function (MVF) and an MDD id.  The MVF
176  gives the function of the vertex in terms of the MDD ids of the immediate
177  fanins of the vertex.<p>
178
179  Roots is an array of char* specifying the vertices of the graph which
180  represent those functions for which we want to compute the image (it must
181  not be empty); for example, for an FSM, roots represent the next state
182  functions.  DomainVars is an array of mddIds; for an FSM, these are the
183  present state variables.  Subsets of the domain are defined over these
184  variables. RangeVars is an array of mddIds over which the range is
185  expressed; for an FSM, these are the next state variables.  This array must
186  be in one-to-one correspondence with the array of roots.  QuantifyVars is an
187  array of mddIds, representing variables to be quantified from results of
188  backward images; for an FSM, these are the input variables.  This array may
189  be empty. No copies are made of any of the input parameters, and thus it is
190  the application's responsibility to free this data *after* the returned
191  Img_ImageInfo_t is freed.]
192
193  Comment     [To add a new method, see the instructions at the top of imgInt.h.]
194
195  SideEffects []
196
197  SeeAlso     [Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd Img_ImageInfoFree]
198
199******************************************************************************/
200Img_ImageInfo_t *
201Img_ImageInfoInitialize(
202  Img_ImageInfo_t *imageInfo,
203  graph_t * mddNetwork,
204  array_t * roots,
205  array_t * domainVars,
206  array_t * rangeVars,
207  array_t * quantifyVars,
208  mdd_t * domainCube,
209  mdd_t * rangeCube,
210  mdd_t * quantifyCube,
211  Ntk_Network_t * network,
212  Img_MethodType methodType,
213  Img_DirectionType  directionType,
214  int FAFWFlag,
215  mdd_t *Winning)
216{
217  char *flagValue;
218  int verbosity;
219  mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork);
220  int updateFlag = 0;
221
222  assert(array_n(roots) != 0);
223
224  /* If it does not exist, create a new one and initialize fields appropriately
225  */
226  if (imageInfo == NIL(Img_ImageInfo_t)) {
227    imageInfo = ALLOC(Img_ImageInfo_t, 1);
228    memset(imageInfo, 0, sizeof(Img_ImageInfo_t));
229    imageInfo->directionType = directionType;
230    if (Cmd_FlagReadByName("linear_optimize")) 
231      imageInfo->linearOptimize = Opt_NS;
232
233    /*
234     * Initialization of the function structure inside ImageInfo .
235     * Since no duplication is needed, this process is not encapsulated
236     * inside a static procedure.
237     */
238    imageInfo->functionData.FAFWFlag     = FAFWFlag;
239    imageInfo->functionData.Winning     = Winning;
240    imageInfo->functionData.mddNetwork   = mddNetwork;
241    imageInfo->functionData.roots        = roots;
242    imageInfo->functionData.domainVars   = domainVars;
243    imageInfo->functionData.rangeVars    = rangeVars;
244    imageInfo->functionData.quantifyVars = quantifyVars;
245    imageInfo->functionData.domainCube   = domainCube;
246    imageInfo->functionData.rangeCube    = rangeCube;
247    imageInfo->functionData.quantifyCube = quantifyCube;
248    imageInfo->functionData.domainBddVars = mdd_id_array_to_bdd_array(
249                                                mddManager, domainVars);
250    imageInfo->functionData.rangeBddVars = mdd_id_array_to_bdd_array(
251                                                mddManager, rangeVars);
252    imageInfo->functionData.quantifyBddVars = mdd_id_array_to_bdd_array(
253                                                mddManager, quantifyVars);
254    if (bdd_get_package_name() == CUDD) {
255      int i, nVars, idD, idR;
256      mdd_t *varD, *varR;
257
258      nVars = bdd_num_vars(mddManager);
259      imageInfo->functionData.permutD2R = ALLOC(int, sizeof(int) * nVars);
260      imageInfo->functionData.permutR2D = ALLOC(int, sizeof(int) * nVars);
261      for (i = 0; i < nVars; i++) {
262        imageInfo->functionData.permutD2R[i] = i;
263        imageInfo->functionData.permutR2D[i] = i;
264      }
265      nVars = array_n(imageInfo->functionData.rangeBddVars);
266      for (i = 0; i < nVars; i++) {
267        varD = array_fetch(bdd_t *, imageInfo->functionData.domainBddVars, i);
268        varR = array_fetch(bdd_t *, imageInfo->functionData.rangeBddVars, i);
269        idD = (int)bdd_top_var_id(varD);
270        idR = (int)bdd_top_var_id(varR);
271        imageInfo->functionData.permutD2R[idD] = idR;
272        imageInfo->functionData.permutR2D[idR] = idD;
273      }
274    } else {
275      imageInfo->functionData.permutD2R = NIL(int);
276      imageInfo->functionData.permutR2D = NIL(int);
277    }
278    if (domainCube)
279      imageInfo->functionData.createVarCubesFlag = 1;
280    imageInfo->functionData.network      = network;
281    imageInfo->methodData                = NIL(void);
282    updateFlag = 1;
283  }
284
285  /*
286   * If methodType is default, use user-specified method if set.
287   */
288  if (methodType == Img_Default_c)
289    methodType = Img_UserSpecifiedMethod();
290
291  /* If image_method changes, we need to free existing method data and
292   * to update proper function calls.
293   */
294  if (imageInfo->methodData) {
295    if (imageInfo->methodType != methodType) {
296      (*imageInfo->imageFreeProc)(imageInfo->methodData);
297      imageInfo->methodData = NIL(void);
298      updateFlag = 1;
299    }
300  }
301
302  if (updateFlag) {
303    imageInfo->methodType = methodType;
304    switch (methodType) {
305    case Img_Monolithic_c:
306      imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdMono;
307      imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdMono;
308      imageInfo->imageComputeFwdWithDomainVarsProc =
309        ImgImageInfoComputeFwdWithDomainVarsMono;
310      imageInfo->imageComputeBwdWithDomainVarsProc =
311        ImgImageInfoComputeBwdWithDomainVarsMono;
312      imageInfo->imageFreeProc       = ImgImageInfoFreeMono;
313      imageInfo->imagePrintMethodParamsProc =
314        ImgImageInfoPrintMethodParamsMono;
315      break;
316
317    case Img_Tfm_c:
318    case Img_Hybrid_c:
319      imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdTfm;
320      imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdTfm;
321      imageInfo->imageComputeFwdWithDomainVarsProc =
322        ImgImageInfoComputeFwdWithDomainVarsTfm;
323      imageInfo->imageComputeBwdWithDomainVarsProc =
324        ImgImageInfoComputeBwdWithDomainVarsTfm;
325      imageInfo->imageFreeProc       = ImgImageInfoFreeTfm;
326      imageInfo->imagePrintMethodParamsProc =
327        ImgImageInfoPrintMethodParamsTfm;
328      break;
329
330    case Img_Linear_Range_c:
331    case Img_Iwls95_c:
332    case Img_Mlp_c:
333    case Img_Linear_c:
334      imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdIwls95;
335      imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdIwls95;
336      imageInfo->imageComputeFwdWithDomainVarsProc =
337        ImgImageInfoComputeFwdWithDomainVarsIwls95;
338      imageInfo->imageComputeBwdWithDomainVarsProc =
339        ImgImageInfoComputeBwdWithDomainVarsIwls95;
340      imageInfo->imageFreeProc       = ImgImageInfoFreeIwls95;
341      imageInfo->imagePrintMethodParamsProc =
342        ImgImageInfoPrintMethodParamsIwls95;
343      break;
344
345    default:
346      fail("** img error: Unexpected type when updating image method");
347    }
348    imageInfo->fwdTrMinimizedFlag = FALSE;
349    imageInfo->bwdTrMinimizedFlag = FALSE;
350    imageInfo->printMinimizeStatus = 0;
351    imageInfo->savedRelation = NIL(void);
352
353    flagValue = Cmd_FlagReadByName("image_verbosity");
354    if (flagValue != NIL(char)) {
355      verbosity = atoi(flagValue);
356      imageInfo->verbosity = verbosity;
357      if (verbosity == 1)
358        imageInfo->printMinimizeStatus = 1;
359      else if (verbosity > 1)
360        imageInfo->printMinimizeStatus = 2;
361    }
362  }
363
364  /*
365   * Perform method-specific initialization of methodData.
366   */
367  switch (imageInfo->methodType) {
368      case Img_Monolithic_c:
369        imageInfo->methodData =
370            ImgImageInfoInitializeMono(imageInfo->methodData,
371                                       &(imageInfo->functionData),
372                                       directionType);
373        break;
374      case Img_Tfm_c:
375      case Img_Hybrid_c:
376        imageInfo->methodData =
377            ImgImageInfoInitializeTfm(imageInfo->methodData,
378                                      &(imageInfo->functionData),
379                                      directionType,
380                                      imageInfo->methodType);
381        break;
382      case Img_Iwls95_c:
383      case Img_Mlp_c:
384      case Img_Linear_c:
385      case Img_Linear_Range_c:
386        imageInfo->methodData =
387            ImgImageInfoInitializeIwls95(imageInfo->methodData,
388                                         &(imageInfo->functionData),
389                                         directionType,
390                                         imageInfo->methodType);
391        break;
392
393      default:
394        fail("IMG Error : Unexpected type when initalizing image method");
395  }
396  return imageInfo;
397}
398
399/**Function********************************************************************
400
401  Synopsis [Check the given address of mdd_t is same as the  functionData.quantifyCube.]
402
403  Description [This function is for remove memory leakage.]
404
405  SideEffects []
406
407  SeeAlso     [Img_ImageInfoInitialize]
408
409******************************************************************************/
410
411int Img_IsQuantifyCubeSame(
412  Img_ImageInfo_t *imageInfo,
413  mdd_t *quantifyCube)
414{
415  if(imageInfo->functionData.quantifyCube == quantifyCube)
416    return (1);
417  else 
418    return(0);
419}
420
421/**Function********************************************************************
422
423  Synopsis [Check the given address of array+t is same as the  functionData.quantifyArray.]
424
425  Description [This function is for remove memory leakage.]
426
427  SideEffects []
428
429  SeeAlso     [Img_ImageInfoInitialize]
430
431******************************************************************************/
432
433int Img_IsQuantifyArraySame(
434  Img_ImageInfo_t *imageInfo,
435  array_t *quantifyArray)
436{
437  if(imageInfo->functionData.quantifyVars == quantifyArray)
438    return (1);
439  else 
440    return(0);
441}
442
443/**Function********************************************************************
444
445  Synopsis [Updates present state and primary input variables.]
446
447  Description [Updates present state and primary input variables.
448  This function is called after calling ImageInfoInitialize for a
449  subFsm.]
450
451  SideEffects []
452
453  SeeAlso     [Img_ImageInfoInitialize]
454
455******************************************************************************/
456void
457Img_ImageInfoUpdateVariables(
458  Img_ImageInfo_t *imageInfo,
459  graph_t * mddNetwork,
460  array_t * domainVars,
461  array_t * quantifyVars,
462  mdd_t * domainCube,
463  mdd_t * quantifyCube)
464{
465  mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork);
466
467  imageInfo->functionData.domainVars   = domainVars;
468  imageInfo->functionData.quantifyVars = quantifyVars;
469  imageInfo->functionData.domainCube   = domainCube;
470  imageInfo->functionData.quantifyCube = quantifyCube;
471  mdd_array_free(imageInfo->functionData.domainBddVars);
472  imageInfo->functionData.domainBddVars = mdd_id_array_to_bdd_array(
473                                                mddManager, domainVars);
474  mdd_array_free(imageInfo->functionData.quantifyBddVars);
475  imageInfo->functionData.quantifyBddVars = mdd_id_array_to_bdd_array(
476                                                mddManager, quantifyVars);
477}
478
479
480/**Function********************************************************************
481
482  Synopsis [Sets the flag to allow the next image computation to
483  return a subset of the actual image.]
484
485  Description [Sets the flag to allow the next image computation to
486  return a subset of the actual image. Default is to not allow partial
487  image computations. This flag is reset at the end of every
488  image/preimage computation i.e., has to be specified before every
489  image/preimage computation if partial image is desired. ]
490
491  SideEffects [Flag is reset at the end of every image/preimage
492  computation.]
493
494  SeeAlso     [Img_ImageWasPartialImage]
495
496******************************************************************************/
497void
498Img_ImageAllowPartialImage(Img_ImageInfo_t *info,
499                          boolean value)
500{
501 if (info->methodType == Img_Iwls95_c || info->methodType == Img_Mlp_c) {
502   ImgImageAllowPartialImageIwls95(info->methodData, value);
503 }
504 return;
505}
506
507/**Function********************************************************************
508
509  Synopsis [Prints partial image options.]
510
511  Description [Prints partial image options.]
512
513  SideEffects []
514
515******************************************************************************/
516void
517Img_ImagePrintPartialImageOptions(void)
518{
519  ImgPrintPartialImageOptions();
520  return;
521}
522
523
524/**Function********************************************************************
525
526  Synopsis    [Queries whether the last image computation was partial.]
527
528  Description [Queries whether the last image computation was
529  partial. Reset before every image/preimage computation i.e., this
530  information is valid for only the previous image/preimage
531  computation.]
532
533  SideEffects [Reset before every image/preimage computation.]
534
535  SeeAlso     [Img_ImageAllowPartialImage]
536
537******************************************************************************/
538boolean
539Img_ImageWasPartial(Img_ImageInfo_t *info)
540{
541 if (info->methodType == Img_Iwls95_c || info->methodType == Img_Mlp_c)
542   return (ImgImageWasPartialIwls95(info->methodData));
543 else
544   return FALSE;
545}
546
547/**Function********************************************************************
548
549  Synopsis [Computes the forward image of a set and expresses it in terms of
550  domain variables.]
551
552  Description [Computes the forward image of a set and expresses it in terms
553  of domain variables. FromLowerBound, fromUpperBound, and toCareSet are
554  expressed in terms of domain variables. See Img_ImageInfoComputeFwd for more
555  information. (Takes care set as an array.)]
556
557  SideEffects []
558
559  SeeAlso     [Img_ImageInfoComputeFwd]
560
561******************************************************************************/
562mdd_t *
563Img_ImageInfoComputeImageWithDomainVars(
564  Img_ImageInfo_t * imageInfo,
565  mdd_t           * fromLowerBound,
566  mdd_t           * fromUpperBound,
567  array_t         * toCareSetArray)
568{
569  mdd_t         *image;
570  mdd_manager   *mddManager;
571  long          peakMem;
572  int           peakLiveNode;
573
574  if (mdd_is_tautology(fromLowerBound, 0)){
575    mddManager = Part_PartitionReadMddManager(
576        imageInfo->functionData.mddNetwork);
577    return (mdd_zero(mddManager));
578  }
579  image  = ((*imageInfo->imageComputeFwdWithDomainVarsProc)
580            (&(imageInfo->functionData), imageInfo,
581             fromLowerBound, fromUpperBound, toCareSetArray));
582  nImgComps++;
583
584  if (imageInfo->verbosity >= 2 && bdd_get_package_name() == CUDD) {
585    mddManager = Part_PartitionReadMddManager(
586        imageInfo->functionData.mddNetwork);
587    peakMem = bdd_read_peak_memory(mddManager);
588    peakLiveNode = bdd_read_peak_live_node(mddManager);
589    fprintf(vis_stdout, "** img info: current peak memory = %ld\n", peakMem);
590    fprintf(vis_stdout, "** img info: current peak live nodes = %d\n",
591            peakLiveNode);
592  }
593#ifndef NDEBUG
594  assert(CheckImageValidity(
595    Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork),
596    image,
597    imageInfo->functionData.rangeVars,
598    imageInfo->functionData.quantifyVars));
599#endif
600  return(image);
601}
602
603/**Function********************************************************************
604
605  Synopsis [Computes the forward image of a set and expresses it in terms of
606  domain variables.]
607
608  Description [Computes the forward image of a set and expresses it in terms
609  of domain variables. FromLowerBound, fromUpperBound, and toCareSet are
610  expressed in terms of domain variables. See Img_ImageInfoComputeFwd for more
611  information. (Takes care states as a set.)]
612
613  SideEffects []
614
615  SeeAlso     [Img_ImageInfoComputeFwd]
616
617******************************************************************************/
618mdd_t *
619Img_ImageInfoComputeFwdWithDomainVars(
620  Img_ImageInfo_t * imageInfo,
621  mdd_t           * fromLowerBound,
622  mdd_t           * fromUpperBound,
623  mdd_t           * toCareSet)
624{
625  array_t       *toCareSetArray;
626  mdd_t         *image;
627
628  toCareSetArray = array_alloc(mdd_t *, 0);
629  array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
630  image = Img_ImageInfoComputeImageWithDomainVars(imageInfo, fromLowerBound,
631                                        fromUpperBound, toCareSetArray);
632  array_free(toCareSetArray);
633  return(image);
634}
635
636
637/**Function********************************************************************
638
639  Synopsis    [Computes the forward image of a set.]
640
641  Description [Computes the forward image of a set, under the function vector
642  in imageInfo, using the image computation method specified in imageInfo.  The
643  set for which the forward image is computed is some set containing
644  fromLowerBound and contained in fromUpperBound. The exact set used is chosen
645  to simplify the computation.  ToCareSet specifies those forward image points
646  of interest; any points not in this set may or may not belong to the returned
647  set.  The MDDs fromLowerBound and fromUpperBound are defined over the domain
648  variables.  The MDD toCareSet and the returned MDD are defined over the range
649  variables. If fromLowerBound is zero, then zero will be returned. (Takes care
650  states as an array.)]
651
652  SideEffects []
653
654  SeeAlso     [Img_ImageInfoInitialize Img_ImageInfoComputeBwd
655  Img_ImageInfoFree Img_ImageInfoComputeFwdWithDomainVars]
656
657******************************************************************************/
658mdd_t *
659Img_ImageInfoComputeFwd(Img_ImageInfo_t * imageInfo,
660                        mdd_t * fromLowerBound,
661                        mdd_t * fromUpperBound,
662                        array_t * toCareSetArray)
663{
664  mdd_t *image;
665  if (mdd_is_tautology(fromLowerBound, 0)){
666    mdd_manager *mddManager = Part_PartitionReadMddManager(
667        imageInfo->functionData.mddNetwork);
668    return (mdd_zero(mddManager));
669  }
670  image =  ((*imageInfo->imageComputeFwdProc) (&(imageInfo->functionData),
671                                               imageInfo,
672                                               fromLowerBound,
673                                               fromUpperBound,
674                                               toCareSetArray));
675  nImgComps++;
676#ifndef NDEBUG
677  assert(CheckImageValidity(
678    Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork),
679    image,
680    imageInfo->functionData.domainVars,
681    imageInfo->functionData.quantifyVars));
682#endif
683  return image;
684}
685
686
687/**Function********************************************************************
688
689  Synopsis [Computes the backward image of a set expressed in terms of domain
690  variables.]
691
692  Description [Computes the backward image of a set expressed in terms
693  of domain variables. FromLowerBound, fromUpperBound, and
694  toCareSetArray are expressed in terms of domain variables. See
695  Img_ImageInfoComputeBwd for more information.  This function takes a
696  care-set array, as opposed to Img_ImageInfoComputeBwdWithDomainVars,
697  which takes a care set.]
698
699  SideEffects []
700
701  SeeAlso     [Img_ImageInfoComputeBwd]
702
703******************************************************************************/
704mdd_t *
705Img_ImageInfoComputePreImageWithDomainVars(
706  Img_ImageInfo_t * imageInfo,
707  mdd_t           * fromLowerBound,
708  mdd_t           * fromUpperBound,
709  array_t         * toCareSetArray)
710{
711  mdd_t *image;
712  if (mdd_is_tautology(fromLowerBound, 0)){
713    mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
714    return (mdd_zero(mddManager));
715  }
716  image =  ((*imageInfo->imageComputeBwdWithDomainVarsProc)
717            (&(imageInfo->functionData), imageInfo,
718             fromLowerBound, fromUpperBound, toCareSetArray));
719  nPreComps++;
720#ifndef NDEBUG
721  assert(CheckImageValidity(
722    Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork),
723    image,
724    imageInfo->functionData.rangeVars,
725    imageInfo->functionData.quantifyVars));
726#endif
727  return image;
728}
729/**Function********************************************************************
730
731  Synopsis [Computes the backward image of a set expressed in terms of domain
732  variables.]
733
734  Description [Computes the backward image of a set expressed in terms
735  of domain variables. FromLowerBound, fromUpperBound, and
736  toCareSetArray are expressed in terms of domain variables. See
737  Img_ImageInfoComputeBwd for more information.  This function takes a
738  care-set array, as opposed to Img_ImageInfoComputeBwdWithDomainVars,
739  which takes a care set.]
740
741  SideEffects []
742
743  SeeAlso     [Img_ImageInfoComputeBwd]
744
745******************************************************************************/
746mdd_t *
747Img_ImageInfoComputeEXWithDomainVars(
748  Img_ImageInfo_t * imageInfo,
749  mdd_t           * fromLowerBound,
750  mdd_t           * fromUpperBound,
751  array_t         * toCareSetArray)
752{
753  mdd_t *image;
754  if (mdd_is_tautology(fromLowerBound, 0)){
755    mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
756    return (mdd_zero(mddManager));
757  }
758  image =  ((*imageInfo->imageComputeBwdWithDomainVarsProc)
759            (&(imageInfo->functionData), imageInfo,
760             fromLowerBound, fromUpperBound, toCareSetArray));
761  nPreComps++;
762
763  return image;
764}
765
766
767/**Function********************************************************************
768
769  Synopsis [Computes the backward image of a set expressed in terms of domain
770  variables.]
771
772  Description [Computes the backward image of a set expressed in terms of
773  domain variables. FromLowerBound, fromUpperBound, and toCareSet are
774  expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more
775  information.  This function takes a care set, as opposed to ComputeBwd,
776  which takes a care-set array.]
777
778  SideEffects []
779
780  SeeAlso     [Img_ImageInfoComputeBwd]
781
782******************************************************************************/
783mdd_t *
784Img_ImageInfoComputeBwdWithDomainVars(
785  Img_ImageInfo_t * imageInfo,
786  mdd_t           * fromLowerBound,
787  mdd_t           * fromUpperBound,
788  mdd_t           * toCareSet)
789{
790  array_t       *toCareSetArray;
791  mdd_t         *preImage;
792
793  toCareSetArray = array_alloc(mdd_t *, 0);
794  array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
795  preImage = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
796                        fromLowerBound, fromUpperBound, toCareSetArray);
797  array_free(toCareSetArray);
798  return(preImage);
799}
800
801
802/**Function********************************************************************
803
804  Synopsis    [Computes the backward image of a set.]
805
806  Description [Computes the backward image of a set, under the function vector
807  in imageInfo, using the image computation method specified in imageInfo.  The
808  set for which the backward image is computed is some set containing
809  fromLowerBound and contained in fromUpperBound.  The exact set used is chosen
810  to simplify the computation.  ToCareSet specifies those backward image points
811  of interest; any points not in this set may or may not belong to the returned
812  set.  The MDDs fromLowerBound and fromUpperBound are defined over the range
813  variables.  The MDD toCareSet and the returned MDD are defined over the
814  domain variables. If fromLowerBound is zero, then zero will be returned.]
815
816  SideEffects []
817
818  SeeAlso     [Img_ImageInfoInitialize Img_ImageInfoComputeFwd
819  Img_ImageInfoFree Img_ImageInfoComputeBwdWithDomainVars]
820
821******************************************************************************/
822mdd_t *
823Img_ImageInfoComputeBwd(Img_ImageInfo_t * imageInfo,
824                        mdd_t * fromLowerBound,
825                        mdd_t * fromUpperBound,
826                        array_t * toCareSetArray)
827{
828  mdd_t *image;
829  if (mdd_is_tautology(fromLowerBound, 0)){
830    mdd_manager *mddManager =
831        Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
832    return (mdd_zero(mddManager));
833  }
834  image =  ((*imageInfo->imageComputeBwdProc) (&(imageInfo->functionData),
835                                             imageInfo,
836                                             fromLowerBound,
837                                             fromUpperBound,
838                                             toCareSetArray));
839  nPreComps++;
840#ifndef NDEBUG
841  assert(CheckImageValidity(
842    Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork),
843    image,
844    imageInfo->functionData.rangeVars,
845    imageInfo->functionData.quantifyVars));
846#endif
847  return image;
848}
849
850
851/**Function********************************************************************
852
853  Synopsis    [Frees the memory associated with imageInfo.]
854
855  SideEffects []
856
857  SeeAlso     [Img_ImageInfoInitialize Img_ImageInfoComputeFwd
858  Img_ImageInfoComputeBwd]
859
860******************************************************************************/
861void
862Img_ImageInfoFree(Img_ImageInfo_t * imageInfo)
863{
864  (*imageInfo->imageFreeProc) (imageInfo->methodData);
865  if (imageInfo->functionData.domainBddVars)
866    mdd_array_free(imageInfo->functionData.domainBddVars);
867  if (imageInfo->functionData.rangeBddVars)
868    mdd_array_free(imageInfo->functionData.rangeBddVars);
869  if (imageInfo->functionData.quantifyBddVars)
870    mdd_array_free(imageInfo->functionData.quantifyBddVars);
871  if (imageInfo->functionData.permutD2R)
872    FREE(imageInfo->functionData.permutD2R);
873  if (imageInfo->functionData.permutR2D)
874    FREE(imageInfo->functionData.permutR2D);
875  if (imageInfo->savedRelation)
876    mdd_array_free((array_t *) imageInfo->savedRelation);
877  FREE(imageInfo);
878}
879
880/**Function********************************************************************
881
882  Synopsis    [Frees the memory associated with imageInfo.]
883
884  SideEffects []
885
886  SeeAlso     [Img_ImageInfoInitialize Img_ImageInfoComputeFwd
887  Img_ImageInfoComputeBwd]
888
889******************************************************************************/
890void
891Img_ImageInfoFreeFAFW(Img_ImageInfo_t * imageInfo)
892{
893  if (imageInfo->functionData.quantifyVars)
894    mdd_array_free(imageInfo->functionData.quantifyVars);
895  if (imageInfo->functionData.quantifyCube)
896    mdd_free(imageInfo->functionData.quantifyCube);
897}
898
899/**Function********************************************************************
900
901  Synopsis    [Returns a string giving the method type of an imageInfo.]
902
903  Description [Returns a string giving the method type of an imageInfo. It is
904  the user's responsibility to free this string.]
905
906  SideEffects []
907
908  SeeAlso     [Img_ImageInfoInitialize]
909
910******************************************************************************/
911char *
912Img_ImageInfoObtainMethodTypeAsString(Img_ImageInfo_t * imageInfo)
913{
914  char *methodString;
915  Img_MethodType methodType = imageInfo->methodType;
916
917  switch (methodType) {
918    case Img_Monolithic_c:
919      methodString = util_strsav("monolithic");
920      break;
921    case Img_Tfm_c:
922      methodString = util_strsav("tfm");
923      break;
924    case Img_Hybrid_c:
925      methodString = util_strsav("hybrid");
926      break;
927    case Img_Iwls95_c:
928      methodString = util_strsav("iwls95");
929      break;
930    case Img_Mlp_c:
931      methodString = util_strsav("mlp");
932      break;
933    case Img_Linear_c:
934      methodString = util_strsav("linear");
935      break;
936    case Img_Default_c:
937      methodString = util_strsav("default");
938      break;
939    default:
940      fail("IMG Error : Unexpected type when initalizing image method");
941  }
942  return methodString;
943}
944
945
946/**Function********************************************************************
947
948  Synopsis    [Returns the method type of an imageInfo.]
949
950  Description [Returns the method type of an imageInfo.]
951
952  SideEffects []
953
954  SeeAlso     [Img_ImageInfoInitialize]
955
956******************************************************************************/
957Img_MethodType
958Img_ImageInfoObtainMethodType(Img_ImageInfo_t * imageInfo)
959{
960  return(imageInfo->methodType);
961}
962
963/**Function********************************************************************
964
965  Synopsis    [Returns the method type of an imageInfo.]
966
967  Description [Returns the method type of an imageInfo.]
968
969  SideEffects []
970
971  SeeAlso     [Img_ImageInfoInitialize]
972
973******************************************************************************/
974Img_OptimizeType
975Img_ImageInfoObtainOptimizeType(Img_ImageInfo_t * imageInfo)
976{
977  return(imageInfo->linearOptimize);
978}
979
980/**Function********************************************************************
981 
982  Synopsis    [set optimization relation flag .]
983
984  Description [set optimization relation flag .]
985
986  SideEffects []
987
988  SeeAlso     [Img_ImageInfoInitialize]
989
990******************************************************************************/
991void
992Img_ImageInfoSetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo)
993{
994  imageInfo->useOptimizedRelationFlag = 1;
995}
996
997/**Function********************************************************************
998
999  Synopsis    [reset optimization relation flag .]
1000
1001  Description [reset optimization relation flag .]
1002
1003  SideEffects []
1004
1005  SeeAlso     [Img_ImageInfoInitialize]
1006
1007******************************************************************************/
1008void
1009Img_ImageInfoResetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo)
1010{
1011  imageInfo->useOptimizedRelationFlag = 0;
1012}
1013
1014/**Function********************************************************************
1015
1016  Synopsis    [Reset linear compute range flag.]
1017
1018  Description  [Reset linear compute range flag.]
1019
1020  SideEffects []
1021
1022  SeeAlso     [Img_ImageInfoInitialize]
1023
1024******************************************************************************/
1025void
1026Img_ImageInfoResetLinearComputeRange(Img_ImageInfo_t * imageInfo)
1027{
1028  imageInfo->linearComputeRange = 0;
1029}
1030
1031/**Function********************************************************************
1032
1033  Synopsis    [Set linear compute range flag.]
1034
1035  Description [Set linear compute range flag.]
1036
1037  SideEffects []
1038
1039  SeeAlso     [Img_ImageInfoInitialize]
1040
1041******************************************************************************/
1042void
1043Img_ImageInfoSetLinearComputeRange(Img_ImageInfo_t * imageInfo)
1044{
1045  imageInfo->linearComputeRange = 1;
1046}
1047
1048/**Function********************************************************************
1049
1050  Synopsis    [Prints information about the image technique currently used.]
1051
1052  Description [Prints information about the image technique currently used.]
1053
1054  SideEffects [None.]
1055
1056******************************************************************************/
1057void
1058Img_ImageInfoPrintMethodParams(Img_ImageInfo_t *imageInfo, FILE *fp)
1059{
1060  (*imageInfo->imagePrintMethodParamsProc)(imageInfo->methodData, fp);
1061}
1062
1063/**Function********************************************************************
1064
1065  Synopsis    [Resets the flag that transition relation is minimized.]
1066
1067  Description [Resets the flag that transition relation is minimized.]
1068
1069  SideEffects []
1070
1071******************************************************************************/
1072void
1073Img_ResetTrMinimizedFlag(Img_ImageInfo_t *imageInfo,
1074        Img_DirectionType directionType)
1075{
1076  if (directionType == Img_Forward_c || directionType == Img_Both_c)
1077    imageInfo->fwdTrMinimizedFlag = FALSE;
1078  if (directionType == Img_Backward_c || directionType == Img_Both_c)
1079    imageInfo->bwdTrMinimizedFlag = FALSE;
1080}
1081
1082
1083/**Function********************************************************************
1084
1085  Synopsis    [Returns current method of minimizing transition relation.]
1086
1087  Description [Returns current method of minimizing transition relation. Default is restrict.]
1088
1089  SideEffects []
1090
1091******************************************************************************/
1092Img_MinimizeType
1093Img_ReadMinimizeMethod(void)
1094{
1095
1096  int                   value;
1097  char                  *flagValue;
1098  Img_MinimizeType      minimizeMethod = Img_Restrict_c;
1099
1100  flagValue = Cmd_FlagReadByName("image_minimize_method");
1101  if (flagValue != NIL(char)) {
1102    sscanf(flagValue, "%d", &value);
1103    switch (value) {
1104    case 0 :
1105      minimizeMethod = Img_Restrict_c;
1106      break;
1107    case 1 :
1108      minimizeMethod = Img_Constrain_c;
1109      break;
1110    case 2 :
1111      if (bdd_get_package_name() != CUDD) {
1112        fprintf(vis_stderr, "** img error : Compact in image_minimize_method ");
1113        fprintf(vis_stderr, "is currently supported only by CUDD. ***\n");
1114        fprintf(vis_stderr,
1115          "** img error : Reverting to default minimize method : restrict\n");
1116        break;
1117      }
1118      minimizeMethod = Img_Compact_c;
1119      break;
1120    case 3 :
1121      if (bdd_get_package_name() != CUDD) {
1122        fprintf(vis_stderr, "** img error : Squeeze in image_minimize_method ");
1123        fprintf(vis_stderr, "is currently supported only by CUDD. ***\n");
1124        fprintf(vis_stderr,
1125          "** img error : Reverting to default minimize method : restrict\n");
1126        break;
1127      }
1128      minimizeMethod = Img_Squeeze_c;
1129      break;
1130    case 4 :
1131      minimizeMethod = Img_And_c;
1132      break;
1133    default :
1134      fprintf(vis_stderr,
1135      "** img error : invalid value %s for image_minimize_method[0-4]. ***\n",
1136              flagValue);
1137      fprintf(vis_stderr,
1138        "** img error : Reverting to default minimize method : restrict\n");
1139      break;
1140    }
1141  }
1142  return(minimizeMethod);
1143}
1144
1145
1146/**Function********************************************************************
1147
1148  Synopsis [Minimizes transition relation with given constraint if it
1149  hasn't been minimized already.]
1150
1151  Description [Minimizes transition relation with given constraint if it hasn't
1152  been minimized already (does nothing otherwise). The constraint is expressed
1153  as an array of conjuncts of BDDs, The transition relation is minimized with
1154  each one of the conjuncts.
1155
1156  <p>The boolean reorderIwls95Clusters is only relevant to the iwls95 image
1157  method.  It causes the clusters to be ordered again after minimization.
1158 
1159  <p>The conjuncts have to be in terms of present-state variables or inputs.
1160  Next-state variables are not allowed.
1161
1162  <p>For the hybrid and tfm methods, for image, we can only minimize wrt a set
1163  that includes any possible argument.  For preimage, the result is only
1164  correct for as far as it lies within the set that the TR is minimized with.
1165  That means that reachability info can be usefully applied here.
1166
1167  <p>For the other methods, we can also minimize wrt different sets.  The
1168  edges in the TR that are outgoing from states not in this set may then get
1169  removed.]
1170
1171  SideEffects []
1172
1173******************************************************************************/
1174void
1175Img_MinimizeTransitionRelation(
1176  Img_ImageInfo_t *imageInfo,
1177  array_t *constrainArray,
1178  Img_MinimizeType minimizeMethod,
1179  Img_DirectionType directionType,
1180  boolean reorderIwls95Clusters)
1181{
1182  if (minimizeMethod == Img_DefaultMinimizeMethod_c)
1183   minimizeMethod = Img_ReadMinimizeMethod();
1184
1185  switch (imageInfo->methodType) {
1186    case Img_Monolithic_c:
1187      if (imageInfo->fwdTrMinimizedFlag)
1188        break;
1189      ImgMinimizeTransitionRelationMono(imageInfo, constrainArray,
1190        minimizeMethod, imageInfo->printMinimizeStatus);
1191      imageInfo->fwdTrMinimizedFlag = TRUE;
1192      break;
1193    case Img_Tfm_c:
1194    case Img_Hybrid_c:
1195      if (imageInfo->fwdTrMinimizedFlag)
1196        break;
1197      ImgMinimizeTransitionFunction(imageInfo->methodData, constrainArray,
1198                        minimizeMethod, directionType,
1199                        imageInfo->printMinimizeStatus);
1200      if (directionType == Img_Forward_c || directionType == Img_Both_c)
1201        imageInfo->fwdTrMinimizedFlag = TRUE;
1202      if (directionType == Img_Backward_c || directionType == Img_Both_c)
1203        imageInfo->bwdTrMinimizedFlag = TRUE;
1204      break;
1205    case Img_Iwls95_c:
1206    case Img_Mlp_c:
1207    case Img_Linear_c:
1208      if (directionType == Img_Forward_c || directionType == Img_Both_c) {
1209        if (imageInfo->fwdTrMinimizedFlag == FALSE) {
1210          ImgMinimizeTransitionRelationIwls95(imageInfo->methodData,
1211                                              &(imageInfo->functionData),
1212                                              constrainArray, minimizeMethod,
1213                                              Img_Forward_c,
1214                                              reorderIwls95Clusters,
1215                                              imageInfo->printMinimizeStatus);
1216          imageInfo->fwdTrMinimizedFlag = TRUE;
1217        }
1218      }
1219      if (directionType == Img_Backward_c || directionType == Img_Both_c) {
1220        if (imageInfo->bwdTrMinimizedFlag == FALSE) {
1221          ImgMinimizeTransitionRelationIwls95(imageInfo->methodData,
1222                                              &(imageInfo->functionData),
1223                                              constrainArray, minimizeMethod,
1224                                              Img_Backward_c, 
1225                                              reorderIwls95Clusters,
1226                                              imageInfo->printMinimizeStatus);
1227          imageInfo->bwdTrMinimizedFlag = TRUE;
1228        }
1229      }
1230      break;
1231    default:
1232      fail("** img error: Unexpected type when minimizing transition relation");
1233  }
1234}
1235
1236
1237
1238/**Function********************************************************************
1239
1240  Synopsis    [Minimizes an image with given constraint.]
1241
1242  Description [Minimizes an image with given constraint. This function
1243  can be used to minimize any BDDs.
1244 
1245  <p>If underapprox is 1, the the bdds are underapproximated.  If it is 0, they
1246  are overapproximated, and the minimizeMethod has to be either ornot or
1247  squeeze.
1248  ]
1249
1250  SideEffects []
1251
1252******************************************************************************/
1253mdd_t *
1254Img_MinimizeImage(
1255  mdd_t *image,
1256  mdd_t *constraint,
1257  Img_MinimizeType method,
1258  boolean underapprox)
1259{
1260  mdd_t *newImage;
1261  mdd_t *l, *u;
1262
1263  if (method == Img_DefaultMinimizeMethod_c)
1264    method = Img_ReadMinimizeMethod();
1265
1266  if(underapprox){
1267    switch (method) {
1268    case Img_Restrict_c :
1269      newImage = bdd_minimize(image, constraint);
1270      break;
1271    case Img_Constrain_c :
1272      newImage = bdd_cofactor(image, constraint);
1273      break;
1274    case Img_Compact_c :
1275      newImage = bdd_compact(image, constraint);
1276      break;
1277    case Img_Squeeze_c :
1278      l = bdd_and(image, constraint, 1, 1);
1279      u = bdd_or(image, constraint, 1, 0);
1280      newImage = bdd_squeeze(l, u);
1281      if (bdd_size(newImage) >= bdd_size(image)) {
1282        bdd_free(newImage);
1283        newImage = bdd_dup(image);
1284      }
1285      mdd_free(l);
1286      mdd_free(u);
1287      break;
1288    case Img_And_c :
1289      newImage = bdd_and(image, constraint, 1, 1);
1290      break;
1291    default :
1292      fail("** img error : Unexpected type when minimizing an image");
1293    }
1294  }else{ /* if underapprox */
1295    switch (method) {
1296    case Img_Squeeze_c :
1297      l = image;
1298      u = bdd_or(image, constraint, 1, 0);
1299      newImage = bdd_squeeze(l, u);
1300      if (bdd_size(newImage) >= bdd_size(image)) {
1301        bdd_free(newImage);
1302        newImage = bdd_dup(image);
1303      }
1304      mdd_free(u);
1305      break;
1306    case Img_OrNot_c :
1307      newImage = bdd_or(image, constraint, 1, 0);
1308      break;
1309    default :
1310      fail("** img error: Unexpected type when adding dont-cares to an image");
1311    }
1312  }/* if underapprox */
1313   
1314  return(newImage);
1315}
1316
1317/**Function********************************************************************
1318
1319  Synopsis    [Adds a dont care set to the given image.]
1320
1321  Description [Adds a dont care set to the given image.]
1322
1323  SideEffects []
1324
1325******************************************************************************/
1326mdd_t *
1327Img_AddDontCareToImage(
1328  mdd_t *image,
1329  mdd_t *constraint,
1330  Img_MinimizeType method)
1331{
1332  return(Img_MinimizeImage(image, constraint, Img_Restrict_c, method));
1333}
1334
1335
1336
1337/**Function********************************************************************
1338
1339  Synopsis [Minimizes a single bdd with a set of constraint.]
1340
1341  Description [Minimizes a bdd with given set of constraints.
1342  Underapproximates if underapprox is true, otherwise overapproximated (in
1343  which case method has to be ornot or squeeze).]
1344
1345  SideEffects [Img_MinimizeImage]
1346
1347******************************************************************************/
1348mdd_t *
1349Img_MinimizeImageArray(
1350  mdd_t *image,
1351  array_t *constraintArray,
1352  Img_MinimizeType method,
1353  boolean underapprox)
1354{
1355  int   i;
1356  mdd_t *newImage, *tmpImage;
1357  mdd_t *constraint;
1358
1359  if (method == Img_DefaultMinimizeMethod_c)
1360    method = Img_ReadMinimizeMethod();
1361
1362  newImage = mdd_dup(image);
1363  arrayForEachItem(mdd_t *, constraintArray, i, constraint) {
1364    tmpImage = newImage;
1365    newImage = Img_MinimizeImage(tmpImage, constraint, method, underapprox);
1366    mdd_free(tmpImage);
1367  }
1368  return(newImage);
1369}
1370
1371/**Function********************************************************************
1372
1373  Synopsis    [Sets the flag whether to print the status of minimizing
1374  transition relation.]
1375
1376  Description [Sets the flag whether to print the status of minimizing
1377  transition relation.]
1378
1379  SideEffects []
1380
1381******************************************************************************/
1382void
1383Img_SetPrintMinimizeStatus(Img_ImageInfo_t *imageInfo, int status)
1384{
1385    if (status < 0 || status > 2)
1386        (void)fprintf(vis_stderr,
1387                "** img error: invalid value[%d] for status.\n", status);
1388    else
1389        imageInfo->printMinimizeStatus = status;
1390}
1391
1392/**Function********************************************************************
1393
1394  Synopsis    [Reads the flag whether to print the status of minimizing
1395  transition relation.]
1396
1397  Description [Reads the flag whether to print the status of minimizing
1398  transition relation.]
1399
1400  SideEffects []
1401
1402******************************************************************************/
1403int
1404Img_ReadPrintMinimizeStatus(Img_ImageInfo_t *imageInfo)
1405{
1406    return(imageInfo->printMinimizeStatus);
1407}
1408
1409/**Function********************************************************************
1410
1411  Synopsis    [Abstracts out given variables from transition relation.]
1412
1413  Description [Abstracts out given variables from transition relation.
1414  abstractVars should be an array of bdd variables.]
1415
1416  SideEffects []
1417
1418******************************************************************************/
1419void
1420Img_AbstractTransitionRelation(Img_ImageInfo_t *imageInfo,
1421        array_t *abstractVars, mdd_t *abstractCube,
1422        Img_DirectionType directionType)
1423{
1424  switch (imageInfo->methodType) {
1425    case Img_Monolithic_c:
1426      ImgAbstractTransitionRelationMono(imageInfo, abstractVars,
1427                                abstractCube, imageInfo->printMinimizeStatus);
1428      break;
1429    case Img_Tfm_c:
1430    case Img_Hybrid_c:
1431      ImgAbstractTransitionFunction(imageInfo, abstractVars,
1432                                abstractCube, directionType,
1433                                imageInfo->printMinimizeStatus);
1434      break;
1435    case Img_Iwls95_c:
1436    case Img_Mlp_c:
1437    case Img_Linear_c:
1438      ImgAbstractTransitionRelationIwls95(imageInfo, abstractVars,
1439                                abstractCube, directionType,
1440                                imageInfo->printMinimizeStatus);
1441      break;
1442    default:
1443      fail("** img error : Unexpected type when abstracting transition relation");
1444  }
1445}
1446
1447/**Function********************************************************************
1448
1449  Synopsis    [Duplicates the transition relation for backup.]
1450
1451  Description [Duplicates the transition relation for backup. Copies transition
1452  relation as well as quantification schedule for temporary use.]
1453
1454  SideEffects []
1455
1456******************************************************************************/
1457void
1458Img_DupTransitionRelation(Img_ImageInfo_t *imageInfo,
1459        Img_DirectionType directionType)
1460{
1461  switch (imageInfo->methodType) {
1462    case Img_Monolithic_c:
1463      ImgDuplicateTransitionRelationMono(imageInfo);
1464      break;
1465    case Img_Tfm_c:
1466    case Img_Hybrid_c:
1467      ImgDuplicateTransitionFunction(imageInfo, directionType);
1468      break;
1469    case Img_Iwls95_c:
1470    case Img_Mlp_c:
1471    case Img_Linear_c:
1472      ImgDuplicateTransitionRelationIwls95(imageInfo, directionType);
1473      break;
1474    default:
1475      fail("** img error: Unexpected type when duplicating transition relation");
1476  }
1477}
1478
1479/**Function********************************************************************
1480
1481  Synopsis    [Restores original transition relation from saved.]
1482
1483  Description [Restores original transition relation from saved.]
1484
1485  SideEffects []
1486
1487******************************************************************************/
1488void
1489Img_RestoreTransitionRelation(Img_ImageInfo_t *imageInfo,
1490        Img_DirectionType directionType)
1491{
1492
1493  switch (imageInfo->methodType) {
1494    case Img_Monolithic_c:
1495      ImgRestoreTransitionRelationMono(imageInfo, directionType);
1496      break;
1497    case Img_Tfm_c:
1498    case Img_Hybrid_c:
1499      ImgRestoreTransitionFunction(imageInfo, directionType);
1500      break;
1501    case Img_Iwls95_c:
1502    case Img_Mlp_c:
1503    case Img_Linear_c:
1504      ImgRestoreTransitionRelationIwls95(imageInfo, directionType);
1505      break;
1506    default:
1507      fail("** img error : Unexpected type when backup transition relation");
1508  }
1509}
1510
1511
1512/**Function********************************************************************
1513
1514  Synopsis [Approximate transition relation.]
1515
1516  Description [Approximate transition relation.]
1517
1518  SideEffects []
1519
1520******************************************************************************/
1521int
1522Img_ApproximateTransitionRelation(Img_ImageInfo_t *imageInfo,
1523                                  bdd_approx_dir_t approxDir,
1524                                  bdd_approx_type_t approxMethod,
1525                                  int approxThreshold,
1526                                  double approxQuality,
1527                                  double approxQualityBias,
1528                                  Img_DirectionType directionType,
1529                                  mdd_t *bias)
1530{
1531  int unchanged = 0;
1532  mdd_manager *mgr =
1533    Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork);
1534
1535  switch (imageInfo->methodType) {
1536    case Img_Monolithic_c:
1537      unchanged = ImgApproximateTransitionRelationMono(mgr, imageInfo,
1538                                                approxDir, approxMethod,
1539                                                approxThreshold,
1540                                                approxQuality,
1541                                                approxQualityBias, bias);
1542      break;
1543    case Img_Tfm_c:
1544    case Img_Hybrid_c:
1545      unchanged = ImgApproximateTransitionFunction(mgr,
1546                                                imageInfo->methodData,
1547                                                approxDir, approxMethod,
1548                                                approxThreshold,
1549                                                approxQuality,
1550                                                approxQualityBias,
1551                                                directionType, bias);
1552      break;
1553    case Img_Iwls95_c:
1554    case Img_Mlp_c:
1555    case Img_Linear_c:
1556      if (directionType == Img_Forward_c || directionType == Img_Both_c) {
1557        unchanged = ImgApproximateTransitionRelationIwls95(mgr,
1558                                                imageInfo->methodData,
1559                                                approxDir, approxMethod,
1560                                                approxThreshold,
1561                                                approxQuality,
1562                                                approxQualityBias,
1563                                                Img_Forward_c, bias);
1564      }
1565      if (directionType == Img_Backward_c || directionType == Img_Both_c) {
1566        unchanged += ImgApproximateTransitionRelationIwls95(mgr,
1567                                                imageInfo->methodData,
1568                                                approxDir, approxMethod,
1569                                                approxThreshold,
1570                                                approxQuality,
1571                                                approxQualityBias,
1572                                                Img_Backward_c, bias);
1573      }
1574      break;
1575    default:
1576      fail(
1577       "** img error : Unexpected type when approximating transition relation");
1578  }
1579  return(unchanged);
1580}
1581
1582
1583/**Function********************************************************************
1584
1585  Synopsis [Approximate image.]
1586
1587  Description [Approximate image.]
1588
1589  SideEffects []
1590
1591******************************************************************************/
1592mdd_t *
1593Img_ApproximateImage(mdd_manager *mgr,
1594                     mdd_t *image,
1595                     bdd_approx_dir_t approxDir,
1596                     bdd_approx_type_t approxMethod,
1597                     int approxThreshold,
1598                     double approxQuality,
1599                     double approxQualityBias,
1600                     mdd_t *bias)
1601{
1602  double quality;
1603  double qualityBias;
1604  int nvars = mdd_get_number_of_bdd_support(mgr, image);
1605  mdd_t *approxImage;
1606
1607  if (approxQuality != 0.0)
1608    quality = approxQuality;
1609  else
1610    quality = 1.0; /* default */
1611
1612  /* based on approximation method specified, compute subset or superset */
1613  switch (approxMethod) {
1614  case BDD_APPROX_HB:
1615    approxImage = bdd_approx_hb(image, approxDir, nvars, approxThreshold);
1616    break;
1617  case BDD_APPROX_SP:
1618    approxImage = bdd_approx_sp(image, approxDir, nvars, approxThreshold, 0);
1619    break;
1620  case BDD_APPROX_UA:
1621    approxImage = bdd_approx_ua(image, approxDir, nvars, approxThreshold, 0,
1622                                quality);
1623    break;
1624  case BDD_APPROX_RUA:
1625    approxImage = bdd_approx_remap_ua(image, approxDir, nvars, approxThreshold,
1626                                      quality);
1627    break;
1628  case BDD_APPROX_BIASED_RUA:
1629    if (approxQualityBias != 0.0)
1630      qualityBias = approxQualityBias;
1631    else
1632      qualityBias = 0.5; /* default */
1633    approxImage = bdd_approx_biased_rua(image, approxDir, bias, nvars,
1634                                        approxThreshold, quality, qualityBias);
1635    break;
1636  case BDD_APPROX_COMP:
1637    approxImage = bdd_approx_compress(image, approxDir, nvars, approxThreshold);
1638    break;
1639  default:
1640    assert(0);
1641    approxImage = NIL(mdd_t);
1642    break;
1643  }
1644
1645  return(approxImage);
1646}
1647
1648
1649/**Function********************************************************************
1650
1651  Synopsis [Returns 1 if partitioned transition relation is used.]
1652
1653  Description [Returns 1 if partitioned transition relation is used.]
1654
1655  SideEffects []
1656
1657******************************************************************************/
1658int
1659Img_IsPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo)
1660{
1661  if (imageInfo->methodType == Img_Iwls95_c ||
1662      imageInfo->methodType == Img_Mlp_c ||
1663      imageInfo->methodType == Img_Linear_c)
1664    return(1);
1665  else if (imageInfo->methodType == Img_Hybrid_c)
1666    return(ImgIsPartitionedTransitionRelationTfm(imageInfo));
1667  else
1668    return(0);
1669}
1670
1671
1672/**Function********************************************************************
1673
1674  Synopsis [Resets number of image/preimage computation.]
1675
1676  Description [Resets number of image/preimage computation.]
1677
1678  SideEffects []
1679
1680******************************************************************************/
1681void
1682Img_ResetNumberOfImageComputation(Img_DirectionType imgDir)
1683{
1684  if (imgDir == Img_Forward_c || imgDir == Img_Both_c)
1685    nImgComps = 0;
1686  if (imgDir == Img_Backward_c || imgDir == Img_Both_c)
1687    nPreComps = 0;
1688}
1689
1690
1691/**Function********************************************************************
1692
1693  Synopsis [Returns number of image/preimage computation.]
1694
1695  Description [Returns number of image/preimage computation.]
1696
1697  SideEffects []
1698
1699******************************************************************************/
1700int
1701Img_GetNumberOfImageComputation(Img_DirectionType imgDir)
1702{
1703  if (imgDir == Img_Forward_c)
1704    return(nImgComps);
1705  else if (imgDir == Img_Backward_c)
1706    return(nPreComps);
1707  else
1708    return(nImgComps + nPreComps);
1709}
1710
1711
1712/**Function********************************************************************
1713
1714  Synopsis    [Returns current partitioned transition relation.]
1715
1716  Description [Returns current partitioned transition relation.]
1717
1718  SideEffects []
1719
1720******************************************************************************/
1721array_t *
1722Img_GetPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo,
1723                                     Img_DirectionType directionType)
1724{
1725  array_t       *relationArray;
1726
1727  switch (imageInfo->methodType) {
1728    case Img_Monolithic_c:
1729      relationArray = (array_t *)imageInfo->methodData;
1730      break;
1731    case Img_Tfm_c:
1732    case Img_Hybrid_c:
1733      relationArray = ImgGetTransitionFunction(imageInfo->methodData,
1734                                                directionType);
1735      break;
1736    case Img_Iwls95_c:
1737    case Img_Mlp_c:
1738    case Img_Linear_c:
1739      relationArray = ImgGetTransitionRelationIwls95(imageInfo->methodData,
1740                                                        directionType);
1741      break;
1742    default:
1743      fail("** img error: Unexpected image method type.\n");
1744  }
1745
1746  return(relationArray);
1747}
1748
1749
1750/**Function********************************************************************
1751
1752  Synopsis    [Replace ith partitioned transition relation.]
1753
1754  Description [Replace ith partitioned transition relation.]
1755
1756  SideEffects []
1757
1758******************************************************************************/
1759void
1760Img_ReplaceIthPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo,
1761        int i, mdd_t *relation, Img_DirectionType directionType)
1762{
1763  switch (imageInfo->methodType) {
1764    case Img_Monolithic_c:
1765      break;
1766    case Img_Tfm_c:
1767    case Img_Hybrid_c:
1768      ImgReplaceIthTransitionFunction(imageInfo->methodData, i, relation,
1769                                        directionType);
1770      break;
1771    case Img_Iwls95_c:
1772    case Img_Mlp_c:
1773    case Img_Linear_c:
1774      ImgReplaceIthPartitionedTransitionRelationIwls95(imageInfo->methodData,
1775                                        i, relation, directionType);
1776      break;
1777    default:
1778      fail("** img error: Unexpected image method type.\n");
1779  }
1780}
1781
1782
1783/**Function********************************************************************
1784
1785  Synopsis    [Replace partitioned transition relation.]
1786
1787  Description [Replace partitioned transition relation.]
1788
1789  SideEffects []
1790
1791******************************************************************************/
1792void
1793Img_ReplacePartitionedTransitionRelation(Img_ImageInfo_t *imageInfo,
1794        array_t *relationArray, Img_DirectionType directionType)
1795{
1796  switch (imageInfo->methodType) {
1797    case Img_Monolithic_c:
1798      break;
1799    case Img_Tfm_c:
1800    case Img_Hybrid_c:
1801      ImgUpdateTransitionFunction(imageInfo->methodData, relationArray,
1802                                  directionType);
1803      break;
1804    case Img_Iwls95_c:
1805    case Img_Mlp_c:
1806    case Img_Linear_c:
1807      ImgUpdateTransitionRelationIwls95(imageInfo->methodData,
1808                                        relationArray, directionType);
1809      break;
1810    default:
1811      fail("** img error: Unexpected image method type.\n");
1812  }
1813}
1814
1815
1816/**Function********************************************************************
1817
1818  Synopsis    [Replace partitioned transition relation.]
1819
1820  Description [Replace partitioned transition relation.]
1821
1822  SideEffects []
1823
1824******************************************************************************/
1825mdd_t *
1826Img_ComposeIntermediateNodes(graph_t *partition, mdd_t *node,
1827                array_t *psVars, array_t *nsVars, array_t *inputVars)
1828{
1829  mdd_manager           *mgr = Part_PartitionReadMddManager(partition);
1830  array_t               *supportList;
1831  st_table              *supportTable = st_init_table(st_numcmp, st_numhash);
1832  int                   i, j;
1833  int                   existIntermediateVars;
1834  int                   mddId;
1835  vertex_t              *vertex;
1836  array_t               *varBddFunctionArray, *varArray;
1837  mdd_t                 *var, *func, *tmpMdd;
1838  mdd_t                 *composedNode;
1839  Mvf_Function_t        *mvf;
1840
1841  if (psVars) {
1842    for (i = 0; i < array_n(psVars); i++) {
1843      mddId = array_fetch(int, psVars, i);
1844      st_insert(supportTable, (char *)(long)mddId, NULL);
1845    }
1846  }
1847  if (nsVars) {
1848    for (i = 0; i < array_n(nsVars); i++) {
1849      mddId = array_fetch(int, nsVars, i);
1850      st_insert(supportTable, (char *)(long)mddId, NULL);
1851    }
1852  }
1853  if (inputVars) {
1854    for (i = 0; i < array_n(inputVars); i++) {
1855      mddId = array_fetch(int, inputVars, i);
1856      st_insert(supportTable, (char *)(long)mddId, NULL);
1857    }
1858  }
1859
1860  composedNode = mdd_dup(node);
1861
1862  existIntermediateVars = 1;
1863  while (existIntermediateVars) {
1864    existIntermediateVars = 0;
1865    supportList = mdd_get_support(mgr, composedNode);
1866    for (i = 0; i < array_n(supportList); i++) {
1867      mddId = array_fetch(int, supportList, i);
1868      if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
1869        vertex = Part_PartitionFindVertexByMddId(partition, mddId);
1870        mvf = Part_VertexReadFunction(vertex);
1871        varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mgr, mddId, mvf);
1872        varArray = mdd_id_to_bdd_array(mgr, mddId);
1873        assert(array_n(varBddFunctionArray) == array_n(varArray));
1874        for (j = 0; j < array_n(varBddFunctionArray); j++) {
1875          var = array_fetch(mdd_t *, varArray, j);
1876          func = array_fetch(mdd_t *, varBddFunctionArray, j);
1877          tmpMdd = composedNode;
1878          composedNode = bdd_compose(composedNode, var, func);
1879          mdd_free(tmpMdd);
1880          mdd_free(var);
1881          mdd_free(func);
1882        }
1883        array_free(varBddFunctionArray);
1884        array_free(varArray);
1885        existIntermediateVars = 1;
1886      }
1887    }
1888    array_free(supportList);
1889  }
1890  st_free_table(supportTable);
1891  return(composedNode);
1892}
1893
1894
1895/**Function********************************************************************
1896
1897  Synopsis [Constrains/adds dont-cares to the bit relations with the
1898  given constraint and creates a new transtion relation.]
1899
1900  Description [Constrains/adds dont-cares to the bit relations with
1901  the given constraint and creates a new transition relation in the
1902  direction indicated. This procedure will incur the cost of creating
1903  the bit relations if they dont already exist. An over/under
1904  approximation of the transition relation may be created according to
1905  the underApprox flag. The flag is TRUE for underapproximations and
1906  FALSE for over approximation. An underapproximation of the
1907  transition relation will be in the interval [T.C, T] and an
1908  overapproximation of the transition relation will be in the interval
1909  [T, T+ C']. THe method used in minimization is set in
1910  Img_GuidedSearchReadUnderApproxMinimizeMethod and
1911  Img_GuidedSearchReadOverApproxMinimizeMethod. The cleanup flag
1912  cleans up the data (e.g., bit relations) stored for applying
1913  constraints repeatedly. ]
1914 
1915  SideEffects [Current transition relation and quantification schedule
1916  are freed. Bit relations are freed if indicated by the cleanUp flag.]
1917
1918  SeeAlso [Img_GuidedSearchReadUnderApproxMinimizeMethod
1919  Img_GuidedSearchReadOverApproxMinimizeMethod]
1920
1921******************************************************************************/
1922void
1923Img_ImageConstrainAndClusterTransitionRelation(Img_ImageInfo_t *imageInfo,
1924                                               Img_DirectionType direction,
1925                                               mdd_t *constrain,
1926                                               Img_MinimizeType minimizeMethod,
1927                                               boolean underApprox,
1928                                               boolean cleanUp,
1929                                               boolean forceReorder,
1930                                               int printStatus)
1931{
1932    switch (imageInfo->methodType) {
1933    case Img_Monolithic_c:
1934      ImgImageConstrainAndClusterTransitionRelationMono(imageInfo,
1935                                                        constrain,
1936                                                        minimizeMethod,
1937                                                        underApprox,
1938                                                        cleanUp,
1939                                                        forceReorder,
1940                                                        printStatus);
1941      break;
1942    case Img_Tfm_c:
1943    case Img_Hybrid_c:
1944      ImgImageConstrainAndClusterTransitionRelationTfm(imageInfo,
1945                                                       direction,
1946                                                       constrain,
1947                                                       minimizeMethod,
1948                                                       underApprox,
1949                                                       cleanUp,
1950                                                       forceReorder,
1951                                                       printStatus);
1952      break;
1953    case Img_Iwls95_c:
1954    case Img_Mlp_c:
1955    case Img_Linear_c:
1956      ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(imageInfo,
1957                                                               direction,
1958                                                               constrain,
1959                                                               minimizeMethod,
1960                                                               underApprox,
1961                                                               cleanUp,
1962                                                               forceReorder,
1963                                                               printStatus);
1964      break;
1965    default:
1966      fail("** img error: Unexpected image method type.\n");
1967  }
1968}
1969
1970/**Function********************************************************************
1971
1972  Synopsis [Returns the guided search minimize method of underapproximating the
1973  transition relation.]
1974
1975  Description [Returns the guided search minimize method of underapproximating the
1976  transition relation. Default is And.]
1977
1978  SideEffects []
1979
1980******************************************************************************/
1981Img_MinimizeType
1982Img_GuidedSearchReadUnderApproxMinimizeMethod(void)
1983{
1984  char                  *flagValue;
1985  Img_MinimizeType      minimizeMethod = Img_And_c;
1986
1987  flagValue = Cmd_FlagReadByName("guided_search_underapprox_minimize_method");
1988  if (flagValue != NIL(char)) {
1989    if (strcmp(flagValue, "constrain") == 0) {
1990      minimizeMethod = Img_Constrain_c;
1991    } else if (strcmp(flagValue, "and") == 0) {
1992      minimizeMethod = Img_And_c;
1993    } else {
1994      fprintf(vis_stderr,
1995      "** img error : invalid value %s for guided_search_underapprox_minimize_method. ***\n",
1996              flagValue);
1997      fprintf(vis_stderr,
1998        "** img error : Reverting to default minimize method : And\n");
1999    }
2000  }
2001  return(minimizeMethod);
2002}
2003
2004/**Function********************************************************************
2005
2006  Synopsis [Returns the guided search minimize method of overapproximating the
2007  transition relation.]
2008
2009  Description [Returns the guided search minimize method of overapproximating the
2010  transition relation. Default is OrNot.]
2011
2012  SideEffects []
2013
2014******************************************************************************/
2015Img_MinimizeType
2016Img_GuidedSearchReadOverApproxMinimizeMethod(void)
2017{
2018  char                  *flagValue;
2019  Img_MinimizeType      minimizeMethod = Img_OrNot_c;
2020
2021  flagValue = Cmd_FlagReadByName("guided_search_overapprox_minimize_method");
2022  if (flagValue != NIL(char)) {
2023    if (strcmp(flagValue, "ornot") == 0) {
2024      minimizeMethod = Img_OrNot_c;
2025    } else if (strcmp(flagValue, "squeeze") == 0) {
2026      minimizeMethod = Img_Squeeze_c;
2027    } else {
2028      fprintf(vis_stderr,
2029      "** img error : invalid value %s for guided_search_overapprox_minimize_method. ***\n",
2030              flagValue);
2031      fprintf(vis_stderr,
2032        "** img error : Reverting to default method : OrNot\n");
2033    }
2034  }
2035  return(minimizeMethod);
2036}
2037
2038
2039/**Function********************************************************************
2040
2041  Synopsis    [Substitutes variables between domain and range.]
2042
2043  Description [Substitutes variables between domain and range.]
2044
2045  SideEffects []
2046
2047******************************************************************************/
2048mdd_t *
2049Img_Substitute(Img_ImageInfo_t *imageInfo, mdd_t *f, Img_SubstituteDir dir)
2050{
2051  mdd_t *new_;
2052
2053  new_ = ImgSubstitute(f, &(imageInfo->functionData), dir);
2054  return(new_);
2055}
2056
2057
2058/*---------------------------------------------------------------------------*/
2059/* Definition of internal functions                                          */
2060/*---------------------------------------------------------------------------*/
2061
2062/**Function********************************************************************
2063
2064  Synopsis    [Minimize array of bdds wrt a set of constraints]
2065
2066  Description [Compute a new array, such that every element corresponds to an
2067  element of imageArray minimized with all elements of careSetArray
2068  successively, using minimizeMethod.  This function can be used for any array
2069  of bdds.
2070
2071  <p>If underapprox is 1, the the bdds are underapproximated.  If it is 0, they
2072  are overapproximated, and the minimizeMethod has to be either ornot or
2073  squeeze.]
2074
2075  SideEffects []
2076
2077  SeeAlso[Img_MinimizeImage ImgMinimizeImageArrayWithCareSetArrayInSitu]
2078
2079******************************************************************************/
2080array_t *
2081ImgMinimizeImageArrayWithCareSetArray(
2082  array_t *imageArray,
2083  array_t *careSetArray,
2084  Img_MinimizeType minimizeMethod,
2085  boolean underapprox,
2086  boolean printInfo,
2087  Img_DirectionType dir
2088  )
2089{
2090  array_t *result; /* of mdd_t * */
2091
2092  result = mdd_array_duplicate(imageArray);
2093  ImgMinimizeImageArrayWithCareSetArrayInSitu(result, careSetArray,
2094                                              minimizeMethod, underapprox,
2095                                              printInfo, dir); 
2096  return result;
2097}
2098
2099/**Function********************************************************************
2100
2101  Synopsis    [Minimize array of bdds wrt a set of constraints]
2102
2103  Description [Compute a new array, such that every element corresponds to an
2104  element of imageArray minimized with all elements of careSetArray
2105  successively, using minimizeMethod.  This function can be used for any array
2106  of bdds.
2107
2108  <p>If underapprox is 1, the the bdds are underapproximated.  If it is 0, they
2109  are overapproximated, and the minimizeMethod has to be either ornot or
2110  squeeze.
2111 
2112  <p>In-situ variant of ImgMinimizeImageArrayWithCareSetArray.  Probably saves
2113  space. ]
2114
2115  SideEffects []
2116
2117  SeeAlso[Img_MinimizeImage,ImgMinimizeImageArrayWithCareSetArray]
2118
2119******************************************************************************/
2120void
2121ImgMinimizeImageArrayWithCareSetArrayInSitu(
2122  array_t *imageArray,
2123  array_t *careSetArray,
2124  Img_MinimizeType minimizeMethod,
2125  boolean underapprox,
2126  boolean printInfo,
2127  Img_DirectionType dir)
2128{
2129  int i;
2130  mdd_t *cluster = NIL(mdd_t);
2131  long constrainSize, initialTotalSize;
2132  char *dirname = NIL(char);
2133 
2134  if (minimizeMethod == Img_DefaultMinimizeMethod_c)
2135    minimizeMethod = Img_ReadMinimizeMethod();   
2136 
2137  if(printInfo){
2138    constrainSize    = mdd_size_multiple(careSetArray);
2139    initialTotalSize =  mdd_size_multiple(imageArray);
2140    assert(dir != Img_Both_c);
2141    if(dir == Img_Forward_c)
2142      dirname = "fwd";
2143    else
2144      dirname = "bwd";
2145  } else { /* to remove uninitialized variable warnings */
2146    constrainSize = 0;
2147    initialTotalSize = 0;
2148  }
2149 
2150  arrayForEachItem(mdd_t *, imageArray, i, cluster){
2151    mdd_t *minimized;
2152   
2153    minimized = Img_MinimizeImageArray(cluster, careSetArray,
2154                                       minimizeMethod, underapprox);
2155    array_insert(mdd_t *, imageArray, i, minimized);
2156   
2157    if(printInfo)
2158      (void) fprintf(vis_stdout,
2159          "IMG Info: minimized %s relation %d | %ld => %d in component %d.\n",
2160                     dirname, mdd_size(cluster), constrainSize,
2161                     mdd_size(minimized), i); 
2162     mdd_free(cluster);
2163 }
2164 
2165  if(printInfo)
2166    (void) fprintf(vis_stdout,
2167      "IMG Info: minimized %s relation %ld | %ld => %ld with %d components.\n",
2168                   dirname, initialTotalSize, constrainSize,
2169                   mdd_size_multiple(imageArray), array_n(imageArray)); 
2170 
2171 return;
2172}
2173
2174/**Function********************************************************************
2175
2176  Synopsis    [Substitutes variables between domain and range.]
2177
2178  Description [Substitutes variables between domain and range.]
2179
2180  SideEffects []
2181
2182******************************************************************************/
2183mdd_t *
2184ImgSubstitute(mdd_t *f, ImgFunctionData_t *functionData, Img_SubstituteDir dir)
2185{
2186  mdd_t *new_;
2187
2188  if (bdd_get_package_name() == CUDD) {
2189    if (dir == Img_D2R_c)
2190      new_ = bdd_substitute_with_permut(f, functionData->permutD2R);
2191    else
2192      new_ = bdd_substitute_with_permut(f, functionData->permutR2D);
2193  } else {
2194    if (dir == Img_D2R_c) {
2195      new_ = bdd_substitute(f, functionData->domainBddVars,
2196                            functionData->rangeBddVars);
2197    } else {
2198      new_ = bdd_substitute(f, functionData->rangeBddVars,
2199                            functionData->domainBddVars);
2200    }
2201  }
2202  return(new_);
2203}
2204
2205/**Function********************************************************************
2206
2207  Synopsis    [Substitutes variables between domain and range.]
2208
2209  Description [Substitutes variables between domain and range.]
2210
2211  SideEffects []
2212
2213******************************************************************************/
2214array_t *
2215ImgSubstituteArray(array_t *f_array, ImgFunctionData_t *functionData,
2216                Img_SubstituteDir dir)
2217{
2218  array_t *new_array;
2219
2220  if (bdd_get_package_name() == CUDD) {
2221    if (dir == Img_D2R_c) {
2222      new_array = bdd_substitute_array_with_permut(f_array,
2223                        functionData->permutD2R);
2224    } else {
2225      new_array = bdd_substitute_array_with_permut(f_array,
2226                        functionData->permutR2D);
2227    }
2228  } else {
2229    if (dir == Img_D2R_c) {
2230      new_array = bdd_substitute_array(f_array, functionData->domainBddVars,
2231                functionData->rangeBddVars);
2232    } else {
2233      new_array = bdd_substitute_array(f_array, functionData->rangeBddVars,
2234                functionData->domainBddVars);
2235    }
2236  }
2237  return(new_array);
2238}
2239
2240/**Function********************************************************************
2241
2242  Synopsis    [Prints Partial Image options.]
2243
2244  Description [Prints Partial Image options.]
2245
2246  SideEffects []
2247
2248******************************************************************************/
2249void
2250ImgPrintPartialImageOptions(void)
2251{
2252  ImgPartialImageOption_t *PIoption;
2253  char *dummy;
2254  PIoption = ImgGetPartialImageOptions();
2255
2256  dummy = ALLOC(char, 25);
2257  switch (PIoption->partialImageMethod) {
2258  case Img_PIApprox_c: sprintf(dummy, "%s", "approx");break;
2259  case Img_PIClipping_c: sprintf(dummy, "%s", "clipping");break;
2260  default: sprintf(dummy, "%s", "approx");break;
2261  }
2262  fprintf(vis_stdout, "HD: Partial Image number of variables = %d\n", PIoption->nvars);
2263  fprintf(vis_stdout, "HD: Partial Image Method = %s\n", dummy);
2264  fprintf(vis_stdout, "HD: Partial Image Threshold = %d\n", PIoption->partialImageThreshold);
2265  fprintf(vis_stdout, "HD: Partial Image Size = %d\n", PIoption->partialImageSize);
2266  switch (PIoption->partialImageApproxMethod) {
2267  case BDD_APPROX_HB: sprintf(dummy, "%s", "heavy_branch"); break;
2268  case BDD_APPROX_SP: sprintf(dummy, "%s", "short_paths"); break;
2269
2270  case BDD_APPROX_UA: sprintf(dummy, "%s", "under_approx"); break;
2271  case BDD_APPROX_RUA: sprintf(dummy, "%s", "remap_ua"); break;
2272
2273  case BDD_APPROX_COMP: sprintf(dummy, "%s", "compress"); break;
2274  default: sprintf(dummy, "%s", "remap_ua"); break;
2275  }
2276  fprintf(vis_stdout, "HD: Partial Image Approximation Method = %s\n", dummy);
2277
2278  fprintf(vis_stdout, "HD: Partial Image Approximation quality factor = %g\n", PIoption->quality);
2279  fprintf(vis_stdout, "HD: Partial Image Approximation Bias quality factor = %g\n", PIoption->qualityBias);
2280  fprintf(vis_stdout, "HD: Partial Image Clipping factor = %g\n", PIoption->clippingDepthFrac);
2281
2282  FREE(dummy);
2283  FREE(PIoption);
2284  return;
2285
2286} /* end of ImgPrintPartialImageOptions */
2287
2288/**Function********************************************************************
2289
2290  Synopsis    [Get partial image options.]
2291
2292  Description [Get partial image options.]
2293
2294  SideEffects []
2295
2296******************************************************************************/
2297ImgPartialImageOption_t *
2298ImgGetPartialImageOptions(void)
2299{
2300  ImgPartialImageOption_t *options;
2301  char *qualityString;
2302  char *partialImageThresholdString, *partialImageApproxString, *partialImageSizeString;
2303  char *partialImageMethodString, *clippingDepthString;
2304
2305  options = ALLOC(ImgPartialImageOption_t , 1);
2306  if (options == NIL(ImgPartialImageOption_t)) return NIL(ImgPartialImageOption_t);
2307
2308  /* initialize to default values; */
2309  options->nvars = 0;
2310  options->partialImageMethod = Img_PIApprox_c;
2311  options->partialImageThreshold = 200000;
2312  options->partialImageSize = 100000;
2313  options->partialImageApproxMethod = BDD_APPROX_RUA;
2314  options->quality = 1.0;
2315  options->qualityBias = 0.5;
2316  options->clippingDepthFrac = IMG_PI_CLIP_DEPTH;
2317
2318  /* what kind of approximation to apply to the image */
2319  partialImageMethodString = Cmd_FlagReadByName("hd_partial_image_method");
2320  if (partialImageMethodString != NIL(char)) {
2321    if (strcmp(partialImageMethodString, "approx") == 0) {
2322      options->partialImageMethod = Img_PIApprox_c;
2323    } else if (strcmp(partialImageMethodString, "clipping") == 0) {
2324      options->partialImageMethod = Img_PIClipping_c;
2325    }
2326  }
2327
2328  /* threshold to trigger partial image computation */
2329  partialImageThresholdString = Cmd_FlagReadByName("hd_partial_image_threshold");
2330  if (partialImageThresholdString != NIL(char)) {
2331    options->partialImageThreshold = strtol(partialImageThresholdString, NULL, 10);
2332    if (options->partialImageThreshold < 0) {
2333      options->partialImageThreshold = 200000;
2334    }
2335  }
2336
2337  /* intended size of partial image */
2338  partialImageSizeString = Cmd_FlagReadByName("hd_partial_image_size");
2339  if (partialImageSizeString != NIL(char)) {
2340    options->partialImageSize = strtol(partialImageSizeString, NULL, 10);
2341    if (options->partialImageSize < 0) {
2342      options->partialImageSize = 100000;
2343    }
2344  }
2345
2346  /* which approximation method to apply */
2347  partialImageApproxString = Cmd_FlagReadByName("hd_partial_image_approx");
2348  if (partialImageApproxString != NIL(char)) {
2349    if (strcmp(partialImageApproxString, "heavy_branch") == 0) {
2350      options->partialImageApproxMethod = BDD_APPROX_HB;
2351    } else if (strcmp(partialImageApproxString, "short_paths") == 0) {
2352      options->partialImageApproxMethod = BDD_APPROX_SP;
2353    } else if (strcmp(partialImageApproxString, "under_approx") == 0) {
2354      options->partialImageApproxMethod = BDD_APPROX_UA;
2355    } else if (strcmp(partialImageApproxString, "remap_ua") == 0) {
2356      options->partialImageApproxMethod = BDD_APPROX_RUA;
2357    } else if (strcmp(partialImageApproxString, "compress") == 0) {
2358      options->partialImageApproxMethod = BDD_APPROX_COMP;
2359    } else if (strcmp(partialImageApproxString, "biased_rua") == 0) {
2360      options->partialImageApproxMethod = BDD_APPROX_BIASED_RUA;
2361    }
2362  }
2363  /* quality factor for remap_ua and under_approx methods */
2364  qualityString = Cmd_FlagReadByName("hd_partial_image_approx_quality");
2365  if (qualityString != NIL(char)) {
2366    options->quality = strtod(qualityString, NULL);
2367    if (options->quality < 0.0) {
2368      options->quality = 1.0;
2369    }
2370  }
2371
2372  /* quality factor for remap_ua and under_approx methods */
2373  qualityString = Cmd_FlagReadByName("hd_partial_image_approx_bias_quality");
2374  if (qualityString != NIL(char)) {
2375    options->qualityBias = strtod(qualityString, NULL);
2376    if (options->qualityBias < 0.0) {
2377      options->qualityBias = 0.5;
2378    }
2379  }
2380
2381  /* fraction of depth of Bdd to clip at. */
2382  clippingDepthString = Cmd_FlagReadByName("hd_partial_image_clipping_depth");
2383  if (clippingDepthString != NIL(char)) {
2384    options->clippingDepthFrac = strtod(clippingDepthString, NULL);
2385    if ((options->clippingDepthFrac > 1.0) ||
2386        (options->clippingDepthFrac < 0.0)) {
2387      options->clippingDepthFrac = IMG_PI_CLIP_DEPTH;
2388    }
2389  }
2390
2391  return (options);
2392} /* end of ImgGetPartialImageOptions */
2393
2394/**Function********************************************************************
2395
2396  Synopsis    [This function checks the validity of an array of array
2397  of BDD nodes.]
2398
2399  SideEffects []
2400
2401  SeeAlso     [ImgBddCheckValidity]
2402
2403******************************************************************************/
2404int
2405ImgArrayBddArrayCheckValidity(array_t *arrayBddArray)
2406{
2407  int i;
2408  for(i=0; i<array_n(arrayBddArray); i++) {
2409    ImgBddArrayCheckValidity(array_fetch(array_t*, arrayBddArray, i));
2410  }
2411  return 1;
2412}
2413
2414
2415/**Function********************************************************************
2416
2417  Synopsis    [This function checks the validity of array of BDD nodes.]
2418
2419  SideEffects []
2420
2421  SeeAlso     [ImgBddCheckValidity]
2422
2423******************************************************************************/
2424int
2425ImgBddArrayCheckValidity(array_t *bddArray)
2426{
2427  int i;
2428  for(i=0; i<array_n(bddArray); i++) {
2429    ImgBddCheckValidity(array_fetch(bdd_t*, bddArray, i));
2430  }
2431  return 1;
2432}
2433
2434
2435/**Function********************************************************************
2436
2437  Synopsis    [This function checks the validity of a BDD.]
2438
2439  Description [[This function checks the validity of a BDD. Three checks are done:
2440  1. The BDD should not be freed. "free" field should be 0.
2441  2. The node pointer of the BDD should be a valid pointer.
2442  3. The manager pointer of the BDD should be a valid pointer.
2443  The assumption for 2 and 3 is that, the value of a valid pointer
2444  should be > 0xf.]
2445
2446  SideEffects []
2447
2448******************************************************************************/
2449int
2450ImgBddCheckValidity(bdd_t *bdd)
2451{
2452#ifndef NDEBUG
2453  int i;
2454#endif
2455  assert(bdd_get_free(bdd) == 0); /* Bdd should not have been freed */
2456  assert(((unsigned long)bdd_get_node(bdd, &i)) & ~0xf); /* Valid node pointer */
2457  assert(((unsigned long)bdd_get_manager(bdd)) & ~0xf); /* Valid manager pointer */
2458  return 1;
2459}
2460
2461
2462/**Function********************************************************************
2463
2464  Synopsis    [Prints the content of a table containing integers.]
2465
2466  Description [Prints the content of a table containing integers.]
2467
2468  SideEffects []
2469
2470******************************************************************************/
2471void
2472ImgPrintVarIdTable(st_table *table)
2473{
2474  st_generator *stgen;
2475  long varId;
2476  st_foreach_item(table, stgen, &varId, NULL){
2477    (void) fprintf(vis_stdout, "%d ", (int) varId);
2478  }
2479  (void) fprintf(vis_stdout, "\n");
2480}
2481
2482
2483/**Function********************************************************************
2484
2485  Synopsis    [Checks whether toCareSetArray changed.]
2486
2487  Description [Checks whether toCareSetArray changed.]
2488
2489  SideEffects []
2490
2491******************************************************************************/
2492int
2493ImgCheckToCareSetArrayChanged(array_t *toCareSetArray1,
2494                                array_t *toCareSetArray2)
2495{
2496  int   i, size1, size2;
2497  mdd_t *careSet1, *careSet2;
2498
2499  size1 = array_n(toCareSetArray1);
2500  size2 = array_n(toCareSetArray2);
2501
2502  if (size1 != size2)
2503    return(1);
2504
2505  for (i = 0; i < size1; i++) {
2506    careSet1 = array_fetch(mdd_t *, toCareSetArray1, i);
2507    careSet2 = array_fetch(mdd_t *, toCareSetArray2, i);
2508    if (bdd_equal(careSet1, careSet2) == 0)
2509      return(1);
2510  }
2511
2512  return(0);
2513}
2514
2515
2516/*---------------------------------------------------------------------------*/
2517
2518/* Definition of static functions                                            */
2519/*---------------------------------------------------------------------------*/
2520
2521/**Function********************************************************************
2522
2523  Synopsis    [Checks the validity of image]
2524
2525  Description [In a properly formed image, there should not be any
2526  domain or quantify variables in its support. This function checks
2527  for that fact.]
2528
2529  SideEffects []
2530
2531******************************************************************************/
2532static int
2533CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t
2534                   *domainVarMddIdArray, array_t *quantifyVarMddIdArray)
2535{
2536  int i;
2537  array_t *imageSupportArray = mdd_get_support(mddManager, image);
2538  st_table *imageSupportTable = st_init_table(st_numcmp, st_numhash);
2539  for (i=0; i<array_n(imageSupportArray); i++){
2540    long mddId = (long) array_fetch(int, imageSupportArray, i);
2541    (void) st_insert(imageSupportTable, (char *) mddId, NIL(char));
2542  }
2543  for (i=0; i<array_n(domainVarMddIdArray); i++){
2544    int domainVarId;
2545    domainVarId = array_fetch(int, domainVarMddIdArray, i);
2546    assert(st_is_member(imageSupportTable, (char *)(long)domainVarId) == 0);
2547  }
2548  for (i=0; i<array_n(quantifyVarMddIdArray); i++){
2549    int quantifyVarId;
2550    quantifyVarId = array_fetch(int, quantifyVarMddIdArray, i);
2551    assert(st_is_member(imageSupportTable, (char *)(long)quantifyVarId) == 0);
2552  }
2553  st_free_table(imageSupportTable);
2554  array_free(imageSupportArray);
2555  return 1;
2556}
2557
2558
Note: See TracBrowser for help on using the repository browser.