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

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

vis2.3
File size: 83.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [imgTfmBwd.c]
4
5  PackageName [img]
6
7  Synopsis    [Routines for preimage computation using transition function
8  method.]
9
10  Description []
11
12  SeeAlso     []
13
14  Author      [In-Ho Moon]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35******************************************************************************/
36#include "imgInt.h"
37
38static char rcsid[] UNUSED = "$Id: imgTfmBwd.c,v 1.29 2002/08/18 04:47:07 fabio Exp $";
39
40/*---------------------------------------------------------------------------*/
41/* Constant declarations                                                     */
42/*---------------------------------------------------------------------------*/
43
44/*---------------------------------------------------------------------------*/
45/* Type declarations                                                         */
46/*---------------------------------------------------------------------------*/
47
48/*---------------------------------------------------------------------------*/
49/* Structure declarations                                                    */
50/*---------------------------------------------------------------------------*/
51
52/*---------------------------------------------------------------------------*/
53/* Variable declarations                                                     */
54/*---------------------------------------------------------------------------*/
55
56/*---------------------------------------------------------------------------*/
57/* Macro declarations                                                        */
58/*---------------------------------------------------------------------------*/
59
60/**AutomaticStart*************************************************************/
61
62/*---------------------------------------------------------------------------*/
63/* Static function prototypes                                                */
64/*---------------------------------------------------------------------------*/
65
66static bdd_t * PreImageByDomainCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int splitMethod, int turnDepth, int depth);
67static mdd_t * PreImageByStaticDomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth);
68static bdd_t * PreImageByConstraintCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, int splitMethod, int turnDepth, int depth);
69static mdd_t * PreImageBySubstitution(ImgTfmInfo_t *info, array_t *vector, mdd_t *from);
70static bdd_t * PreImageMakeVectorCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube);
71static bdd_t * PreImageMakeRelationCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray);
72static bdd_t * PreImageDeleteOneComponent(ImgTfmInfo_t *info, array_t *delta, int index, array_t **newDelta);
73static int PreImageChooseSplitVar(ImgTfmInfo_t *info, array_t *delta, bdd_t *img, int splitMethod, int split);
74static mdd_t * DomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *c, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube);
75static int CheckPreImageVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *image);
76
77/**AutomaticEnd***************************************************************/
78
79
80/*---------------------------------------------------------------------------*/
81/* Definition of exported functions                                          */
82/*---------------------------------------------------------------------------*/
83
84
85/*---------------------------------------------------------------------------*/
86/* Definition of internal functions                                          */
87/*---------------------------------------------------------------------------*/
88
89
90/**Function********************************************************************
91
92  Synopsis    [Computes a preimage with transition function method.]
93
94  Description [Computes a preimage with transition function method.]
95
96  SideEffects []
97
98******************************************************************************/
99bdd_t *
100ImgTfmPreImage(ImgTfmInfo_t *info, bdd_t *image)
101{
102  bdd_t         *preImg, *pre;
103  int           turnDepth;
104  bdd_t         *refResult, *one;
105  array_t       *relationArray;
106  int           partial;
107  bdd_t         *from;
108  array_t       *vector;
109
110  if (bdd_is_tautology(image, 1)) {
111    preImg = mdd_one(info->manager);
112    return(preImg);
113  } else if (bdd_is_tautology(image, 0)) {
114    preImg = mdd_zero(info->manager);
115    return(preImg);
116  }
117
118  info->maxIntermediateSize = 0;
119  if (info->buildTR) {
120    if (info->option->preSplitMethod == 4 &&
121        info->option->preSplitMaxDepth < 0 &&
122        info->option->buildPartialTR == FALSE &&
123        info->preKeepPiInTr == FALSE &&
124        info->option->preCanonical == FALSE) {
125      mdd_t *range;
126      range = ImgSubstitute(image, info->functionData, Img_D2R_c);
127      preImg = ImgBddLinearAndSmooth(info->manager, range,
128                      info->bwdClusteredRelationArray,
129                      info->bwdArraySmoothVarBddArray,
130                      info->bwdSmoothVarCubeArray,
131                      info->option->verbosity);
132      mdd_free(range);
133      return(preImg);
134    }
135    relationArray = mdd_array_duplicate(info->bwdClusteredRelationArray);
136  } else
137    relationArray = NIL(array_t);
138
139  one = mdd_one(info->manager);
140
141  vector = info->vector;
142  from = image;
143
144  partial = 0;
145  if (info->option->preSplitMethod == 0) {
146    preImg = PreImageByDomainCofactoring(info, vector, from,
147                                         NIL(array_t), NIL(mdd_t), NIL(mdd_t),
148                                         info->option->preSplitMethod, 0, 0);
149  } else if (info->option->preSplitMethod == 1) {
150    preImg = PreImageByConstraintCofactoring(info, vector, from,
151                                             info->option->preSplitMethod,
152                                             0, 0);
153  } else if (info->option->preSplitMethod == 3) {
154    preImg = PreImageBySubstitution(info, vector, from);
155  } else {
156    turnDepth = info->option->turnDepth;
157    if (turnDepth == 0) {
158      if (info->option->preSplitMethod == 2) {
159        preImg = PreImageByConstraintCofactoring(info, vector, from,
160                                                 info->option->preSplitMethod,
161                                                 turnDepth, 0);
162      } else
163        preImg = ImgPreImageByHybrid(info, vector, from);
164    } else if (info->option->preSplitMethod == 2) {
165      preImg = PreImageByDomainCofactoring(info, vector, from,
166                                           relationArray,
167                                           NIL(mdd_t), NIL(mdd_t),
168                                           info->option->preSplitMethod,
169                                           turnDepth, 0);
170    } else {
171      if (info->buildTR) {
172        if (info->buildTR == 2) {
173          if (info->buildPartialTR) {
174            preImg = PreImageByStaticDomainCofactoring(info, vector,
175                                                        from, relationArray,
176                                                        turnDepth, 0);
177            partial = 1;
178          } else {
179            preImg = PreImageByStaticDomainCofactoring(info, NIL(array_t),
180                                                        from, relationArray,
181                                                        turnDepth, 0);
182          }
183        } else if (info->option->delayedSplit) {
184          preImg = PreImageByDomainCofactoring(info, vector, from,
185                                                relationArray, one, one,
186                                                info->option->preSplitMethod,
187                                                turnDepth, 0);
188        } else {
189          preImg = PreImageByDomainCofactoring(info, vector, from,
190                                                relationArray,
191                                                NIL(mdd_t), NIL(mdd_t),
192                                                info->option->preSplitMethod,
193                                                turnDepth, 0);
194        }
195      } else {
196        preImg = PreImageByDomainCofactoring(info, vector, from,
197                                             relationArray,
198                                             NIL(mdd_t), NIL(mdd_t),
199                                             info->option->preSplitMethod,
200                                             turnDepth, 0);
201      }
202    }
203  }
204  mdd_free(one);
205
206  if (info->option->debug) {
207    if (info->buildTR == 2) {
208      refResult = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t),
209                                                        image, relationArray,
210                                                        NIL(mdd_t), NIL(mdd_t));
211    } else {
212      if (partial) {
213        refResult = ImgPreImageByHybridWithStaticSplit(info, info->vector,
214                                                        image, relationArray,
215                                                        NIL(mdd_t), NIL(mdd_t));
216      } else
217        refResult = ImgPreImageByHybrid(info, info->vector, image);
218    }
219    assert(mdd_equal_mod_care_set_array(refResult, preImg,
220                                        info->toCareSetArray));
221    mdd_free(refResult);
222  }
223
224  if (relationArray)
225    mdd_array_free(relationArray);
226
227  if (info->preCache && info->option->autoFlushCache == 1)
228    ImgFlushCache(info->preCache);
229  if (info->preKeepPiInTr == TRUE) {
230    if (info->functionData->quantifyCube)
231      pre = bdd_smooth_with_cube(preImg, info->functionData->quantifyCube);
232    else
233      pre = bdd_smooth(preImg, info->functionData->quantifyBddVars);
234    mdd_free(preImg);
235  } else
236    pre = preImg;
237  if (info->option->verbosity) {
238    fprintf(vis_stdout,
239            "** tfm info: max BDD size for intermediate product = %d\n",
240            info->maxIntermediateSize);
241  }
242  return(pre);
243}
244
245
246/*---------------------------------------------------------------------------*/
247/* Definition of static functions                                            */
248/*---------------------------------------------------------------------------*/
249
250
251/**Function********************************************************************
252
253  Synopsis    [Computes preimage with domain cofactoring method.]
254
255  Description [Computes preimage with domain cofactoring method.]
256
257  SideEffects []
258
259******************************************************************************/
260static bdd_t *
261PreImageByDomainCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image,
262                            array_t *relationArray,
263                            mdd_t *cofactorCube, mdd_t *abstractCube,
264                            int splitMethod, int turnDepth, int depth)
265{
266  array_t       *newDelta, *tmpDelta, *vectorT, *vectorE;
267  bdd_t         *preImg, *preImgT, *preImgE, *imgT, *imgE, *newImg, *tmpImg;
268  int           split;
269  bdd_t         *var, *varNot, *refResult;
270  int           nRecur;
271  array_t       *relationArrayT, *relationArrayE;
272  array_t       *newRelationArray, *tmpRelationArray;
273  mdd_t         *cofactorCubeT, *cofactorCubeE;
274  mdd_t         *abstractCubeT, *abstractCubeE;
275  mdd_t         *newCofactorCube, *newAbstractCube;
276  mdd_t         *cofactor, *abstract;
277  mdd_t         *essentialCube, *tmp;
278  int           findEssential;
279  int           foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE;
280  int           turnFlag, size;
281  mdd_t         *saveCareSet = NIL(mdd_t);
282
283  newRelationArray = NIL(array_t);
284
285  if (info->option->checkEquivalence && relationArray) {
286    assert(ImgCheckEquivalence(info, delta, relationArray,
287                                cofactorCube, abstractCube, 1));
288  }
289
290  info->nRecursionB++;
291  if (info->option->debug) {
292    if (relationArray) {
293      refResult = ImgPreImageByHybrid(info, delta, image);
294      preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), image,
295                                                  relationArray,
296                                                  cofactorCube, abstractCube);
297      tmp = refResult;
298      refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
299      mdd_free(tmp);
300      tmp = preImg;
301      preImg = mdd_and(tmp, info->debugCareSet, 1, 1);
302      mdd_free(tmp);
303      assert(mdd_equal_mod_care_set_array(refResult, preImg,
304                                          info->toCareSetArray));
305      mdd_free(refResult);
306      mdd_free(preImg);
307    }
308  }
309
310  if (info->nIntermediateVars)
311    size = ImgVectorFunctionSize(delta);
312  else
313    size = array_n(delta);
314  if (size == 1) {
315    preImg = PreImageBySubstitution(info, delta, image);
316    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
317                                (float)depth) / (float)(info->nLeavesB + 1);
318    if (depth > info->maxDepthB)
319      info->maxDepthB = depth;
320    info->nLeavesB++;
321    info->foundEssentialDepth = info->option->maxEssentialDepth;
322    return(preImg);
323  }
324
325  if (info->option->findEssential) {
326    if (info->option->findEssential == 1)
327      findEssential = 1;
328    else {
329      if (depth >= info->lastFoundEssentialDepth)
330        findEssential = 1;
331      else
332        findEssential = 0;
333    }
334  } else
335    findEssential = 0;
336  if (findEssential) {
337    essentialCube = bdd_find_essential_cube(image);
338
339    if (!bdd_is_tautology(essentialCube, 1)) {
340      info->averageFoundEssential = (info->averageFoundEssential *
341        (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) /
342        (float)(info->nFoundEssentials + 1);
343      info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth *
344        (float)info->nFoundEssentials + (float)depth) /
345        (float)(info->nFoundEssentials + 1);
346      if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth)
347        info->topFoundEssentialDepth = depth;
348      if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
349        info->foundEssentials[depth]++;
350      info->nFoundEssentials++;
351      if (info->option->delayedSplit && relationArray) {
352        tmpRelationArray = relationArray;
353        tmpImg = ImgVectorMinimize(info, delta, essentialCube, image,
354                        tmpRelationArray, &tmpDelta, NIL(mdd_t *),
355                        NIL(array_t *), &cofactor, &abstract);
356        if (bdd_is_tautology(cofactor, 1))
357          newCofactorCube = cofactorCube;
358        else
359          newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1);
360        mdd_free(cofactor);
361        if (bdd_is_tautology(abstract, 1))
362          newAbstractCube = abstractCube;
363        else
364          newAbstractCube = mdd_and(abstractCube, abstract, 1, 1);
365        mdd_free(abstract);
366      } else {
367        if (relationArray)
368          tmpRelationArray = mdd_array_duplicate(relationArray);
369        else
370          tmpRelationArray = relationArray;
371        tmpImg = ImgVectorMinimize(info, delta, essentialCube, image,
372                        tmpRelationArray, &tmpDelta, NIL(mdd_t *),
373                        NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *));
374        newCofactorCube = cofactorCube;
375        newAbstractCube = abstractCube;
376      }
377      foundEssentialDepth = depth;
378    } else {
379      tmpDelta = delta;
380      tmpRelationArray = relationArray;
381      tmpImg = image;
382      newCofactorCube = cofactorCube;
383      newAbstractCube = abstractCube;
384      foundEssentialDepth = info->option->maxEssentialDepth;
385    }
386    mdd_free(essentialCube);
387    foundEssentialDepthT = info->option->maxEssentialDepth;
388    foundEssentialDepthE = info->option->maxEssentialDepth;
389  } else {
390    tmpDelta = delta;
391    tmpRelationArray = relationArray;
392    tmpImg = image;
393    newCofactorCube = cofactorCube;
394    newAbstractCube = abstractCube;
395    /* To remove compiler warnings */
396    foundEssentialDepth = -1;
397    foundEssentialDepthT = -1;
398    foundEssentialDepthE = -1;
399  }
400
401  if (!info->option->preCanonical) {
402    newImg = tmpImg;
403    newDelta = tmpDelta;
404    newRelationArray = tmpRelationArray;
405  } else if (info->option->delayedSplit && relationArray) {
406    newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg,
407                                        tmpRelationArray, &newDelta,
408                                        &newRelationArray,
409                                        &cofactor, &abstract);
410    if (!bdd_is_tautology(cofactor, 1)) {
411      if (newCofactorCube == cofactorCube)
412        newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1);
413      else {
414        tmp = newCofactorCube;
415        newCofactorCube = mdd_and(tmp, cofactor, 1, 1);
416        mdd_free(tmp);
417      }
418    }
419    mdd_free(cofactor);
420    if (!bdd_is_tautology(abstract, 1)) {
421      if (newAbstractCube == abstractCube)
422        newAbstractCube = mdd_and(abstractCube, abstract, 1, 1);
423      else {
424        tmp = newAbstractCube;
425        newAbstractCube = mdd_and(tmp, abstract, 1, 1);
426        mdd_free(tmp);
427      }
428    }
429    mdd_free(abstract);
430  } else {
431    newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg,
432                                        tmpRelationArray, &newDelta,
433                                        &newRelationArray,
434                                        NIL(mdd_t *), NIL(mdd_t *));
435  }
436  if (tmpDelta != delta)
437    ImgVectorFree(tmpDelta);
438  if (tmpImg != image)
439    mdd_free(tmpImg);
440  if (tmpRelationArray && tmpRelationArray != relationArray &&
441      tmpRelationArray != newRelationArray) {
442    mdd_array_free(tmpRelationArray);
443  }
444
445  if (info->option->debug) {
446    if (relationArray) {
447      refResult = ImgPreImageByHybrid(info, newDelta, newImg);
448      preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg,
449                                                  newRelationArray,
450                                                  newCofactorCube,
451                                                  newAbstractCube);
452      tmp = refResult;
453      refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
454      mdd_free(tmp);
455      tmp = preImg;
456      preImg = mdd_and(tmp, info->debugCareSet, 1, 1);
457      mdd_free(tmp);
458      assert(mdd_equal_mod_care_set_array(refResult, preImg,
459                                          info->toCareSetArray));
460      mdd_free(refResult);
461      mdd_free(preImg);
462    }
463  }
464
465  if (bdd_is_tautology(newImg, 1) || bdd_is_tautology(newImg, 0)) {
466    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
467                                (float)depth) / (float)(info->nLeavesB + 1);
468    if (depth > info->maxDepthB)
469      info->maxDepthB = depth;
470    info->nLeavesB++;
471    if (info->option->debug) {
472      refResult = ImgPreImageByHybrid(info, newDelta, newImg);
473      tmp = refResult;
474      refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
475      mdd_free(tmp);
476      tmp = mdd_and(newImg, info->debugCareSet, 1, 1);
477      assert(mdd_equal_mod_care_set_array(refResult, tmp,
478                                          info->toCareSetArray));
479      mdd_free(refResult);
480      mdd_free(tmp);
481    }
482    if (newDelta != delta)
483      ImgVectorFree(newDelta);
484    if (relationArray && newRelationArray != relationArray)
485      mdd_array_free(newRelationArray);
486    if (newCofactorCube && newCofactorCube != cofactorCube)
487      mdd_free(newCofactorCube);
488    if (newAbstractCube && newAbstractCube != abstractCube)
489      mdd_free(newAbstractCube);
490    if (findEssential)
491      info->foundEssentialDepth = foundEssentialDepth;
492    return(newImg);
493  }
494  if (array_n(newDelta) <= 1) {
495    if (array_n(newDelta) == 0)
496      preImg = newImg;
497    else {
498      assert(array_n(newDelta) == 1);
499      preImg = PreImageBySubstitution(info, newDelta, newImg);
500      mdd_free(newImg);
501    }
502    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
503                                (float)depth) / (float)(info->nLeavesB + 1);
504    if (depth > info->maxDepthB)
505      info->maxDepthB = depth;
506    info->nLeavesB++;
507    if (info->option->debug) {
508      refResult = ImgPreImageByHybrid(info, delta, image);
509      tmp = refResult;
510      refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
511      mdd_free(tmp);
512      tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
513      assert(mdd_equal_mod_care_set_array(refResult, tmp,
514                                          info->toCareSetArray));
515      mdd_free(refResult);
516      mdd_free(tmp);
517    }
518    if (newDelta != delta)
519      ImgVectorFree(newDelta);
520    if (relationArray && newRelationArray != relationArray)
521      mdd_array_free(newRelationArray);
522    if (newCofactorCube && newCofactorCube != cofactorCube)
523      mdd_free(newCofactorCube);
524    if (newAbstractCube && newAbstractCube != abstractCube)
525      mdd_free(newAbstractCube);
526    if (findEssential)
527      info->foundEssentialDepth = foundEssentialDepth;
528    return(preImg);
529  }
530
531  if (info->preCache) {
532    preImg = ImgCacheLookupTable(info, info->preCache, newDelta, newImg);
533    if (preImg) {
534      info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
535                                (float)depth) / (float)(info->nLeavesB + 1);
536      if (depth > info->maxDepthB)
537        info->maxDepthB = depth;
538      info->nLeavesB++;
539      if (info->option->debug) {
540        refResult = ImgPreImageByHybrid(info, newDelta, newImg);
541        tmp = refResult;
542        refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
543        mdd_free(tmp);
544        tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
545        assert(mdd_equal_mod_care_set_array(refResult, tmp,
546                                            info->toCareSetArray));
547        mdd_free(refResult);
548        mdd_free(tmp);
549      }
550      if (newDelta != delta)
551        ImgVectorFree(newDelta);
552      if (newImg != image)
553        mdd_free(newImg);
554      if (relationArray && newRelationArray != relationArray)
555        mdd_array_free(newRelationArray);
556      if (newCofactorCube && newCofactorCube != cofactorCube)
557        mdd_free(newCofactorCube);
558      if (newAbstractCube && newAbstractCube != abstractCube)
559        mdd_free(newAbstractCube);
560      if (findEssential)
561        info->foundEssentialDepth = foundEssentialDepth;
562      return(preImg);
563    }
564  }
565
566  turnFlag = 0;
567  if (splitMethod == 4 && turnDepth == -1) {
568    if (depth < info->option->preSplitMinDepth) {
569      info->nSplitsB++;
570      turnFlag = 0;
571    } else if (depth > info->option->preSplitMaxDepth) {
572      info->nConjoinsB++;
573      turnFlag = 1;
574    } else {
575      turnFlag = ImgDecideSplitOrConjoin(info, newDelta, newImg, 1,
576                                         newRelationArray, newCofactorCube,
577                                         newAbstractCube, 0, depth);
578    }
579  } else {
580    if (depth == turnDepth)
581      turnFlag = 1;
582    else
583      turnFlag = 0;
584  }
585  if (turnFlag) {
586    if (splitMethod == 2) {
587      preImg = PreImageByConstraintCofactoring(info, newDelta, newImg,
588                                                info->option->preSplitMethod,
589                                                0, depth + 1);
590    } else {
591      if (relationArray) {
592        preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg,
593                                                    newRelationArray,
594                                                    newCofactorCube,
595                                                    newAbstractCube);
596      } else
597        preImg = ImgPreImageByHybrid(info, newDelta, newImg);
598    }
599    if (info->option->debug) {
600      refResult = ImgPreImageByHybrid(info, newDelta, newImg);
601      tmp = refResult;
602      refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
603      mdd_free(tmp);
604      tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
605      assert(mdd_equal_mod_care_set_array(refResult, tmp,
606                                          info->toCareSetArray));
607      mdd_free(refResult);
608      mdd_free(tmp);
609    }
610    if (splitMethod == 4) {
611      if (info->preCache)
612        ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
613      else {
614        if (newDelta != delta)
615          ImgVectorFree(newDelta);
616        if (newImg != image)
617          mdd_free(newImg);
618      }
619      info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
620                              (float)depth) / (float)(info->nLeavesB + 1);
621      if (depth > info->maxDepthB)
622        info->maxDepthB = depth;
623      info->nLeavesB++;
624    } else {
625      if (newDelta != delta)
626        ImgVectorFree(newDelta);
627      if (newImg != image)
628        mdd_free(newImg);
629    }
630    if (relationArray && newRelationArray != relationArray)
631      mdd_array_free(newRelationArray);
632    if (newCofactorCube && newCofactorCube != cofactorCube)
633      mdd_free(newCofactorCube);
634    if (newAbstractCube && newAbstractCube != abstractCube)
635      mdd_free(newAbstractCube);
636    info->nTurnsB++;
637    if (findEssential)
638      info->foundEssentialDepth = foundEssentialDepth;
639    return(preImg);
640  }
641
642  split = PreImageChooseSplitVar(info, newDelta, newImg,
643                                 0, info->option->preInputSplit);
644
645  /* No more present state variable to split */
646  if (split == -1) {
647    if (info->option->preDcLeafMethod == 0 ||
648        info->option->preDcLeafMethod == 2) {
649      if (info->option->preDcLeafMethod == 0)
650        preImg = PreImageBySubstitution(info, newDelta, newImg);
651      else if (relationArray) {
652        preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg,
653                                                    newRelationArray,
654                                                    newCofactorCube,
655                                                    newAbstractCube);
656      } else
657        preImg = ImgPreImageByHybrid(info, newDelta, newImg);
658      if (info->preCache)
659        ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
660      info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
661                                (float)depth) / (float)(info->nLeavesB + 1);
662      if (depth > info->maxDepthB)
663        info->maxDepthB = depth;
664      info->nLeavesB++;
665    } else {
666      preImg = PreImageByConstraintCofactoring(info, newDelta, newImg,
667                                            splitMethod, turnDepth,
668                                            depth + 1);
669      info->nRecursionB--;
670    }
671    if (splitMethod == 0)
672      info->nTurnsB++;
673    if (info->option->debug) {
674      refResult = ImgPreImageByHybrid(info, newDelta, newImg);
675      tmp = refResult;
676      refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
677      mdd_free(tmp);
678      tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
679      assert(mdd_equal_mod_care_set_array(refResult, tmp,
680                                          info->toCareSetArray));
681      mdd_free(refResult);
682      mdd_free(tmp);
683    }
684    if (info->option->preDcLeafMethod != 0 || !info->preCache) {
685      if (newDelta != delta)
686        ImgVectorFree(newDelta);
687      if (newImg != image)
688        mdd_free(newImg);
689    }
690    if (relationArray && newRelationArray != relationArray)
691      mdd_array_free(newRelationArray);
692    if (newCofactorCube && newCofactorCube != cofactorCube)
693      mdd_free(newCofactorCube);
694    if (newAbstractCube && newAbstractCube != abstractCube)
695      mdd_free(newAbstractCube);
696    if (findEssential)
697      info->foundEssentialDepth = foundEssentialDepth;
698    return(preImg);
699  }
700
701  var = bdd_var_with_index(info->manager, split);
702  varNot = mdd_not(var);
703  if (info->option->delayedSplit && relationArray) {
704    imgT = DomainCofactoring(info, newDelta, newImg, newRelationArray, var,
705                             &vectorT, &relationArrayT, &cofactor, &abstract);
706    if (bdd_is_tautology(cofactor, 1))
707      cofactorCubeT = newCofactorCube;
708    else
709      cofactorCubeT = mdd_and(newCofactorCube, cofactor, 1, 1);
710    mdd_free(cofactor);
711    if (bdd_is_tautology(abstract, 1))
712      abstractCubeT = newAbstractCube;
713    else
714      abstractCubeT = mdd_and(newAbstractCube, abstract, 1, 1);
715    mdd_free(abstract);
716
717    imgE = DomainCofactoring(info, newDelta, newImg, newRelationArray, varNot,
718                             &vectorE, &relationArrayE, &cofactor, &abstract);
719    if (bdd_is_tautology(cofactor, 1))
720      cofactorCubeE = newCofactorCube;
721    else
722      cofactorCubeE = mdd_and(newCofactorCube, cofactor, 1, 1);
723    mdd_free(cofactor);
724    if (bdd_is_tautology(abstract, 1))
725      abstractCubeE = newAbstractCube;
726    else
727      abstractCubeE = mdd_and(newAbstractCube, abstract, 1, 1);
728    mdd_free(abstract);
729  } else {
730    imgT = DomainCofactoring(info, newDelta, newImg, newRelationArray, var,
731                             &vectorT, &relationArrayT,
732                             NIL(mdd_t *), NIL(mdd_t *));
733    cofactorCubeT = NIL(mdd_t);
734    abstractCubeT = NIL(mdd_t);
735
736    imgE = DomainCofactoring(info, newDelta, newImg, newRelationArray, varNot,
737                             &vectorE, &relationArrayE,
738                             NIL(mdd_t *), NIL(mdd_t *));
739    cofactorCubeE = NIL(mdd_t);
740    abstractCubeE = NIL(mdd_t);
741  }
742  if (relationArray && newRelationArray != relationArray)
743    mdd_array_free(newRelationArray);
744  mdd_free(varNot);
745
746  if (!info->preCache && !info->option->debug) {
747    if (newDelta != delta)
748      ImgVectorFree(newDelta);
749    if (newImg != image)
750      mdd_free(newImg);
751  }
752
753  nRecur = 0;
754  if (bdd_is_tautology(imgT, 1))
755    preImgT = mdd_one(info->manager);
756  else if (bdd_is_tautology(imgT, 0))
757    preImgT = mdd_zero(info->manager);
758  else {
759    if (info->option->debug) {
760      saveCareSet = info->debugCareSet;
761      info->debugCareSet = mdd_and(saveCareSet, var, 1, 1);
762    }
763    preImgT = PreImageByDomainCofactoring(info, vectorT, imgT, relationArrayT,
764                                          cofactorCubeT, abstractCubeT,
765                                          splitMethod, turnDepth,
766                                          depth + 1);
767    if (info->option->debug) {
768      mdd_free(info->debugCareSet);
769      info->debugCareSet = saveCareSet;
770    }
771    if (findEssential)
772      foundEssentialDepthT = info->foundEssentialDepth;
773    nRecur++;
774  }
775  ImgVectorFree(vectorT);
776  mdd_free(imgT);
777  if (relationArrayT && relationArrayT != newRelationArray)
778    mdd_array_free(relationArrayT);
779  if (cofactorCubeT && cofactorCubeT != newCofactorCube)
780    mdd_free(cofactorCubeT);
781  if (abstractCubeT && abstractCubeT != newAbstractCube)
782    mdd_free(abstractCubeT);
783
784  if (bdd_is_tautology(imgE, 1))
785    preImgE = mdd_one(info->manager);
786  else if (bdd_is_tautology(imgE, 0))
787    preImgE = mdd_zero(info->manager);
788  else {
789    if (info->option->debug) {
790      saveCareSet = info->debugCareSet;
791      info->debugCareSet = mdd_and(saveCareSet, var, 1, 0);
792    }
793    preImgE = PreImageByDomainCofactoring(info, vectorE, imgE, relationArrayE,
794                                          cofactorCubeE, abstractCubeE,
795                                          splitMethod, turnDepth,
796                                          depth + 1);
797    if (info->option->debug) {
798      mdd_free(info->debugCareSet);
799      info->debugCareSet = saveCareSet;
800    }
801    if (findEssential)
802      foundEssentialDepthE = info->foundEssentialDepth;
803    nRecur++;
804  }
805  ImgVectorFree(vectorE);
806  mdd_free(imgE);
807  if (relationArrayE && relationArrayT != newRelationArray)
808    mdd_array_free(relationArrayE);
809  if (cofactorCubeE && cofactorCubeE != newCofactorCube)
810    mdd_free(cofactorCubeE);
811  if (abstractCubeE && abstractCubeE != newAbstractCube)
812    mdd_free(abstractCubeE);
813  if (newCofactorCube && newCofactorCube != cofactorCube)
814    mdd_free(newCofactorCube);
815  if (newAbstractCube && newAbstractCube != abstractCube)
816    mdd_free(newAbstractCube);
817
818  preImg = bdd_ite(var, preImgT, preImgE, 1, 1, 1);
819  if (info->option->verbosity) {
820    size = bdd_size(preImg);
821    if (size > info->maxIntermediateSize)
822      info->maxIntermediateSize = size;
823    if (info->option->printBddSize) {
824      fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n",
825              bdd_size(preImgT), bdd_size(preImgE), bdd_size(preImg));
826    }
827  }
828  mdd_free(var);
829  mdd_free(preImgE);
830  mdd_free(preImgT);
831
832  if (info->preCache)
833    ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
834
835  if (info->option->debug) {
836    refResult = ImgPreImageByHybrid(info, newDelta, newImg);
837    tmp = refResult;
838    refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
839    mdd_free(tmp);
840    tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
841    assert(mdd_equal_mod_care_set_array(refResult, tmp,
842                                        info->toCareSetArray));
843    mdd_free(refResult);
844    mdd_free(tmp);
845    if (!info->preCache) {
846      if (newDelta != delta)
847        ImgVectorFree(newDelta);
848      if (newImg != image)
849        mdd_free(newImg);
850    }
851  }
852
853  if (nRecur == 0) {
854    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
855                                (float)depth) / (float)(info->nLeavesB + 1);
856    if (depth > info->maxDepthB)
857      info->maxDepthB = depth;
858    info->nLeavesB++;
859  }
860
861  if (findEssential) {
862    if (foundEssentialDepth == info->option->maxEssentialDepth) {
863      if (foundEssentialDepthT < foundEssentialDepthE)
864        foundEssentialDepth = foundEssentialDepthT;
865      else
866        foundEssentialDepth = foundEssentialDepthE;
867    }
868    info->foundEssentialDepth = foundEssentialDepth;
869  }
870  return(preImg);
871}
872
873
874/**Function********************************************************************
875
876  Synopsis    [Computes a preimage by static input splitting.]
877
878  Description [Computes a preimage by static input splitting.]
879
880  SideEffects []
881
882******************************************************************************/
883static mdd_t *
884PreImageByStaticDomainCofactoring(ImgTfmInfo_t *info, array_t *vector,
885                                  mdd_t *from, array_t *relationArray,
886                                  int turnDepth, int depth)
887{
888  array_t       *vectorT, *vectorE, *newVector;
889  mdd_t         *resT, *resE, *res, *cubeT, *cubeE;
890  mdd_t         *fromT, *fromE, *newFrom, *tmpFrom;
891  mdd_t         *var, *varNot;
892  array_t       *relationArrayT, *relationArrayE;
893  array_t       *newRelationArray, *tmpRelationArray;
894  int           nRecur;
895  mdd_t         *essentialCube, *refResult;
896  int           findEssential;
897  int           foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE;
898  int           turnFlag, size;
899  mdd_t         *saveCareSet = NIL(mdd_t), *tmp;
900
901  info->nRecursionB++;
902
903  turnFlag = 0;
904  if (turnDepth == -1) {
905    if (depth < info->option->preSplitMinDepth) {
906      info->nSplitsB++;
907      turnFlag = 0;
908    } else if (depth > info->option->preSplitMaxDepth) {
909      info->nConjoinsB++;
910      turnFlag = 1;
911    } else {
912      turnFlag = ImgDecideSplitOrConjoin(info, vector, from, 1,
913                                         relationArray, NIL(mdd_t),
914                                         NIL(mdd_t), 1, depth);
915    }
916  } else {
917    if (depth == turnDepth)
918      turnFlag = 1;
919    else
920      turnFlag = 0;
921  }
922  if (turnFlag) {
923    res = ImgPreImageByHybridWithStaticSplit(info, vector, from, relationArray,
924                                             NIL(mdd_t), NIL(mdd_t));
925    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
926                          (float)depth) / (float)(info->nLeavesB + 1);
927    if (depth > info->maxDepthB)
928      info->maxDepthB = depth;
929    info->nLeavesB++;
930    info->foundEssentialDepth = info->option->maxEssentialDepth;
931    return(res);
932  }
933
934  if (info->option->findEssential) {
935    if (info->option->findEssential == 1)
936      findEssential = 1;
937    else {
938      if (depth >= info->lastFoundEssentialDepth)
939        findEssential = 1;
940      else
941        findEssential = 0;
942    }
943  } else
944    findEssential = 0;
945  if (findEssential) {
946    essentialCube = bdd_find_essential_cube(from);
947
948    if (!bdd_is_tautology(essentialCube, 1)) {
949      info->averageFoundEssential = (info->averageFoundEssential *
950        (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) /
951        (float)(info->nFoundEssentials + 1);
952      info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth *
953        (float)info->nFoundEssentials + (float)depth) /
954        (float)(info->nFoundEssentials + 1);
955      if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth)
956        info->topFoundEssentialDepth = depth;
957      if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
958        info->foundEssentials[depth]++;
959      info->nFoundEssentials++;
960      if (vector) {
961        array_t *tmpVector;
962        if (info->option->preCanonical) {
963          tmpFrom = PreImageMakeRelationCanonical(info, vector, from,
964                                                relationArray, &newVector,
965                                                &newRelationArray);
966        } else {
967          tmpFrom = from;
968          newVector = vector;
969          newRelationArray = relationArray;
970        }
971        tmpVector = newVector;
972        newFrom = ImgVectorMinimize(info, tmpVector, essentialCube, tmpFrom,
973                        newRelationArray, &newVector, NIL(mdd_t *),
974                        NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *));
975        if (tmpVector != vector)
976          ImgVectorFree(tmpVector);
977        if (tmpFrom != from)
978          mdd_free(tmpFrom);
979      } else {
980        tmpRelationArray = ImgGetCofactoredRelationArray(relationArray,
981                                                         essentialCube);
982        if (info->option->preCanonical) {
983          newFrom = PreImageMakeRelationCanonical(info, vector, from,
984                                                tmpRelationArray, &newVector,
985                                                &newRelationArray);
986          mdd_array_free(tmpRelationArray);
987        } else {
988          newFrom = from;
989          newVector = vector;
990          newRelationArray = tmpRelationArray;
991        }
992      }
993      foundEssentialDepth = depth;
994    } else {
995      if (info->option->preCanonical) {
996        newFrom = PreImageMakeRelationCanonical(info, vector, from,
997                                                relationArray,
998                                                &newVector, &newRelationArray);
999      } else {
1000        newFrom = from;
1001        newVector = vector;
1002        newRelationArray = relationArray;
1003      }
1004      foundEssentialDepth = info->option->maxEssentialDepth;
1005    }
1006    mdd_free(essentialCube);
1007    foundEssentialDepthT = info->option->maxEssentialDepth;
1008    foundEssentialDepthE = info->option->maxEssentialDepth;
1009  } else {
1010    if (info->option->preCanonical) {
1011      newFrom = PreImageMakeRelationCanonical(info, vector, from, relationArray,
1012                                            &newVector, &newRelationArray);
1013    } else {
1014      newFrom = from;
1015      newVector = vector;
1016      newRelationArray = relationArray;
1017    }
1018    /* To remove compiler warnings */
1019    foundEssentialDepth = -1;
1020    foundEssentialDepthT = -1;
1021    foundEssentialDepthE = -1;
1022  }
1023
1024  if (info->option->debug) {
1025    refResult = ImgPreImageByHybridWithStaticSplit(info, vector, from,
1026                                                   relationArray,
1027                                                   NIL(mdd_t), NIL(mdd_t));
1028    res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom,
1029                                                   newRelationArray,
1030                                                   NIL(mdd_t), NIL(mdd_t));
1031    tmp = refResult;
1032    refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
1033    mdd_free(tmp);
1034    tmp = res;
1035    res = mdd_and(tmp, info->debugCareSet, 1, 1);
1036    mdd_free(tmp);
1037    assert(mdd_equal_mod_care_set_array(refResult, res, info->toCareSetArray));
1038    mdd_free(refResult);
1039    mdd_free(res);
1040  }
1041
1042  if (bdd_is_tautology(newFrom, 1)) {
1043    if (newVector && newVector != vector)
1044      ImgVectorFree(newVector);
1045    if (newRelationArray != relationArray)
1046      mdd_array_free(newRelationArray);
1047    if (newFrom != from)
1048      mdd_free(newFrom);
1049    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1050                          (float)depth) / (float)(info->nLeavesB + 1);
1051    if (depth > info->maxDepthB)
1052      info->maxDepthB = depth;
1053    info->nLeavesB++;
1054    if (findEssential)
1055      info->foundEssentialDepth = foundEssentialDepth;
1056    return(mdd_one(info->manager));
1057  }
1058
1059  if (depth == turnDepth ||
1060      (info->option->splitCubeFunc && bdd_is_cube(newFrom))) {
1061    res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom,
1062                                             newRelationArray,
1063                                             NIL(mdd_t), NIL(mdd_t));
1064    if (newVector && newVector != vector)
1065      ImgVectorFree(newVector);
1066    if (newRelationArray != relationArray)
1067      mdd_array_free(newRelationArray);
1068    if (newFrom != from)
1069      mdd_free(newFrom);
1070    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1071                          (float)depth) / (float)(info->nLeavesB + 1);
1072    if (depth > info->maxDepthB)
1073      info->maxDepthB = depth;
1074    info->nLeavesB++;
1075    if (findEssential)
1076      info->foundEssentialDepth = foundEssentialDepth;
1077    return(res);
1078  }
1079
1080  var = ImgChooseTrSplitVar(info, newVector, newRelationArray,
1081                            info->option->trSplitMethod, 0);
1082  if (!var) {
1083    res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom,
1084                                                   newRelationArray,
1085                                                   NIL(mdd_t), NIL(mdd_t));
1086    if (newVector && newVector != vector)
1087      ImgVectorFree(newVector);
1088    if (newRelationArray != relationArray)
1089      mdd_array_free(newRelationArray);
1090    if (newFrom != from)
1091      mdd_free(newFrom);
1092    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1093                          (float)depth) / (float)(info->nLeavesB + 1);
1094    if (depth > info->maxDepthB)
1095      info->maxDepthB = depth;
1096    info->nLeavesB++;
1097    if (findEssential)
1098      info->foundEssentialDepth = foundEssentialDepth;
1099    return(res);
1100  }
1101
1102  varNot = mdd_not(var);
1103
1104  nRecur = 0;
1105  if (newVector) {
1106    ImgVectorConstrain(info, newVector, var, NIL(array_t),
1107                        &vectorT, &cubeT, NIL(array_t *),
1108                        NIL(mdd_t *), NIL(mdd_t *), TRUE);
1109    fromT = bdd_cofactor(newFrom, cubeT);
1110    mdd_free(cubeT);
1111  } else {
1112    vectorT = NIL(array_t);
1113    fromT = mdd_dup(newFrom);
1114  }
1115  relationArrayT = ImgGetCofactoredRelationArray(newRelationArray, var);
1116  if (bdd_is_tautology(fromT, 1)) {
1117    resT = mdd_one(info->manager);
1118    if (vectorT)
1119      ImgVectorFree(vectorT);
1120  } else if (bdd_is_tautology(fromT, 0)) {
1121    resT = mdd_zero(info->manager);
1122    if (vectorT)
1123      ImgVectorFree(vectorT);
1124  } else {
1125    if (info->option->debug) {
1126      saveCareSet = info->debugCareSet;
1127      info->debugCareSet = mdd_and(saveCareSet, var, 1, 1);
1128    }
1129    resT = PreImageByStaticDomainCofactoring(info, vectorT, fromT,
1130                             relationArrayT, turnDepth, depth + 1);
1131    if (info->option->debug) {
1132      mdd_free(info->debugCareSet);
1133      info->debugCareSet = saveCareSet;
1134    }
1135    if (findEssential)
1136      foundEssentialDepthE = info->foundEssentialDepth;
1137    if (vectorT)
1138      ImgVectorFree(vectorT);
1139    nRecur++;
1140  }
1141  mdd_free(fromT);
1142  mdd_array_free(relationArrayT);
1143
1144  if (newVector) {
1145    ImgVectorConstrain(info, newVector, varNot, NIL(array_t),
1146                        &vectorE, &cubeE, NIL(array_t *),
1147                        NIL(mdd_t *), NIL(mdd_t *), TRUE);
1148    if (newVector != vector)
1149      ImgVectorFree(newVector);
1150    fromE = bdd_cofactor(newFrom, cubeE);
1151    mdd_free(cubeE);
1152  } else {
1153    vectorE = NIL(array_t);
1154    fromE = mdd_dup(newFrom);
1155  }
1156  if (newFrom != from)
1157    mdd_free(newFrom);
1158  relationArrayE = ImgGetCofactoredRelationArray(newRelationArray, varNot);
1159  if (newRelationArray != relationArray)
1160    mdd_array_free(newRelationArray);
1161  if (bdd_is_tautology(fromE, 1)) {
1162    resE = mdd_one(info->manager);
1163    if (vectorE)
1164      ImgVectorFree(vectorE);
1165  } else if (bdd_is_tautology(fromE, 0)) {
1166    resE = mdd_zero(info->manager);
1167    if (vectorE)
1168      ImgVectorFree(vectorE);
1169  } else {
1170    if (info->option->debug) {
1171      saveCareSet = info->debugCareSet;
1172      info->debugCareSet = mdd_and(saveCareSet, var, 1, 0);
1173    }
1174    resE = PreImageByStaticDomainCofactoring(info, vectorE, fromE,
1175                             relationArrayE, turnDepth, depth + 1);
1176    if (info->option->debug) {
1177      mdd_free(info->debugCareSet);
1178      info->debugCareSet = saveCareSet;
1179    }
1180    if (findEssential)
1181      foundEssentialDepthE = info->foundEssentialDepth;
1182    if (vectorE)
1183      ImgVectorFree(vectorE);
1184    nRecur++;
1185  }
1186  mdd_free(fromE);
1187  mdd_array_free(relationArrayE);
1188 
1189  res = bdd_ite(var, resT, resE, 1, 1, 1);
1190  if (info->option->verbosity) {
1191    size = bdd_size(res);
1192    if (size > info->maxIntermediateSize)
1193      info->maxIntermediateSize = size;
1194    if (info->option->printBddSize) {
1195      fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n",
1196              bdd_size(resT), bdd_size(resE), bdd_size(res));
1197    }
1198  }
1199  mdd_free(resT);
1200  mdd_free(resE);
1201  mdd_free(var);
1202  mdd_free(varNot);
1203
1204  if (info->option->debug) {
1205    refResult = ImgPreImageByHybridWithStaticSplit(info, vector, from,
1206                                                   relationArray,
1207                                                   NIL(mdd_t), NIL(mdd_t));
1208    tmp = refResult;
1209    refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
1210    mdd_free(tmp);
1211    tmp = mdd_and(res, info->debugCareSet, 1, 1);
1212    assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray));
1213    mdd_free(refResult);
1214    mdd_free(tmp);
1215  }
1216
1217  if (nRecur == 0) {
1218    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1219                          (float)depth) / (float)(info->nLeavesB + 1);
1220    if (depth > info->maxDepthB)
1221      info->maxDepthB = depth;
1222    info->nLeavesB++;
1223  }
1224
1225  if (findEssential) {
1226    if (foundEssentialDepth == info->option->maxEssentialDepth) {
1227      if (foundEssentialDepthT < foundEssentialDepthE)
1228        foundEssentialDepth = foundEssentialDepthT;
1229      else
1230        foundEssentialDepth = foundEssentialDepthE;
1231    }
1232    info->foundEssentialDepth = foundEssentialDepth;
1233  }
1234  return(res);
1235}
1236
1237
1238/**Function********************************************************************
1239
1240  Synopsis    [Computes preimage with constraint cofactoring method.]
1241
1242  Description [Computes preimage with constraint cofactoring method.]
1243
1244  SideEffects []
1245
1246******************************************************************************/
1247static bdd_t *
1248PreImageByConstraintCofactoring(ImgTfmInfo_t *info, array_t *delta,
1249                                bdd_t *image, int splitMethod,
1250                                int turnDepth, int depth)
1251{
1252  array_t               *newDelta, *tmpDelta, *vector;
1253  bdd_t                 *preImg, *preImgT, *preImgE, *imgT, *imgE;
1254  bdd_t                 *c, *newImg, *tmpImg;
1255  int                   split;
1256  bdd_t                 *var, *varNot, *refResult;
1257  ImgComponent_t        *comp;
1258  int                   nRecur, size;
1259  mdd_t                 *essentialCube;
1260  int                   findEssential;
1261  int                   foundEssentialDepth;
1262  int                   foundEssentialDepthT, foundEssentialDepthE;
1263  mdd_t                 *saveCareSet = NIL(mdd_t), *tmp;
1264
1265  info->nRecursionB++;
1266
1267  if (info->nIntermediateVars)
1268    size = ImgVectorFunctionSize(delta);
1269  else
1270    size = array_n(delta);
1271  if (size == 1) {
1272    preImg = PreImageBySubstitution(info, delta, image);
1273    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1274                                (float)depth) / (float)(info->nLeavesB + 1);
1275    if (depth > info->maxDepthB)
1276      info->maxDepthB = depth;
1277    info->nLeavesB++;
1278    info->foundEssentialDepth = info->option->maxEssentialDepth;
1279    return(preImg);
1280  }
1281
1282  if (info->option->findEssential) {
1283    if (info->option->findEssential == 1)
1284      findEssential = 1;
1285    else {
1286      if (depth >= info->lastFoundEssentialDepth)
1287        findEssential = 1;
1288      else
1289        findEssential = 0;
1290    }
1291  } else
1292    findEssential = 0;
1293  if (findEssential) {
1294    essentialCube = bdd_find_essential_cube(image);
1295
1296    if (!bdd_is_tautology(essentialCube, 1)) {
1297      info->averageFoundEssential = (info->averageFoundEssential *
1298        (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) /
1299        (float)(info->nFoundEssentials + 1);
1300      info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth *
1301        (float)info->nFoundEssentials + (float)depth) /
1302        (float)(info->nFoundEssentials + 1);
1303      if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth)
1304        info->topFoundEssentialDepth = depth;
1305      if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
1306        info->foundEssentials[depth]++;
1307      info->nFoundEssentials++;
1308      tmpImg = ImgVectorMinimize(info, delta, essentialCube, image,
1309                        NIL(array_t), &tmpDelta, NIL(mdd_t *),
1310                        NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *));
1311      foundEssentialDepth = depth;
1312    } else {
1313      tmpDelta = delta;
1314      tmpImg = image;
1315      foundEssentialDepth = info->option->maxEssentialDepth;
1316    }
1317    mdd_free(essentialCube);
1318    foundEssentialDepthT = info->option->maxEssentialDepth;
1319    foundEssentialDepthE = info->option->maxEssentialDepth;
1320  } else {
1321    tmpDelta = delta;
1322    tmpImg = image;
1323    /* To remove compiler warnings */
1324    foundEssentialDepth = -1;
1325    foundEssentialDepthT = -1;
1326    foundEssentialDepthE = -1;
1327  }
1328
1329  if (info->option->preCanonical) {
1330    newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg, NIL(array_t),
1331                                &newDelta, NIL(array_t *), NIL(mdd_t *),
1332                                NIL(mdd_t *));
1333  } else {
1334    newImg = tmpImg;
1335    newDelta = tmpDelta;
1336  }
1337  if (tmpDelta != delta)
1338    ImgVectorFree(tmpDelta);
1339  if (tmpImg != image)
1340    mdd_free(tmpImg);
1341
1342  if (bdd_is_tautology(newImg, 1) || bdd_is_tautology(newImg, 0)) {
1343    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1344                                (float)depth) / (float)(info->nLeavesB + 1);
1345    if (depth > info->maxDepthB)
1346      info->maxDepthB = depth;
1347    info->nLeavesB++;
1348    if (info->option->debug) {
1349      refResult = ImgPreImageByHybrid(info, newDelta, newImg);
1350      tmp = refResult;
1351      refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
1352      mdd_free(tmp);
1353      tmp = mdd_and(newImg, info->debugCareSet, 1, 1);
1354      assert(mdd_equal_mod_care_set_array(refResult, tmp,
1355                                          info->toCareSetArray));
1356      mdd_free(refResult);
1357      mdd_free(tmp);
1358    }
1359    ImgVectorFree(newDelta);
1360    if (findEssential)
1361      info->foundEssentialDepth = foundEssentialDepth;
1362    return(newImg);
1363  }
1364
1365  if (info->preCache) {
1366    preImg = ImgCacheLookupTable(info, info->preCache, newDelta, newImg);
1367    if (preImg) {
1368      info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1369                                (float)depth) / (float)(info->nLeavesB + 1);
1370      if (depth > info->maxDepthB)
1371        info->maxDepthB = depth;
1372      info->nLeavesB++;
1373      if (info->option->debug) {
1374        refResult = ImgPreImageByHybrid(info, newDelta, newImg);
1375        tmp = refResult;
1376        refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
1377        mdd_free(tmp);
1378        tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
1379        assert(mdd_equal_mod_care_set_array(refResult, tmp,
1380                                            info->toCareSetArray));
1381        mdd_free(refResult);
1382        mdd_free(tmp);
1383      }
1384      ImgVectorFree(newDelta);
1385      mdd_free(newImg);
1386      if (findEssential)
1387        info->foundEssentialDepth = foundEssentialDepth;
1388      return(preImg);
1389    }
1390  }
1391
1392  if (depth == turnDepth) {
1393    preImg = ImgPreImageByHybrid(info, newDelta, newImg);
1394    if (info->option->debug) {
1395      refResult = ImgPreImageByHybrid(info, newDelta, newImg);
1396      tmp = refResult;
1397      refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
1398      mdd_free(tmp);
1399      tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
1400      assert(mdd_equal_mod_care_set_array(refResult, tmp,
1401                                          info->toCareSetArray));
1402      mdd_free(refResult);
1403      mdd_free(tmp);
1404    }
1405    if (info->preCache)
1406      ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
1407    else {
1408      ImgVectorFree(newDelta);
1409      mdd_free(newImg);
1410    }
1411    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1412                                (float)depth) / (float)(info->nLeavesB + 1);
1413    if (depth > info->maxDepthB)
1414      info->maxDepthB = depth;
1415    info->nLeavesB++;
1416    info->nTurnsB++;
1417    if (findEssential)
1418      info->foundEssentialDepth = foundEssentialDepth;
1419    return(preImg);
1420  }
1421
1422  split = PreImageChooseSplitVar(info, newDelta, newImg,
1423                                 1, info->option->preOutputSplit);
1424  comp = array_fetch(ImgComponent_t *, newDelta, split);
1425  var = mdd_dup(comp->var);
1426  varNot = mdd_not(var);
1427  imgE = bdd_cofactor(newImg, varNot);
1428  mdd_free(varNot);
1429  imgT = bdd_cofactor(newImg, var);
1430  mdd_free(var);
1431  if (!info->preCache && !info->option->debug)
1432    mdd_free(newImg);
1433  c = PreImageDeleteOneComponent(info, newDelta, split, &vector);
1434  if (!info->preCache && !info->option->debug)
1435    ImgVectorFree(newDelta);
1436
1437  nRecur = 0;
1438  if (bdd_is_tautology(imgT, 1))
1439    preImgT = mdd_one(info->manager);
1440  else if (bdd_is_tautology(imgT, 0))
1441    preImgT = mdd_zero(info->manager);
1442  else {
1443    if (info->option->debug) {
1444      saveCareSet = info->debugCareSet;
1445      info->debugCareSet = mdd_and(saveCareSet, c, 1, 1);
1446    }
1447    preImgT = PreImageByConstraintCofactoring(info, vector, imgT, splitMethod,
1448                                                turnDepth, depth + 1);
1449    if (info->option->debug) {
1450      mdd_free(info->debugCareSet);
1451      info->debugCareSet = saveCareSet;
1452    }
1453    if (findEssential)
1454      foundEssentialDepthT = info->foundEssentialDepth;
1455    nRecur++;
1456  }
1457  mdd_free(imgT);
1458  if (bdd_is_tautology(imgE, 1))
1459    preImgE = mdd_one(info->manager);
1460  else if (bdd_is_tautology(imgE, 0))
1461    preImgE = mdd_zero(info->manager);
1462  else {
1463    if (info->option->debug) {
1464      saveCareSet = info->debugCareSet;
1465      info->debugCareSet = mdd_and(saveCareSet, c, 1, 0);
1466    }
1467    preImgE = PreImageByConstraintCofactoring(info, vector, imgE, splitMethod,
1468                                                turnDepth, depth + 1);
1469    if (info->option->debug) {
1470      mdd_free(info->debugCareSet);
1471      info->debugCareSet = saveCareSet;
1472    }
1473    if (findEssential)
1474      foundEssentialDepthE = info->foundEssentialDepth;
1475    nRecur++;
1476  }
1477  mdd_free(imgE);
1478  ImgVectorFree(vector);
1479  preImg = bdd_ite(c, preImgT, preImgE, 1, 1, 1);
1480  if (info->option->verbosity) {
1481    size = bdd_size(preImg);
1482    if (size > info->maxIntermediateSize)
1483      info->maxIntermediateSize = size;
1484    if (info->option->printBddSize) {
1485      fprintf(vis_stdout, "** tfm info: bdd_ite(%d,%d,%d) = %d\n",
1486              bdd_size(c), bdd_size(preImgT), bdd_size(preImgE),
1487              bdd_size(preImg));
1488    }
1489  }
1490  mdd_free(c);
1491  mdd_free(preImgT);
1492  mdd_free(preImgE);
1493
1494  if (info->preCache)
1495    ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg));
1496
1497  if (info->option->debug) {
1498    refResult = ImgPreImageByHybrid(info, newDelta, newImg);
1499    tmp = refResult;
1500    refResult = mdd_and(tmp, info->debugCareSet, 1, 1);
1501    mdd_free(tmp);
1502    tmp = mdd_and(preImg, info->debugCareSet, 1, 1);
1503    assert(mdd_equal_mod_care_set_array(refResult, tmp,
1504                                        info->toCareSetArray));
1505    mdd_free(refResult);
1506    mdd_free(tmp);
1507    if (!info->preCache) {
1508      ImgVectorFree(newDelta);
1509      mdd_free(newImg);
1510    }
1511  }
1512
1513  if (nRecur == 0) {
1514    info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB +
1515                                (float)depth) / (float)(info->nLeavesB + 1);
1516    if (depth > info->maxDepthB)
1517      info->maxDepthB = depth;
1518    info->nLeavesB++;
1519  }
1520
1521  if (findEssential) {
1522    if (foundEssentialDepth == info->option->maxEssentialDepth) {
1523      if (foundEssentialDepthT < foundEssentialDepthE)
1524        foundEssentialDepth = foundEssentialDepthT;
1525      else
1526        foundEssentialDepth = foundEssentialDepthE;
1527    }
1528    info->foundEssentialDepth = foundEssentialDepth;
1529  }
1530  return(preImg);
1531}
1532
1533
1534/**Function********************************************************************
1535
1536  Synopsis    [Computes a preimage by Filkorn's substitution.]
1537
1538  Description [Computes a preimage by Filkorn's substitution.]
1539
1540  SideEffects []
1541
1542******************************************************************************/
1543static mdd_t *
1544PreImageBySubstitution(ImgTfmInfo_t *info, array_t *vector, mdd_t *from)
1545{
1546  int                   i, index;
1547  ImgComponent_t        *comp, *fromComp;
1548  array_t               *varArray, *funcArray;
1549  mdd_t                 *result;
1550
1551  if (bdd_is_tautology(from, 1))
1552    return(mdd_one(info->manager));
1553  else if (bdd_is_tautology(from, 0))
1554    return(mdd_zero(info->manager));
1555
1556  fromComp = ImgComponentAlloc(info);
1557  fromComp->func = from;
1558  ImgComponentGetSupport(fromComp);
1559
1560  varArray = array_alloc(mdd_t *, 0);
1561  funcArray = array_alloc(mdd_t *, 0);
1562
1563  for (i = 0; i < array_n(vector); i++) {
1564    comp = array_fetch(ImgComponent_t *, vector, i);
1565    index = bdd_top_var_id(comp->var);
1566    if (fromComp->support[index] || comp->intermediate) {
1567      array_insert_last(mdd_t *, varArray, comp->var);
1568      array_insert_last(mdd_t *, funcArray, comp->func);
1569    }
1570  }
1571
1572  fromComp->func = NIL(mdd_t);
1573  ImgComponentFree(fromComp);
1574
1575  result = bdd_vector_compose(from, varArray, funcArray);
1576  array_free(varArray);
1577  array_free(funcArray);
1578
1579  /* quantify all primary inputs */
1580  if (info->preKeepPiInTr == FALSE) {
1581    array_t *quantifyVarBddArray;
1582    mdd_t *tmp;
1583
1584    if (info->newQuantifyBddVars)
1585      quantifyVarBddArray = info->newQuantifyBddVars;
1586    else
1587      quantifyVarBddArray = info->quantifyVarBddArray;
1588
1589    tmp = result;
1590    result = bdd_smooth(tmp, quantifyVarBddArray);
1591    mdd_free(tmp);
1592  }
1593
1594  return(result);
1595}
1596
1597
1598/**Function********************************************************************
1599
1600  Synopsis    [Makes a vector canonical for preimage.]
1601
1602  Description [Makes a vector canonical for preimage.
1603  Delete all the components which doesn't appear as a support
1604  in the image. If a component is constant, simplify the image with the
1605  constant value and delete the corresponding component from delta
1606  Side effect on delta.  Return new image.]
1607
1608  SideEffects []
1609
1610******************************************************************************/
1611static bdd_t *
1612PreImageMakeVectorCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image,
1613                            array_t *relationArray, array_t **newVector,
1614                            array_t **newRelationArray,
1615                            mdd_t **cofactorCube, mdd_t **abstractCube)
1616{
1617  array_t               *tmpVector, *cofactoredVector;
1618  bdd_t                 *simple, *tmp, *newImage;
1619  ImgComponent_t        *comp, *comp1, *imgComp;
1620  int                   i, id, n, pos;
1621  st_table              *equivTable;
1622  int                   *ptr, *regularPtr;
1623  mdd_t                 *var, *cofactor, *abstract, *nsVar;
1624  array_t               *tmpRelationArray;
1625  int                   changed = 0;
1626
1627  newImage = mdd_dup(image);
1628
1629  imgComp = ImgComponentAlloc(info);
1630  imgComp->func = image;
1631  ImgComponentGetSupport(imgComp);
1632
1633  if (relationArray) {
1634    cofactor = mdd_one(info->manager);
1635    abstract = mdd_one(info->manager);
1636  } else {
1637    cofactor = NIL(mdd_t);
1638    abstract = NIL(mdd_t);
1639  }
1640
1641  if (info->nIntermediateVars) {
1642    mdd_t       *tmpCofactor, *tmpAbstract;
1643    mdd_t       *constIntermediate;
1644
1645    if (ImgExistConstIntermediateVar(vector)) {
1646      constIntermediate = mdd_one(info->manager);
1647      for (i = 0; i < array_n(vector); i++) {
1648        comp = array_fetch(ImgComponent_t *, vector, i);
1649        if (comp->intermediate) {
1650          if (mdd_is_tautology(comp->func, 1)) {
1651            tmp = constIntermediate;
1652            constIntermediate = mdd_and(tmp, comp->var, 1, 1);
1653            mdd_free(tmp);
1654          } else if (mdd_is_tautology(comp->func, 0)) {
1655            tmp = constIntermediate;
1656            constIntermediate = mdd_and(tmp, comp->var, 1, 0);
1657            mdd_free(tmp);
1658          }
1659        }
1660      }
1661      if (relationArray) {
1662        cofactoredVector = ImgComposeConstIntermediateVars(info, vector,
1663                                                  constIntermediate,
1664                                                  &tmpCofactor, &tmpAbstract,
1665                                                  NIL(mdd_t *), &newImage);
1666
1667        if (!bdd_is_tautology(tmpCofactor, 1)) {
1668          tmp = cofactor;
1669          cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
1670          mdd_free(tmp);
1671        }
1672        mdd_free(tmpCofactor);
1673        if (!bdd_is_tautology(tmpAbstract, 1)) {
1674          tmp = abstract;
1675          abstract = mdd_and(tmp, tmpAbstract, 1, 1);
1676          mdd_free(tmp);
1677        }
1678        mdd_free(tmpAbstract);
1679      } else {
1680        cofactoredVector = ImgComposeConstIntermediateVars(info, vector,
1681                                                  constIntermediate,
1682                                                  NIL(mdd_t *), NIL(mdd_t *),
1683                                                  NIL(mdd_t *), &newImage);
1684      }
1685      mdd_free(constIntermediate);
1686    } else
1687      cofactoredVector = vector;
1688  } else
1689    cofactoredVector = vector;
1690
1691  /* Simplify image -- canonicalize the image first */
1692  n = 0;
1693  equivTable = st_init_table(st_ptrcmp, st_ptrhash);
1694  tmpVector = array_alloc(ImgComponent_t *, 0);
1695  for (i = 0; i < array_n(cofactoredVector); i++) {
1696    comp = array_fetch(ImgComponent_t *, cofactoredVector, i);
1697    if (comp->intermediate) {
1698      comp1 = ImgComponentCopy(info, comp);
1699      array_insert_last(ImgComponent_t *, tmpVector, comp1);
1700      n++;
1701      continue;
1702    }
1703    id = (int)bdd_top_var_id(comp->var);
1704    if (!imgComp->support[id]) {
1705      if (abstract) {
1706        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1707        tmp = abstract;
1708        abstract = mdd_and(tmp, nsVar, 1, 1);
1709        mdd_free(tmp);
1710        mdd_free(nsVar);
1711      }
1712      continue;
1713    }
1714    if (mdd_is_tautology(comp->func, 1)) {
1715      changed = 1;
1716      simple = bdd_cofactor(newImage, comp->var);
1717      mdd_free(newImage);
1718      newImage = simple;
1719      if (abstract) {
1720        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1721        tmp = abstract;
1722        abstract = mdd_and(tmp, nsVar, 1, 1);
1723        mdd_free(tmp);
1724        mdd_free(nsVar);
1725      }
1726    } else if (mdd_is_tautology(comp->func, 0)) {
1727      changed = 1;
1728      tmp = mdd_not(comp->var);
1729      simple = bdd_cofactor(newImage, tmp);
1730      mdd_free(tmp);
1731      mdd_free(newImage);
1732      newImage = simple;
1733      if (abstract) {
1734        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1735        tmp = abstract;
1736        abstract = mdd_and(tmp, nsVar, 1, 1);
1737        mdd_free(tmp);
1738        mdd_free(nsVar);
1739      }
1740    } else {
1741      ptr = (int *)bdd_pointer(comp->func);
1742      regularPtr = (int *)((unsigned long)ptr & ~01);
1743      if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
1744        changed = 1;
1745        comp1 = array_fetch(ImgComponent_t *, tmpVector, pos);
1746        if (mdd_equal(comp->func, comp1->func)) {
1747          tmp = newImage;
1748          newImage = bdd_compose(tmp, comp->var, comp1->var);
1749          mdd_free(tmp);
1750        } else {
1751          tmp = newImage;
1752          var = mdd_not(comp1->var);
1753          newImage = bdd_compose(tmp, comp->var, var);
1754          mdd_free(tmp);
1755          mdd_free(var);
1756        }
1757        if (abstract) {
1758          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1759          tmp = abstract;
1760          abstract = mdd_and(tmp, nsVar, 1, 1);
1761          mdd_free(tmp);
1762          mdd_free(nsVar);
1763        }
1764      } else {
1765        comp1 = ImgComponentCopy(info, comp);
1766        array_insert_last(ImgComponent_t *, tmpVector, comp1);
1767        st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
1768        n++;
1769      }
1770    }
1771  }
1772  st_free_table(equivTable);
1773  if (cofactoredVector && cofactoredVector != vector)
1774    ImgVectorFree(cofactoredVector);
1775
1776  if (changed) {
1777    /* Now Simplify delta by deleting the non-affecting components */
1778    *newVector = array_alloc(ImgComponent_t *, 0);
1779
1780    imgComp->func = NIL(mdd_t);
1781    ImgComponentFree(imgComp);
1782
1783    imgComp = ImgComponentAlloc(info);
1784    imgComp->func = newImage;
1785    ImgSupportClear(info, imgComp->support);
1786    ImgComponentGetSupport(imgComp);
1787    for (i = 0; i < array_n(tmpVector); i++) {
1788      comp = array_fetch(ImgComponent_t *, tmpVector, i);
1789      id = (int)bdd_top_var_id(comp->var);
1790      if (imgComp->support[id] || comp->intermediate)
1791        array_insert_last(ImgComponent_t *, *newVector, comp);
1792      else {
1793        if (abstract) {
1794          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1795          tmp = abstract;
1796          abstract = mdd_and(tmp, nsVar, 1, 1);
1797          mdd_free(tmp);
1798          mdd_free(nsVar);
1799        }
1800        ImgComponentFree(comp);
1801      }
1802    }
1803    array_free(tmpVector);
1804  } else
1805    *newVector = tmpVector;
1806
1807  imgComp->func = NIL(mdd_t);
1808  ImgComponentFree(imgComp);
1809
1810  if (newRelationArray)
1811    *newRelationArray = relationArray;
1812  if (cofactor) {
1813    if (cofactorCube)
1814      *cofactorCube = cofactor;
1815    else {
1816      if (!bdd_is_tautology(cofactor, 1)) {
1817        tmpRelationArray = *newRelationArray;
1818        *newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray,
1819                                                          cofactor);
1820        if (tmpRelationArray != relationArray)
1821          mdd_array_free(tmpRelationArray);
1822      }
1823      mdd_free(cofactor);
1824    }
1825  }
1826  if (abstract) {
1827    if (abstractCube)
1828      *abstractCube = abstract;
1829    else {
1830      if (bdd_is_tautology(abstract, 1))
1831        mdd_free(abstract);
1832      else {
1833        tmpRelationArray = *newRelationArray;
1834        *newRelationArray = ImgGetAbstractedRelationArray(info->manager,
1835                                                          tmpRelationArray,
1836                                                          abstract);
1837        mdd_free(abstract);
1838        if (tmpRelationArray != relationArray)
1839          mdd_array_free(tmpRelationArray);
1840      }
1841    }
1842  }
1843  assert(CheckPreImageVector(info, *newVector, newImage));
1844  return(newImage);
1845}
1846
1847
1848/**Function********************************************************************
1849
1850  Synopsis    [Makes transition relation canonical for preimage.]
1851
1852  Description [Makes transition relation canonical for preimage.
1853  Quantifies out the next state variables that do not occur in the image,
1854  and when a vector exists, delete the components which do not appear
1855  in the image. If a component is constant, simplify the image with the
1856  constant value and delete the corresponding component from delta
1857  Side effect on delta.  Return new image.]
1858
1859  SideEffects []
1860
1861******************************************************************************/
1862static bdd_t *
1863PreImageMakeRelationCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image,
1864                              array_t *relationArray, array_t **newVector,
1865                              array_t **newRelationArray)
1866{
1867  array_t               *tmpVector, *cofactoredVector;
1868  bdd_t                 *simple, *tmp, *newImage;
1869  ImgComponent_t        *comp, *comp1, *imgComp;
1870  int                   i, j, id;
1871  mdd_t                 *cofactor, *abstract, *var, *nsVar;
1872  array_t               *tmpRelationArray;
1873  int                   changed = 0;
1874  mdd_t                 *yVarsCube, *rangeCube, *relation, *tmp2;
1875  array_t               *supportIds;
1876
1877  imgComp = ImgComponentAlloc(info);
1878  imgComp->func = image;
1879  ImgComponentGetSupport(imgComp);
1880
1881  if (vector) {
1882    newImage = mdd_dup(image);
1883    cofactor = mdd_one(info->manager);
1884    abstract = mdd_one(info->manager);
1885
1886    if (info->nIntermediateVars) {
1887      mdd_t     *tmpCofactor, *tmpAbstract;
1888      mdd_t     *constIntermediate;
1889
1890      if (ImgExistConstIntermediateVar(vector)) {
1891        constIntermediate = mdd_one(info->manager);
1892
1893        for (i = 0; i < array_n(vector); i++) {
1894          comp = array_fetch(ImgComponent_t *, vector, i);
1895          if (comp->intermediate) {
1896            if (mdd_is_tautology(comp->func, 1)) {
1897              tmp = constIntermediate;
1898              constIntermediate = mdd_and(tmp, comp->var, 1, 1);
1899              mdd_free(tmp);
1900            } else if (mdd_is_tautology(comp->func, 0)) {
1901              tmp = constIntermediate;
1902              constIntermediate = mdd_and(tmp, comp->var, 1, 0);
1903              mdd_free(tmp);
1904            }
1905          }
1906        }
1907
1908        cofactoredVector = ImgComposeConstIntermediateVars(info, vector,
1909                                                           constIntermediate,
1910                                                           &tmpCofactor,
1911                                                           &tmpAbstract,
1912                                                           NIL(mdd_t *),
1913                                                           &newImage);
1914
1915        if (!bdd_is_tautology(tmpCofactor, 1)) {
1916          tmp = cofactor;
1917          cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
1918          mdd_free(tmp);
1919        }
1920        mdd_free(tmpCofactor);
1921        if (!bdd_is_tautology(tmpAbstract, 1)) {
1922          tmp = abstract;
1923          abstract = mdd_and(tmp, tmpAbstract, 1, 1);
1924          mdd_free(tmp);
1925        }
1926        mdd_free(tmpAbstract);
1927        mdd_free(constIntermediate);
1928      } else
1929        cofactoredVector = vector;
1930    } else
1931      cofactoredVector = vector;
1932
1933    /* Simplify image -- canonicalize vector */
1934    tmpVector = array_alloc(ImgComponent_t *, 0);
1935    for (i = 0; i < array_n(cofactoredVector); i++) {
1936      comp = array_fetch(ImgComponent_t *, cofactoredVector, i);
1937      if (comp->intermediate) {
1938        comp1 = ImgComponentCopy(info, comp);
1939        array_insert_last(ImgComponent_t *, tmpVector, comp1);
1940        continue;
1941      }
1942      id = (int)bdd_top_var_id(comp->var);
1943      if (!imgComp->support[id]) {
1944        if (abstract) {
1945          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1946          tmp = abstract;
1947          abstract = mdd_and(tmp, nsVar, 1, 1);
1948          mdd_free(tmp);
1949          mdd_free(nsVar);
1950        }
1951        continue;
1952      }
1953      if (mdd_is_tautology(comp->func, 1)) {
1954        changed = 1;
1955        simple = bdd_cofactor(newImage, comp->var);
1956        mdd_free(newImage);
1957        newImage = simple;
1958        if (abstract) {
1959          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1960          tmp = abstract;
1961          abstract = mdd_and(tmp, nsVar, 1, 1);
1962          mdd_free(tmp);
1963          mdd_free(nsVar);
1964        }
1965      } else if (mdd_is_tautology(comp->func, 0)) {
1966        changed = 1;
1967        tmp = mdd_not(comp->var);
1968        simple = bdd_cofactor(newImage, tmp);
1969        mdd_free(tmp);
1970        mdd_free(newImage);
1971        newImage = simple;
1972        if (abstract) {
1973          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1974          tmp = abstract;
1975          abstract = mdd_and(tmp, nsVar, 1, 1);
1976          mdd_free(tmp);
1977          mdd_free(nsVar);
1978        }
1979      } else {
1980        comp1 = ImgComponentCopy(info, comp);
1981        array_insert_last(ImgComponent_t *, tmpVector, comp1);
1982      }
1983    }
1984    if (cofactoredVector && cofactoredVector != vector)
1985      ImgVectorFree(cofactoredVector);
1986
1987    if (changed) {
1988      /* Now Simplify delta by deleting the non-affecting components */
1989      *newVector = array_alloc(ImgComponent_t *, 0);
1990
1991      imgComp->func = NIL(mdd_t);
1992      ImgComponentFree(imgComp);
1993
1994      imgComp = ImgComponentAlloc(info);
1995      imgComp->func = newImage;
1996      ImgSupportClear(info, imgComp->support);
1997      ImgComponentGetSupport(imgComp);
1998      for (i = 0; i < array_n(tmpVector); i++) {
1999        comp = array_fetch(ImgComponent_t *, tmpVector, i);
2000        id = (int)bdd_top_var_id(comp->var);
2001        if (imgComp->support[id] || comp->intermediate)
2002          array_insert_last(ImgComponent_t *, *newVector, comp);
2003        else {
2004          if (abstract) {
2005            nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
2006            tmp = abstract;
2007            abstract = mdd_and(tmp, nsVar, 1, 1);
2008            mdd_free(tmp);
2009            mdd_free(nsVar);
2010          }
2011          ImgComponentFree(comp);
2012        }
2013      }
2014      array_free(tmpVector);
2015    } else
2016      *newVector = tmpVector;
2017  } else {
2018    newImage = image;
2019    *newVector = vector;
2020    cofactor = NIL(mdd_t);
2021    abstract = NIL(mdd_t);
2022  }
2023
2024  yVarsCube = mdd_one(info->manager);
2025  for (i = 0; i < info->nVars; i++) {
2026    if (imgComp->support[i]) {
2027      imgComp->support[i] = 0;
2028      if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
2029        continue;
2030      if (info->intermediateVarsTable &&
2031          st_lookup(info->intermediateVarsTable, (char *)(long)i,
2032                    NIL(char *))) {
2033        continue;
2034      }
2035      var = bdd_var_with_index(info->manager, i);
2036      nsVar = ImgSubstitute(var, info->functionData, Img_D2R_c);
2037      mdd_free(var);
2038      id = (int)bdd_top_var_id(nsVar);
2039      imgComp->support[id] = 1;
2040      tmp = yVarsCube;
2041      yVarsCube = mdd_and(tmp, nsVar, 1, 1);
2042      mdd_free(tmp);
2043      mdd_free(nsVar);
2044    }
2045  }
2046
2047  if (vector) {
2048    for (i = 0; i < array_n(*newVector); i++) {
2049      comp = array_fetch(ImgComponent_t *, *newVector, i);
2050      nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
2051      id = (int)bdd_top_var_id(nsVar);
2052      imgComp->support[id] = 2;
2053      mdd_free(nsVar);
2054    }
2055  }
2056
2057  for (i = 0; i < array_n(relationArray); i++) {
2058    relation = array_fetch(mdd_t *, relationArray, i);
2059    supportIds = mdd_get_bdd_support_ids(info->manager, relation);
2060    for (j = 0; j < array_n(supportIds); j++) {
2061      id = array_fetch(int, supportIds, j);
2062      imgComp->support[id] = 2;
2063    }
2064    array_free(supportIds);
2065  }
2066
2067  for (i = 0; i < info->nVars; i++) {
2068    if (imgComp->support[i] == 1) {
2069      nsVar = bdd_var_with_index(info->manager, i);
2070      var = ImgSubstitute(nsVar, info->functionData, Img_R2D_c);
2071      mdd_free(nsVar);
2072      tmp = newImage;
2073      newImage = bdd_smooth_with_cube(tmp, var);
2074      if (tmp != image)
2075        mdd_free(tmp);
2076      mdd_free(var);
2077    }
2078  }
2079
2080  imgComp->func = NIL(mdd_t);
2081  ImgComponentFree(imgComp);
2082
2083  if (bdd_get_package_name() == CUDD)
2084    rangeCube = info->functionData->rangeCube;
2085  else {
2086    rangeCube = mdd_one(info->manager);
2087    for (i = 0; i < array_n(info->functionData->rangeBddVars); i++) {
2088      var = array_fetch(mdd_t *, info->functionData->rangeBddVars, i);
2089      tmp = rangeCube;
2090      rangeCube = mdd_and(tmp, var, 1, 1);
2091      mdd_free(tmp);
2092    }
2093  }
2094
2095  cofactor = NIL(mdd_t);
2096  if (abstract) {
2097    tmp2 = bdd_smooth_with_cube(rangeCube, yVarsCube);
2098    tmp = abstract;
2099    abstract = mdd_and(tmp, tmp2, 1, 1);
2100    mdd_free(tmp);
2101    mdd_free(tmp2);
2102  } else
2103    abstract = bdd_smooth_with_cube(rangeCube, yVarsCube);
2104  mdd_free(yVarsCube);
2105  if (rangeCube != info->functionData->rangeCube)
2106    mdd_free(rangeCube);
2107
2108  *newRelationArray = relationArray;
2109  if (cofactor) {
2110    if (!bdd_is_tautology(cofactor, 1)) {
2111      tmpRelationArray = *newRelationArray;
2112      *newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray,
2113                                                        cofactor);
2114      if (tmpRelationArray != relationArray)
2115        mdd_array_free(tmpRelationArray);
2116    }
2117    mdd_free(cofactor);
2118  }
2119  if (bdd_is_tautology(abstract, 1))
2120    mdd_free(abstract);
2121  else {
2122    tmpRelationArray = *newRelationArray;
2123    *newRelationArray = ImgGetAbstractedRelationArray(info->manager,
2124                                                      tmpRelationArray,
2125                                                      abstract);
2126    mdd_free(abstract);
2127    if (tmpRelationArray != relationArray)
2128      mdd_array_free(tmpRelationArray);
2129  }
2130  return(newImage);
2131}
2132
2133
2134/**Function********************************************************************
2135
2136  Synopsis    [Deletes a component in a vector.]
2137
2138  Description [Deletes a component in a vector. Deletes index-th component
2139  out of delta and copy it into newDelta.]
2140
2141  SideEffects []
2142
2143******************************************************************************/
2144static bdd_t *
2145PreImageDeleteOneComponent(ImgTfmInfo_t *info, array_t *delta, int index,
2146                           array_t **newDelta)
2147{
2148  int                   i;
2149  ImgComponent_t        *comp, *tmpComp;
2150  bdd_t                 *func, *newFunc;
2151  int                   preMinimize = info->option->preMinimize;
2152
2153  assert(array_n(delta) > 0);
2154
2155  comp = array_fetch(ImgComponent_t *, delta, index);
2156  func = mdd_dup(comp->func);
2157
2158  *newDelta = array_alloc(ImgComponent_t *, 0);
2159  for (i = 0; i < array_n(delta); i++) {
2160    if (i != index) {
2161      comp = array_fetch(ImgComponent_t *, delta, i);
2162      tmpComp = ImgComponentCopy(info, comp);
2163      if (preMinimize) {
2164        newFunc = bdd_minimize(tmpComp->func, func);
2165        if (mdd_equal(newFunc, tmpComp->func))
2166          mdd_free(newFunc);
2167        else {
2168          mdd_free(tmpComp->func);
2169          tmpComp->func = newFunc;
2170          ImgSupportClear(info, tmpComp->support);
2171          ImgComponentGetSupport(tmpComp);
2172        }
2173      }
2174      array_insert_last(ImgComponent_t *, (*newDelta), tmpComp);
2175    }
2176  }
2177
2178  return(func);
2179}
2180
2181
2182/**Function********************************************************************
2183
2184  Synopsis    [Chooses a splitting variable for preimage.]
2185
2186  Description [Chooses a splitting variable for preimage.]
2187
2188  SideEffects []
2189
2190******************************************************************************/
2191static int
2192PreImageChooseSplitVar(ImgTfmInfo_t *info, array_t *delta, bdd_t *img,
2193                        int splitMethod, int split)
2194{
2195  ImgComponent_t        *comp, *imgComp;
2196  int                   i, j, bestCost, newCost;
2197  int                   index, bestVar, bestComp;
2198  int                   nFuncs, nVars, bestOccur = 0;
2199  int                   *varOccur, *varCost;
2200  mdd_t                 *var, *varNot, *pcFunc, *ncFunc;
2201  int                   tieCount = 0;
2202
2203  assert(array_n(delta) > 0);
2204
2205  if (splitMethod == 0) {
2206    bestVar = -1;
2207    bestComp = -1;
2208    nFuncs = array_n(delta);
2209    nVars = info->nVars;
2210    varOccur = ALLOC(int, nVars);
2211    memset(varOccur, 0, sizeof(int) * nVars);
2212    varCost = NIL(int);
2213    for (i = 0; i < nFuncs; i++) {
2214      comp = array_fetch(ImgComponent_t *, delta, i);
2215      for (j = 0; j < nVars; j++) {
2216        if (comp->support[j])
2217          varOccur[j]++;
2218      }
2219    }
2220    switch (split) {
2221    case 0: /* largest support */
2222      for (i = 0; i < nVars; i++) {
2223        if (varOccur[i] == 0)
2224          continue;
2225        if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
2226          continue;
2227        if (info->intermediateVarsTable &&
2228            st_lookup(info->intermediateVarsTable, (char *)(long)i,
2229                        NIL(char *))) {
2230          continue;
2231        }
2232        if (bestVar == -1 || varOccur[i] > bestOccur) {
2233          bestVar = i;
2234          bestOccur = varOccur[i];
2235          tieCount = 1;
2236        } else if (varOccur[i] == bestOccur) {
2237          tieCount++;
2238          if (info->option->tieBreakMode == 0 &&
2239              bdd_get_level_from_id(info->manager, i) <
2240              bdd_get_level_from_id(info->manager, bestVar)) {
2241            bestVar = i;
2242          }
2243        }
2244      }
2245
2246      if (info->option->tieBreakMode == 1 && tieCount > 1) {
2247        bestCost = IMG_TF_MAX_INT;
2248        for (i = bestVar; i < nVars; i++) {
2249          if (varOccur[i] != bestOccur)
2250            continue;
2251          if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
2252            continue;
2253          if (info->intermediateVarsTable &&
2254              st_lookup(info->intermediateVarsTable, (char *)(long)i,
2255                        NIL(char *))) {
2256            continue;
2257          }
2258          var = bdd_var_with_index(info->manager, i);
2259          newCost = 0;
2260          for (j = 0; j < array_n(delta); j++) {
2261            comp = array_fetch(ImgComponent_t *, delta, j);
2262            newCost += bdd_estimate_cofactor(comp->func, var, 1);
2263            newCost += bdd_estimate_cofactor(comp->func, var, 0);
2264          }
2265          mdd_free(var);
2266
2267          if (newCost < bestCost) {
2268            bestVar = i;
2269            bestCost = newCost;
2270          } else if (newCost == bestCost) {
2271            if (bdd_get_level_from_id(info->manager, i) <
2272                bdd_get_level_from_id(info->manager, bestVar)) {
2273              bestVar = i;
2274            }
2275          }
2276        }
2277      }
2278      break;
2279    case 1: /* smallest support after splitting */
2280      /* Find the variable which makes the smallest support after splitting */
2281      bestCost = IMG_TF_MAX_INT;
2282      varCost = ALLOC(int, nVars);
2283      memset(varCost, 0, sizeof(int) * nVars);
2284      for (i = 0; i < nVars; i++) {
2285        if (varOccur[i] == 0)
2286          continue;
2287        if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
2288          continue;
2289        if (info->intermediateVarsTable &&
2290            st_lookup(info->intermediateVarsTable, (char *)(long)i,
2291                        NIL(char *))) {
2292          continue;
2293        }
2294        var = bdd_var_with_index(info->manager, i);
2295        varNot = mdd_not(var);
2296        for (j = 0; j < array_n(delta); j++) {
2297          comp = array_fetch(ImgComponent_t *, delta, j);
2298          pcFunc = bdd_cofactor(comp->func, var);
2299          varCost[i] += ImgCountBddSupports(pcFunc);
2300          mdd_free(pcFunc);
2301          ncFunc = bdd_cofactor(comp->func, varNot);
2302          varCost[i] += ImgCountBddSupports(ncFunc);
2303          mdd_free(ncFunc);
2304        }
2305        mdd_free(var);
2306        mdd_free(varNot);
2307
2308        if (varCost[i] < bestCost) {
2309          bestCost = varCost[i];
2310          bestVar = i;
2311        } else if (varCost[i] == bestCost) {
2312          if (varOccur[i] < varOccur[bestVar]) {
2313            bestVar = i;
2314          } else if (varOccur[i] == varOccur[bestVar]) {
2315            if (bdd_get_level_from_id(info->manager, i) <
2316                bdd_get_level_from_id(info->manager, bestVar)) {
2317              bestVar = i;
2318            }
2319          }
2320        }
2321      }
2322      break;
2323    case 2: /* smallest BDD size after splitting */
2324      /* Find the variable which makes the smallest BDDs of all functions
2325         after splitting */
2326      bestCost = IMG_TF_MAX_INT;
2327      varCost = ALLOC(int, nVars);
2328      memset(varCost, 0, sizeof(int) * nVars);
2329      for (i = 0; i < nVars; i++) {
2330        if (varOccur[i] == 0)
2331          continue;
2332        if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
2333          continue;
2334        if (info->intermediateVarsTable &&
2335            st_lookup(info->intermediateVarsTable, (char *)(long)i,
2336                        NIL(char *))) {
2337          continue;
2338        }
2339        var = bdd_var_with_index(info->manager, i);
2340        for (j = 0; j < array_n(delta); j++) {
2341          comp = array_fetch(ImgComponent_t *, delta, j);
2342          varCost[i] += bdd_estimate_cofactor(comp->func, var, 1);
2343          varCost[i] += bdd_estimate_cofactor(comp->func, var, 0);
2344        }
2345        mdd_free(var);
2346
2347        if (varCost[i] < bestCost) {
2348          bestCost = varCost[i];
2349          bestVar = i;
2350        } else if (varCost[i] == bestCost) {
2351          if (varOccur[i] < varOccur[bestVar]) {
2352            bestVar = i;
2353          } else if (varOccur[i] == varOccur[bestVar]) {
2354            if (bdd_get_level_from_id(info->manager, i) <
2355                bdd_get_level_from_id(info->manager, bestVar)) {
2356              bestVar = i;
2357            }
2358          }
2359        }
2360      }
2361      break;
2362    case 3: /* top variable */
2363    default:
2364      for (i = 0; i < nVars; i++) {
2365        if (varOccur[i] == 0)
2366          continue;
2367        if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
2368          continue;
2369        if (info->intermediateVarsTable &&
2370            st_lookup(info->intermediateVarsTable, (char *)(long)i,
2371                        NIL(char *))) {
2372          continue;
2373        }
2374        if (bestVar == -1)
2375          bestVar = i;
2376        else if (bdd_get_level_from_id(info->manager, i) <
2377                 bdd_get_level_from_id(info->manager, bestVar)) {
2378          bestVar = i;
2379        }
2380      }
2381    }
2382    FREE(varOccur);
2383    if (varCost)
2384      FREE(varCost);
2385  } else {
2386    bestComp = -1;
2387    bestVar = -1;
2388    switch (split) {
2389    case 0: /* smallest BDD size */
2390      bestCost = IMG_TF_MAX_INT;
2391      imgComp = ImgComponentAlloc(info);
2392      imgComp->func = img;
2393      ImgComponentGetSupport(imgComp);
2394      for (i = 0; i < array_n(delta); i++) {
2395        comp = array_fetch(ImgComponent_t *, delta, i);
2396        if (comp->intermediate)
2397          continue;
2398        index = (int)bdd_top_var_id(comp->var);
2399        if (imgComp->support[index]) {
2400          newCost = bdd_size(comp->func);
2401          if (newCost < bestCost) {
2402            bestComp = i;
2403            bestCost = newCost;
2404          }
2405        }
2406      }
2407      imgComp->func = NIL(mdd_t);
2408      ImgComponentFree(imgComp);
2409      break;
2410    case 1: /* largest BDD size */
2411      bestCost = 0;
2412      imgComp = ImgComponentAlloc(info);
2413      imgComp->func = img;
2414      ImgComponentGetSupport(imgComp);
2415      for (i = 0; i < array_n(delta); i++) {
2416        comp = array_fetch(ImgComponent_t *, delta, i);
2417        if (comp->intermediate)
2418          continue;
2419        index = (int)bdd_top_var_id(comp->var);
2420        if (imgComp->support[index]) {
2421          newCost = bdd_size(comp->func);
2422          if (newCost > bestCost) {
2423            bestComp = i;
2424            bestCost = newCost;
2425          }
2426        }
2427      }
2428      imgComp->func = NIL(mdd_t);
2429      ImgComponentFree(imgComp);
2430      break;
2431    case 2: /* top variable */
2432    default:
2433      for (i = 0; i < array_n(delta); i++) {
2434        comp = array_fetch(ImgComponent_t *, delta, i);
2435        if (comp->intermediate)
2436          continue;
2437        index = (int)bdd_top_var_id(comp->var);
2438        if (bestComp == -1 ||
2439            bdd_get_level_from_id(info->manager, index) <
2440            bdd_get_level_from_id(info->manager, bestVar)) {
2441          bestVar = index;
2442          bestComp = i;
2443        }
2444      }
2445      break;
2446    }
2447    assert(bestComp != -1);
2448  }
2449
2450  if (splitMethod == 0)
2451    return(bestVar);
2452  else
2453    return(bestComp);
2454}
2455
2456
2457/**Function********************************************************************
2458
2459  Synopsis    [Performs domain cofactoring on a vector and from set with
2460  respect to a variable.]
2461
2462  Description [Performs domain cofactoring on a vector and from set with
2463  respect to a variable.]
2464
2465  SideEffects []
2466
2467******************************************************************************/
2468static mdd_t *
2469DomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from,
2470                  array_t *relationArray, mdd_t *c, array_t **newVector,
2471                  array_t **newRelationArray, mdd_t **cofactorCube,
2472                  mdd_t **abstractCube)
2473{
2474  mdd_t                 *res, *tmp;
2475  ImgComponent_t        *comp, *comp1;
2476  array_t               *vector1;
2477  int                   i, index, n, pos;
2478  mdd_t                 *newFrom, *var, *nsVar;
2479  mdd_t                 *cofactor, *abstract, *constIntermediate;
2480  array_t               *tmpRelationArray;
2481  st_table              *equivTable;
2482  int                   *ptr, *regularPtr;
2483  int                   size;
2484
2485  newFrom = mdd_dup(from);
2486  vector1 = array_alloc(ImgComponent_t *, 0);
2487
2488  if (relationArray) {
2489    cofactor = mdd_one(info->manager);
2490    abstract = mdd_one(info->manager);
2491  } else {
2492    cofactor = NIL(mdd_t);
2493    abstract = NIL(mdd_t);
2494  }
2495
2496  if (info->nIntermediateVars) {
2497    size = ImgVectorFunctionSize(vector);
2498    if (size == array_n(vector))
2499      constIntermediate = NIL(mdd_t);
2500    else
2501      constIntermediate = mdd_one(info->manager);
2502  } else
2503    constIntermediate = NIL(mdd_t);
2504
2505  n = 0;
2506  equivTable = st_init_table(st_ptrcmp, st_ptrhash);
2507  index = (int)bdd_top_var_id(c);
2508  for (i = 0; i < array_n(vector); i++) {
2509    comp = array_fetch(ImgComponent_t *, vector, i);
2510    if (comp->support[index])
2511      res = bdd_cofactor(comp->func, c);
2512    else
2513      res = mdd_dup(comp->func);
2514    if (bdd_is_tautology(res, 1)) {
2515      if (comp->intermediate) {
2516        tmp = constIntermediate;
2517        constIntermediate = mdd_and(tmp, comp->var, 1, 1);
2518        mdd_free(tmp);
2519        mdd_free(res);
2520        continue;
2521      }
2522      tmp = newFrom;
2523      newFrom = bdd_cofactor(tmp, comp->var);
2524      mdd_free(tmp);
2525      mdd_free(res);
2526      if (relationArray) {
2527        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
2528        tmp = abstract;
2529        abstract = mdd_and(tmp, nsVar, 1, 1);
2530        mdd_free(tmp);
2531        mdd_free(nsVar);
2532      }
2533    } else if (bdd_is_tautology(res, 0)) {
2534      if (comp->intermediate) {
2535        tmp = constIntermediate;
2536        constIntermediate = mdd_and(tmp, comp->var, 1, 0);
2537        mdd_free(tmp);
2538        mdd_free(res);
2539        continue;
2540      }
2541      tmp = newFrom;
2542      var = mdd_not(comp->var);
2543      newFrom = bdd_cofactor(tmp, var);
2544      mdd_free(tmp);
2545      mdd_free(var);
2546      mdd_free(res);
2547      if (relationArray) {
2548        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
2549        tmp = abstract;
2550        abstract = mdd_and(tmp, nsVar, 1, 1);
2551        mdd_free(tmp);
2552        mdd_free(nsVar);
2553      }
2554    } else {
2555      if (comp->intermediate) {
2556        comp1 = ImgComponentAlloc(info);
2557        comp1->var = mdd_dup(comp->var);
2558        comp1->func = res;
2559        if (mdd_equal(res, comp->func))
2560          ImgSupportCopy(info, comp1->support, comp->support);
2561        else
2562          ImgComponentGetSupport(comp1);
2563        comp1->intermediate = 1;
2564        array_insert_last(ImgComponent_t *, vector1, comp1);
2565        n++;
2566        continue;
2567      }
2568      ptr = (int *)bdd_pointer(res);
2569      regularPtr = (int *)((unsigned long)ptr & ~01);
2570      if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
2571        comp1 = array_fetch(ImgComponent_t *, vector1, pos);
2572        if (mdd_equal(res, comp1->func)) {
2573          tmp = newFrom;
2574          newFrom = bdd_compose(tmp, comp->var, comp1->var);
2575          mdd_free(tmp);
2576        } else {
2577          tmp = newFrom;
2578          var = mdd_not(comp1->var);
2579          newFrom = bdd_compose(tmp, comp->var, var);
2580          mdd_free(tmp);
2581          mdd_free(var);
2582        }
2583        mdd_free(res);
2584        if (abstract) {
2585          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
2586          tmp = abstract;
2587          abstract = mdd_and(tmp, nsVar, 1, 1);
2588          mdd_free(tmp);
2589          mdd_free(nsVar);
2590        }
2591      } else {
2592        comp1 = ImgComponentAlloc(info);
2593        comp1->var = mdd_dup(comp->var);
2594        comp1->func = res;
2595        if (mdd_equal(res, comp->func))
2596          ImgSupportCopy(info, comp1->support, comp->support);
2597        else
2598          ImgComponentGetSupport(comp1);
2599        array_insert_last(ImgComponent_t *, vector1, comp1);
2600        st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
2601        n++;
2602      }
2603    }
2604  }
2605  st_free_table(equivTable);
2606
2607  if (constIntermediate) {
2608    if (!bdd_is_tautology(constIntermediate, 1)) {
2609      mdd_t     *tmpCofactor, *tmpAbstract;
2610
2611      if (relationArray) {
2612        vector1 = ImgComposeConstIntermediateVars(info, vector1,
2613                                                  constIntermediate,
2614                                                  &tmpCofactor, &tmpAbstract,
2615                                                  NIL(mdd_t *), &newFrom);
2616        if (!bdd_is_tautology(tmpCofactor, 1)) {
2617          tmp = cofactor;
2618          cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
2619          mdd_free(tmp);
2620        }
2621        mdd_free(tmpCofactor);
2622        if (!bdd_is_tautology(tmpAbstract, 1)) {
2623          tmp = abstract;
2624          abstract = mdd_and(tmp, tmpAbstract, 1, 1);
2625          mdd_free(tmp);
2626        }
2627        mdd_free(tmpAbstract);
2628        tmp = cofactor;
2629        cofactor = mdd_and(tmp, constIntermediate, 1, 1);
2630        mdd_free(tmp);
2631      } else {
2632        vector1 = ImgComposeConstIntermediateVars(info, vector1,
2633                                                  constIntermediate,
2634                                                  NIL(mdd_t *), NIL(mdd_t *),
2635                                                  NIL(mdd_t *), &newFrom);
2636      }
2637    }
2638    mdd_free(constIntermediate);
2639  }
2640
2641  *newVector = vector1;
2642
2643  if (relationArray) {
2644    if (newRelationArray)
2645      *newRelationArray = relationArray;
2646    if (cofactorCube && abstractCube) {
2647      if (cofactor) {
2648        if (bdd_is_tautology(cofactor, 1)) {
2649          mdd_free(cofactor);
2650          *cofactorCube = mdd_dup(c);
2651        } else {
2652          *cofactorCube = mdd_and(cofactor, c, 1, 1);
2653          mdd_free(cofactor);
2654        }
2655      }
2656      if (abstract)
2657        *abstractCube = abstract;
2658    } else {
2659      if (bdd_is_tautology(cofactor, 1)) {
2660        *newRelationArray = ImgGetCofactoredRelationArray(relationArray, c);
2661        mdd_free(cofactor);
2662      } else {
2663        tmp = cofactor;
2664        cofactor = mdd_and(tmp, c, 1, 1);
2665        mdd_free(tmp);
2666        *newRelationArray = ImgGetCofactoredRelationArray(relationArray,
2667                                                          cofactor);
2668        mdd_free(cofactor);
2669      }
2670      if (bdd_is_tautology(abstract, 1))
2671        mdd_free(abstract);
2672      else {
2673        tmpRelationArray = *newRelationArray;
2674        *newRelationArray = ImgGetAbstractedRelationArray(info->manager,
2675                                                        tmpRelationArray,
2676                                                        abstract);
2677        mdd_free(abstract);
2678        if (tmpRelationArray != relationArray)
2679          mdd_array_free(tmpRelationArray);
2680      }
2681    }
2682  } else
2683    *newRelationArray = NIL(array_t);
2684
2685  return(newFrom);
2686}
2687
2688
2689/**Function********************************************************************
2690
2691  Synopsis    [Checks sanity of a vector for preimage.]
2692
2693  Description [Checks sanity of a vector for preimage.]
2694
2695  SideEffects []
2696
2697******************************************************************************/
2698static int
2699CheckPreImageVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *image)
2700{
2701  ImgComponent_t        *comp, *imgComp;
2702  int                   i, id, size, status;
2703
2704  status = 1;
2705  if (info->nIntermediateVars)
2706    size = ImgVectorFunctionSize(vector);
2707  else
2708    size = array_n(vector);
2709  if (size != mdd_get_number_of_bdd_support(info->manager, image)) {
2710    fprintf(vis_stderr,
2711            "** tfm error: function vector length is different. (%d != %d)\n",
2712            size, mdd_get_number_of_bdd_support(info->manager, image));
2713    status = 0;
2714  }
2715
2716  imgComp = ImgComponentAlloc(info);
2717  imgComp->func = image;
2718  ImgComponentGetSupport(imgComp);
2719  for (i = 0; i < array_n(vector); i++) {
2720    comp = array_fetch(ImgComponent_t *, vector, i);
2721    id = (int)bdd_top_var_id(comp->var);
2722    if (comp->intermediate)
2723      imgComp->support[id] = 2;
2724    else if (imgComp->support[id] == 0) {
2725      fprintf(vis_stderr,
2726              "** tfm error: variable index[%d] is not in constraint\n", id);
2727      status = 0;
2728    } else
2729      imgComp->support[id] = 2;
2730  }
2731  for (i = 0; i < info->nVars; i++) {
2732    if (imgComp->support[i] == 1) {
2733      fprintf(vis_stderr,
2734            "** tfm error: variable index[%d] is not in function vector\n", i);
2735      status = 0;
2736    }
2737  }
2738  imgComp->func = NIL(mdd_t);
2739  ImgComponentFree(imgComp);
2740  return(status);
2741}
Note: See TracBrowser for help on using the repository browser.