source: vis_dev/vis-2.3/src/img/imgTfmFwd.c @ 83

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

vis2.3
File size: 99.3 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [imgTfmFwd.c]
4
5  PackageName [img]
6
7  Synopsis    [Routines for image computation using transition function method.]
8
9  Description []
10
11  SeeAlso     []
12
13  Author      [In-Ho Moon]
14
15  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado.
16  All rights reserved.
17
18  Permission is hereby granted, without written agreement and without license
19  or royalty fees, to use, copy, modify, and distribute this software and its
20  documentation for any purpose, provided that the above copyright notice and
21  the following two paragraphs appear in all copies of this software.
22
23  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
24  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
25  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
26  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27
28  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
29  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
30  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
31  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
32  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
33
34******************************************************************************/
35#include "imgInt.h"
36
37static char rcsid[] UNUSED = "$Id: imgTfmFwd.c,v 1.37 2005/04/22 19:45:46 jinh Exp $";
38
39/*---------------------------------------------------------------------------*/
40/* Constant declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43/*---------------------------------------------------------------------------*/
44/* Type declarations                                                         */
45/*---------------------------------------------------------------------------*/
46
47/*---------------------------------------------------------------------------*/
48/* Structure declarations                                                    */
49/*---------------------------------------------------------------------------*/
50
51/*---------------------------------------------------------------------------*/
52/* Variable declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Macro declarations                                                        */
57/*---------------------------------------------------------------------------*/
58
59/**AutomaticStart*************************************************************/
60
61/*---------------------------------------------------------------------------*/
62/* Static function prototypes                                                */
63/*---------------------------------------------------------------------------*/
64
65static mdd_t * ImageByInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int splitMethod, int turnDepth, int depth);
66static mdd_t * ImageByStaticInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth);
67static mdd_t * ImageByOutputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, int depth);
68static int ImageDecomposeAndChooseSplitVar(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, int splitMethod, int split, int piSplitFlag, array_t *vectorArray, array_t *varArray, mdd_t **singles, array_t *relationArray, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube);
69static mdd_t * ImageFast2(ImgTfmInfo_t *info, array_t *vector);
70static int FindDecomposableVariable(ImgTfmInfo_t *info, array_t *vector);
71static int TfmCheckImageValidity(ImgTfmInfo_t *info, mdd_t *image);
72static void FindIntermediateSupport(array_t *vector, ImgComponent_t *comp, int nVars, int nGroups, int *stack, char *stackFlag, int *funcGroup, int *size, char *intermediateVarFlag, int *intermediateVarFuncMap);
73static void PrintVectorDecomposition(ImgTfmInfo_t *info, array_t *vectorArray, array_t *varArray);
74static int CheckIfValidSplitOrGetNew(ImgTfmInfo_t *info, int split, array_t *vector, array_t *relationArray, mdd_t *from);
75static int ChooseInputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, int splitMethod, int decompose, int piSplitFlag, int *varOccur);
76static int ChooseOutputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, int splitMethod);
77
78/**AutomaticEnd***************************************************************/
79
80
81/*---------------------------------------------------------------------------*/
82/* Definition of exported functions                                          */
83/*---------------------------------------------------------------------------*/
84
85
86/*---------------------------------------------------------------------------*/
87/* Definition of internal functions                                          */
88/*---------------------------------------------------------------------------*/
89
90
91/**Function********************************************************************
92
93  Synopsis    [Computes an image with transition function method.]
94
95  Description [Computes an image with transition function method.]
96
97  SideEffects []
98
99******************************************************************************/
100mdd_t *
101ImgTfmImage(ImgTfmInfo_t *info, mdd_t *from)
102{
103  mdd_t         *res, *r, *cube, *newFrom, *one;
104  array_t       *newVector, *depVector;
105  int           splitMethod, turnDepth;
106  mdd_t         *refResult;
107  array_t       *relationArray, *newRelationArray, *tmpRelationArray;
108  int           eliminateDepend;
109  int           partial, saveUseConstraint;
110  long          size1, size2;
111  mdd_t         *cofactorCube, *abstractCube;
112  int           i, maxDepth, size, nDependVars;
113
114  info->maxIntermediateSize = 0;
115  if (info->eliminateDepend == 1 ||
116      (info->eliminateDepend == 2 && info->nPrevEliminatedFwd > 0)) {
117    eliminateDepend = 1;
118  } else
119    eliminateDepend = 0;
120
121  saveUseConstraint = info->useConstraint;
122  if (info->buildTR) {
123    if (eliminateDepend == 0 &&
124        info->option->splitMethod == 3 &&
125        info->option->splitMaxDepth < 0 &&
126        info->option->buildPartialTR == FALSE &&
127        info->option->rangeComp == 0 &&
128        info->option->findEssential == FALSE) {
129      r = ImgBddLinearAndSmooth(info->manager, from,
130                      info->fwdClusteredRelationArray,
131                      info->fwdArraySmoothVarBddArray,
132                      info->fwdSmoothVarCubeArray,
133                      info->option->verbosity);
134      res = ImgSubstitute(r, info->functionData, Img_R2D_c);
135      mdd_free(r);
136      return(res);
137    }
138    relationArray = mdd_array_duplicate(info->fwdClusteredRelationArray);
139  } else
140    relationArray = NIL(array_t);
141  if (info->useConstraint == 1 ||
142      (info->useConstraint == 2 &&
143       info->nImageComps == info->option->rangeTryThreshold)) {
144    if (info->buildTR == 2) {
145      newVector = NIL(array_t);
146      cube = mdd_one(info->manager);
147      if (eliminateDepend) {
148        newFrom = ImgTrmEliminateDependVars(info->functionData, relationArray,
149                                            from, NIL(mdd_t *), &nDependVars);
150        if (nDependVars) {
151          if (info->option->verbosity > 0)
152            (void)fprintf(vis_stdout, "Eliminated %d vars.\n", nDependVars);
153          info->averageFoundDependVars = (info->averageFoundDependVars *
154                    (float)info->nFoundDependVars + (float)nDependVars) /
155                    (float)(info->nFoundDependVars + 1);
156          info->nFoundDependVars++;
157        }
158
159        info->nPrevEliminatedFwd = nDependVars;
160      } else
161        newFrom = from;
162      cofactorCube = NIL(mdd_t);
163      abstractCube = NIL(mdd_t);
164    } else {
165      newVector = ImgVectorCopy(info, info->vector);
166      cube = mdd_one(info->manager);
167      if (eliminateDepend) {
168        newFrom = ImgTfmEliminateDependVars(info, newVector, relationArray,
169                                            from, NIL(array_t *), NIL(mdd_t *));
170      } else
171        newFrom = from;
172      if (info->option->delayedSplit && relationArray && info->buildTR != 2) {
173        cofactorCube = mdd_one(info->manager);
174        abstractCube = mdd_one(info->manager);
175      } else {
176        cofactorCube = NIL(mdd_t);
177        abstractCube = NIL(mdd_t);
178      }
179    }
180  } else {
181    if (eliminateDepend) {
182      depVector = ImgVectorCopy(info, info->vector);
183      newFrom = ImgTfmEliminateDependVars(info, depVector, relationArray, from,
184                                          NIL(array_t *), NIL(mdd_t *));
185      /* constrain delta w.r.t. from here */
186      if (info->option->delayedSplit && relationArray && info->buildTR != 2) {
187        ImgVectorConstrain(info, depVector, newFrom, relationArray,
188                           &newVector, &cube, &newRelationArray, &cofactorCube,
189                           &abstractCube, FALSE);
190      } else if (relationArray) {
191        ImgVectorConstrain(info, depVector, newFrom, relationArray,
192                           &newVector, &cube, NIL(array_t *), &cofactorCube,
193                           &abstractCube, FALSE);
194        newRelationArray = NIL(array_t);
195      } else {
196        ImgVectorConstrain(info, depVector, newFrom, NIL(array_t),
197                           &newVector, &cube, NIL(array_t *), NIL(mdd_t *),
198                           NIL(mdd_t *), FALSE);
199        newRelationArray = NIL(array_t);
200        cofactorCube = NIL(mdd_t);
201        abstractCube = NIL(mdd_t);
202      }
203
204      if (info->useConstraint == 2) {
205        size1 = ImgVectorBddSize(depVector);
206        size2 = ImgVectorBddSize(newVector);
207        if (info->option->rangeCheckReorder) {
208          bdd_reorder(info->manager);
209          size1 = ImgVectorBddSize(depVector);
210          size2 = ImgVectorBddSize(newVector);
211        }
212        if (size2 > size1 * info->option->rangeThreshold) { /* cancel */
213          if (info->option->verbosity)
214            fprintf(vis_stdout, "** tfm info: canceled range computation.\n");
215          info->useConstraint = 1;
216          ImgVectorFree(newVector);
217          newVector = depVector;
218          mdd_free(cube);
219          cube = mdd_one(info->manager);
220          if (newRelationArray && newRelationArray != relationArray)
221            mdd_array_free(newRelationArray);
222          if (cofactorCube) {
223            mdd_free(cofactorCube);
224            cofactorCube = mdd_one(info->manager);
225          }
226          if (abstractCube) {
227            mdd_free(abstractCube);
228            abstractCube = mdd_one(info->manager);
229          }
230          info->nImageComps++;
231        } else {
232          info->useConstraint = 0;
233          info->nImageComps = 0;
234          info->nRangeComps++;
235        }
236      }
237      if (info->useConstraint == 0)
238        ImgVectorFree(depVector);
239    } else {
240      newFrom = from;
241      /* constrain delta w.r.t. from here */
242      if (info->option->delayedSplit && relationArray && info->buildTR != 2) {
243        ImgVectorConstrain(info, info->vector, newFrom, relationArray,
244                           &newVector, &cube, &newRelationArray, &cofactorCube,
245                           &abstractCube, FALSE);
246        if (info->option->debug) {
247          refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
248          res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), NIL(mdd_t),
249                                                newRelationArray,
250                                                cofactorCube, abstractCube);
251          assert(mdd_equal(refResult, res));
252          mdd_free(refResult);
253          mdd_free(res);
254        }
255      } else if (relationArray) {
256        ImgVectorConstrain(info, info->vector, newFrom, relationArray,
257                           &newVector, &cube, NIL(array_t *), &cofactorCube,
258                           &abstractCube, FALSE);
259        newRelationArray = NIL(array_t);
260      } else {
261        ImgVectorConstrain(info, info->vector, newFrom, NIL(array_t),
262                           &newVector, &cube, NIL(array_t *), NIL(mdd_t *),
263                           NIL(mdd_t *), FALSE);
264        newRelationArray = NIL(array_t);
265        cofactorCube = NIL(mdd_t);
266        abstractCube = NIL(mdd_t);
267      }
268
269      if (info->useConstraint == 2) {
270        size1 = ImgVectorBddSize(info->vector);
271        size2 = ImgVectorBddSize(newVector);
272        if (info->option->rangeCheckReorder) {
273          bdd_reorder(info->manager);
274          size1 = ImgVectorBddSize(info->vector);
275          size2 = ImgVectorBddSize(newVector);
276        }
277        if (size2 > size1 * info->option->rangeThreshold) { /* cancel */
278          if (info->option->verbosity)
279            fprintf(vis_stdout, "** tfm info: canceled range computation.\n");
280          info->useConstraint = 1;
281          ImgVectorFree(newVector);
282          newVector = info->vector;
283          mdd_free(cube);
284          cube = mdd_one(info->manager);
285          if (newRelationArray && newRelationArray != relationArray)
286            mdd_array_free(newRelationArray);
287          if (cofactorCube) {
288            mdd_free(cofactorCube);
289            cofactorCube = mdd_one(info->manager);
290          }
291          if (abstractCube) {
292            mdd_free(abstractCube);
293            abstractCube = mdd_one(info->manager);
294          }
295          info->nImageComps++;
296        } else {
297          info->useConstraint = 0;
298          info->nImageComps = 0;
299          info->nRangeComps++;
300        }
301      }
302    }
303    if (info->useConstraint == 0 && relationArray) {
304      if (!newRelationArray) {
305        if (bdd_is_tautology(cofactorCube, 1) &&
306            bdd_is_tautology(abstractCube, 1)) {
307          newRelationArray = ImgGetConstrainedRelationArray(info, relationArray,
308                                                            newFrom);
309        } else {
310          tmpRelationArray = ImgGetConstrainedRelationArray(info, relationArray,
311                                                            newFrom);
312          newRelationArray = ImgGetCofactoredAbstractedRelationArray(
313                                        info->manager, tmpRelationArray,
314                                        cofactorCube, abstractCube);
315          if (info->option->debug) {
316            array_t     *tmpVector;
317
318            tmpVector = ImgGetConstrainedVector(info, info->vector, newFrom);
319            if (info->option->checkEquivalence) {
320              assert(ImgCheckEquivalence(info, tmpVector, tmpRelationArray,
321                                         NIL(mdd_t), NIL(mdd_t), 0));
322            }
323            refResult = ImgImageByHybrid(info, tmpVector, NIL(mdd_t));
324            ImgVectorFree(tmpVector);
325            res = ImgImageByHybridWithStaticSplit(info, NIL(array_t),
326                                                  NIL(mdd_t),
327                                                  tmpRelationArray,
328                                                  NIL(mdd_t), NIL(mdd_t));
329            assert(mdd_equal(refResult, res));
330            mdd_free(refResult);
331            mdd_free(res);
332          }
333          mdd_array_free(tmpRelationArray);
334        }
335        mdd_free(cofactorCube);
336        cofactorCube = NIL(mdd_t);
337        mdd_free(abstractCube);
338        abstractCube = NIL(mdd_t);
339        if (info->option->debug) {
340          refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
341          res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), NIL(mdd_t),
342                                                newRelationArray,
343                                                NIL(mdd_t), NIL(mdd_t));
344          assert(mdd_equal(refResult, res));
345          mdd_free(refResult);
346          mdd_free(res);
347
348          if (info->nIntermediateVars) {
349            mdd_t       *tmp;
350
351            refResult = ImgImageByHybrid(info, info->vector, newFrom);
352            res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), newFrom,
353                                                  relationArray,
354                                                  NIL(mdd_t), NIL(mdd_t));
355            assert(mdd_equal(refResult, res));
356            mdd_free(res);
357            tmp = ImgImageByHybrid(info, newVector, NIL(mdd_t));
358            res = mdd_and(tmp, cube, 1, 1);
359            if (info->option->verbosity) {
360              size = bdd_size(res);
361              if (size > info->maxIntermediateSize)
362                info->maxIntermediateSize = size;
363              if (info->option->printBddSize) {
364                fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
365                        bdd_size(tmp), bdd_size(cube), size);
366              }
367            }
368            mdd_free(tmp);
369            assert(mdd_equal(refResult, res));
370            mdd_free(refResult);
371            mdd_free(res);
372          }
373        }
374      }
375      if (relationArray != newRelationArray) {
376        mdd_array_free(relationArray);
377        relationArray = newRelationArray;
378      }
379    }
380    if (info->option->checkEquivalence) {
381      assert(ImgCheckEquivalence(info, newVector, newRelationArray,
382                                  NIL(mdd_t), NIL(mdd_t), 0));
383    }
384  }
385  partial = 0;
386  one = mdd_one(info->manager);
387  splitMethod = info->option->splitMethod;
388  if (splitMethod == 0) {
389    r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t),
390                          NIL(mdd_t), NIL(mdd_t), 0, 0, 0);
391  } else if (splitMethod == 1)
392    r = ImageByOutputSplit(info, newVector, one, 0);
393  else {
394    if (info->option->splitMethod == 0)
395      turnDepth = info->nVars + 1;
396    else
397      turnDepth = info->option->turnDepth;
398    if (turnDepth == 0) {
399      if (splitMethod == 2)
400        r = ImageByOutputSplit(info, newVector, one, 0);
401      else {
402        if (info->useConstraint && info->buildTR == 2) {
403          if (info->buildPartialTR) {
404            r = ImgImageByHybridWithStaticSplit(info, newVector, newFrom,
405                                                relationArray,
406                                                NIL(mdd_t), NIL(mdd_t));
407          } else {
408            r = ImgImageByHybridWithStaticSplit(info, NIL(array_t), newFrom,
409                                                relationArray,
410                                                NIL(mdd_t), NIL(mdd_t));
411          }
412        } else
413          r = ImgImageByHybrid(info, newVector, newFrom);
414      }
415    } else if (splitMethod == 2) {
416      r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t),
417                                NIL(mdd_t), NIL(mdd_t),
418                                splitMethod, turnDepth, 0);
419    } else {
420      if (info->useConstraint) {
421        if (info->buildTR) {
422          if (info->buildTR == 2) {
423            if (info->buildPartialTR) {
424              r = ImageByStaticInputSplit(info, newVector, newFrom,
425                                          relationArray, turnDepth, 0);
426              partial = 1;
427            } else {
428              r = ImageByStaticInputSplit(info, NIL(array_t), newFrom,
429                                          relationArray, turnDepth, 0);
430            }
431          } else if (info->option->delayedSplit) {
432            r = ImageByInputSplit(info, newVector, one, newFrom, relationArray,
433                                  cofactorCube, abstractCube,
434                                  splitMethod, turnDepth, 0);
435          } else {
436            r = ImageByInputSplit(info, newVector, one, newFrom, relationArray,
437                                  NIL(mdd_t), NIL(mdd_t),
438                                  splitMethod, turnDepth, 0);
439          }
440        } else {
441          r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t),
442                                NIL(mdd_t), NIL(mdd_t),
443                                splitMethod, turnDepth, 0);
444        }
445      } else if (info->buildTR == 1 && info->option->delayedSplit) {
446        r = ImageByInputSplit(info, newVector, one, NIL(mdd_t), relationArray,
447                                cofactorCube, abstractCube,
448                                splitMethod, turnDepth, 0);
449      } else {
450        r = ImageByInputSplit(info, newVector, one, NIL(mdd_t), relationArray,
451                                NIL(mdd_t), NIL(mdd_t),
452                                splitMethod, turnDepth, 0);
453      }
454    }
455  }
456  info->useConstraint = saveUseConstraint;
457  if (relationArray &&
458      !(info->option->debug && (partial || info->buildTR == 2))) {
459    mdd_array_free(relationArray);
460  }
461  if (info->imgCache && info->option->autoFlushCache == 1)
462    ImgFlushCache(info->imgCache);
463  mdd_free(one);
464  if (cofactorCube)
465    mdd_free(cofactorCube);
466  if (abstractCube)
467    mdd_free(abstractCube);
468  if (newFrom && newFrom != from)
469    mdd_free(newFrom);
470  res = bdd_and(r, cube, 1, 1);
471  if (info->option->verbosity) {
472    size = bdd_size(res);
473    if (size > info->maxIntermediateSize)
474      info->maxIntermediateSize = size;
475    if (info->option->printBddSize) {
476      fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
477              bdd_size(r), bdd_size(cube), size);
478    }
479  }
480  mdd_free(r);
481  mdd_free(cube);
482  if (newVector != info->vector)
483    ImgVectorFree(newVector);
484
485  if (info->option->debug) {
486    if (info->buildTR == 2) {
487      refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
488                                                  relationArray,
489                                                  NIL(mdd_t), NIL(mdd_t));
490      mdd_array_free(relationArray);
491    } else {
492      if (partial) {
493        refResult = ImgImageByHybrid(info, info->fullVector, from);
494        assert(mdd_equal(refResult, res));
495        mdd_free(refResult);
496        refResult = ImgImageByHybridWithStaticSplit(info, info->vector, from,
497                                                    relationArray,
498                                                    NIL(mdd_t), NIL(mdd_t));
499        mdd_array_free(relationArray);
500      } else
501        refResult = ImgImageByHybrid(info, info->vector, from);
502    }
503    assert(mdd_equal(refResult, res));
504    mdd_free(refResult);
505  }
506  if (info->option->findEssential)
507    info->lastFoundEssentialDepth = info->foundEssentialDepth;
508  if (info->option->printEssential == 2) {
509    maxDepth = info->maxDepth < IMG_TF_MAX_PRINT_DEPTH ?
510                info->maxDepth : IMG_TF_MAX_PRINT_DEPTH;
511    fprintf(vis_stdout, "foundEssential:");
512    for (i = 0; i < maxDepth; i++)
513      fprintf(vis_stdout, " [%d]%d", i, info->foundEssentials[i]);
514    fprintf(vis_stdout, "\n");
515  }
516  if (info->option->verbosity) {
517    fprintf(vis_stdout, "** tfm info: max intermediate BDD size = %d\n",
518            info->maxIntermediateSize);
519  }
520  if (info->option->debug)
521    assert(TfmCheckImageValidity(info, res));
522  return(res);
523}
524
525
526/**Function********************************************************************
527
528  Synopsis    [Chooses splitting variables for static splitting.]
529
530  Description [Chooses splitting variables for static splitting.]
531
532  SideEffects []
533
534******************************************************************************/
535mdd_t *
536ImgChooseTrSplitVar(ImgTfmInfo_t *info, array_t *vector,
537                    array_t *relationArray, int trSplitMethod, int piSplitFlag)
538{
539  int                   i, j, nVars;
540  ImgComponent_t        *comp;
541  char                  *support;
542  int                   *varCost, bestCost = 0;
543  int                   id, split;
544  mdd_t                 *var, *relation;
545
546  nVars = info->nVars;
547  varCost = ALLOC(int, nVars);
548  memset(varCost, 0, sizeof(int) * nVars);
549
550  if (trSplitMethod == 0) {
551    if (vector) {
552      for (i = 0; i < array_n(vector); i++) {
553        comp = array_fetch(ImgComponent_t *, vector, i);
554        support = comp->support;
555        for (j = 0; j < nVars; j++) {
556          if (support[j])
557            varCost[j]++;
558        }
559      }
560    }
561    comp = ImgComponentAlloc(info);
562    support = comp->support;
563    for (i = 0; i < array_n(relationArray); i++) {
564      relation = array_fetch(mdd_t *, relationArray, i);
565      comp->func = relation;
566      ImgSupportClear(info, comp->support);
567      ImgComponentGetSupport(comp);
568      for (j = 0; j < nVars; j++) {
569        if (support[j])
570          varCost[j]++;
571      }
572    }
573    comp->func = NIL(mdd_t);
574    ImgComponentFree(comp);
575  } else {
576    for (i = 0; i < array_n(info->domainVarBddArray); i++) {
577      var = array_fetch(mdd_t *, info->domainVarBddArray, i);
578      id = (int)bdd_top_var_id(var);
579      if (vector) {
580        for (j = 0; j < array_n(vector); j++) {
581          comp = array_fetch(ImgComponent_t *, vector, j);
582          varCost[id] += bdd_estimate_cofactor(comp->func, var, 1);
583          varCost[id] += bdd_estimate_cofactor(comp->func, var, 0);
584        }
585      }
586      for (j = 0; j < array_n(relationArray); j++) {
587        relation = array_fetch(mdd_t *, relationArray, j);
588        varCost[id] += bdd_estimate_cofactor(relation, var, 1);
589        varCost[id] += bdd_estimate_cofactor(relation, var, 0);
590      }
591      varCost[id] = IMG_TF_MAX_INT - varCost[id];
592    }
593  }
594
595  split = -1;
596  for (i = 0; i < nVars; i++) {
597    if (varCost[i] == 0)
598      continue;
599    if (!piSplitFlag) {
600      if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
601        continue;
602    }
603    if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
604      continue;
605    if (info->intermediateVarsTable &&
606        st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) {
607      continue;
608    }
609
610    if (split == -1 || varCost[i] > bestCost) {
611      bestCost = varCost[i];
612      split = i;
613    }
614  }
615  FREE(varCost);
616  if (split == -1)
617    return(NIL(mdd_t));
618  var = bdd_var_with_index(info->manager, split);
619  return(var);
620}
621
622
623/*---------------------------------------------------------------------------*/
624/* Definition of static functions                                            */
625/*---------------------------------------------------------------------------*/
626
627
628/**Function********************************************************************
629
630  Synopsis    [Computes an image by input splitting.]
631
632  Description [Computes an image by input splitting.]
633
634  SideEffects []
635
636******************************************************************************/
637static mdd_t *
638ImageByInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint,
639                  mdd_t *from, array_t *relationArray, mdd_t *cofactorCube,
640                  mdd_t *abstractCube, int splitMethod, int turnDepth,
641                  int depth)
642{
643  array_t               *newVector, *tmpVector;
644  mdd_t                 *new_, *resT, *resE, *res, *resPart, *resTmp;
645  mdd_t                 *var, *varNot, *cube, *tmp, *func;
646  int                   size, i, j, k, vectorSize;
647  array_t               *vectorArray, *varArray;
648  int                   hit, turnFlag;
649  int                   split, nGroups, cubeSize;
650  mdd_t                 *refResult, *product;
651  mdd_t                 *newFrom, *fromT, *fromE;
652  ImgComponent_t        *comp;
653  array_t               *relationArrayT, *relationArrayE, *partRelationArray;
654  int                   constConstrain;
655  int                   nRecur;
656  array_t               *newRelationArray, *tmpRelationArray, *abstractVars;
657  mdd_t                 *cofactor, *abstract;
658  mdd_t                 *newCofactorCube, *newAbstractCube;
659  mdd_t                 *partCofactorCube, *partAbstractCube;
660  mdd_t                 *cofactorCubeT, *cofactorCubeE;
661  mdd_t                 *abstractCubeT, *abstractCubeE;
662  mdd_t                 *essentialCube, *tmpRes;
663  int                   findEssential;
664  int                   foundEssentialDepth;
665  int                   foundEssentialDepthT, foundEssentialDepthE;
666  array_t               *vectorT, *vectorE;
667  mdd_t                 *andT, *andE, *one;
668  float                 prevLambda;
669  int                   prevTotal, prevVectorBddSize, prevVectorSize;
670  int                   arraySize, nFuncs;
671
672  newRelationArray = NIL(array_t);
673
674  if (info->option->delayedSplit && relationArray) {
675    ImgVectorConstrain(info, vector, constraint, relationArray,
676                        &newVector, &res, &newRelationArray,
677                        &cofactor, &abstract, TRUE);
678    newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1);
679    mdd_free(cofactor);
680    newAbstractCube = mdd_and(abstractCube, abstract, 1, 1);
681    mdd_free(abstract);
682    if (info->option->debug) {
683      refResult = ImgImageByHybrid(info, newVector, from);
684      resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
685                                                newRelationArray,
686                                                newCofactorCube,
687                                                newAbstractCube);
688      assert(mdd_equal(refResult, resPart));
689      mdd_free(refResult);
690      mdd_free(resPart);
691    }
692  } else {
693    ImgVectorConstrain(info, vector, constraint, relationArray,
694                        &newVector, &res, &newRelationArray,
695                        NIL(mdd_t *), NIL(mdd_t *), TRUE);
696    newCofactorCube = NIL(mdd_t);
697    newAbstractCube = NIL(mdd_t);
698    if (info->option->debug) {
699      refResult = ImgImageByHybrid(info, newVector, from);
700      resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
701                                                newRelationArray,
702                                                NIL(mdd_t), NIL(mdd_t));
703      assert(mdd_equal(refResult, resPart));
704      mdd_free(refResult);
705
706      refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
707                                                relationArray,
708                                                NIL(mdd_t), NIL(mdd_t));
709      resTmp = mdd_and(resPart, res, 1, 1);
710      mdd_free(resPart);
711      assert(mdd_equal(refResult, resTmp));
712      mdd_free(refResult);
713      mdd_free(resTmp);
714    }
715  }
716
717  if (info->option->checkEquivalence &&
718      relationArray && !info->option->buildPartialTR) {
719    assert(ImgCheckEquivalence(info, newVector, newRelationArray,
720                                newCofactorCube, newAbstractCube, 0));
721  }
722
723  if (from && info->option->findEssential) {
724    if (info->option->findEssential == 1)
725      findEssential = 1;
726    else {
727      if (depth >= info->lastFoundEssentialDepth)
728        findEssential = 1;
729      else
730        findEssential = 0;
731    }
732  } else
733    findEssential = 0;
734  if (findEssential) {
735    essentialCube = bdd_find_essential_cube(from);
736
737    if (!bdd_is_tautology(essentialCube, 1)) {
738      info->averageFoundEssential = (info->averageFoundEssential *
739        (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) /
740        (float)(info->nFoundEssentials + 1);
741      info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth *
742        (float)info->nFoundEssentials + (float)depth) /
743        (float)(info->nFoundEssentials + 1);
744      if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth)
745        info->topFoundEssentialDepth = depth;
746      info->nFoundEssentials++;
747      if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
748        info->foundEssentials[depth]++;
749      tmpVector = newVector;
750      tmpRelationArray = newRelationArray;
751      if (info->option->delayedSplit && relationArray) {
752        ImgVectorMinimize(info, tmpVector, essentialCube, NIL(mdd_t),
753                          tmpRelationArray, &newVector, &tmpRes,
754                          &newRelationArray, &cofactor, &abstract);
755        tmp = newCofactorCube;
756        newCofactorCube = mdd_and(tmp, cofactor, 1, 1);
757        mdd_free(tmp);
758        mdd_free(cofactor);
759        tmp = newAbstractCube;
760        newAbstractCube = mdd_and(tmp, abstract, 1, 1);
761        mdd_free(tmp);
762        mdd_free(abstract);
763      } else {
764        ImgVectorMinimize(info, tmpVector, essentialCube, NIL(mdd_t),
765                          tmpRelationArray, &newVector, &tmpRes,
766                          &newRelationArray, NIL(mdd_t *), NIL(mdd_t *));
767      }
768      tmp = res;
769      res = mdd_and(tmp, tmpRes, 1, 1);
770      mdd_free(tmp);
771      ImgVectorFree(tmpVector);
772      if (tmpRelationArray && tmpRelationArray != relationArray &&
773          tmpRelationArray != newRelationArray)
774        mdd_array_free(tmpRelationArray);
775      foundEssentialDepth = depth;
776    } else
777      foundEssentialDepth = info->option->maxEssentialDepth;
778    mdd_free(essentialCube);
779    foundEssentialDepthT = info->option->maxEssentialDepth;
780    foundEssentialDepthE = info->option->maxEssentialDepth;
781  } else {
782    /* To remove compiler warnings */
783    foundEssentialDepth = -1;
784    foundEssentialDepthT = -1;
785    foundEssentialDepthE = -1;
786  }
787
788  if (info->option->debug) {
789    if (relationArray && from) {
790      refResult = ImgImageByHybrid(info, newVector, from);
791      resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
792                                                newRelationArray,
793                                                newCofactorCube,
794                                                newAbstractCube);
795      assert(mdd_equal(refResult, resPart));
796      mdd_free(refResult);
797      mdd_free(resPart);
798    }
799  }
800
801  info->nRecursion++;
802  arraySize = array_n(newVector);
803  if (info->nIntermediateVars)
804    nFuncs = ImgVectorFunctionSize(newVector);
805  else
806    nFuncs = arraySize;
807  if (nFuncs <= 1) {
808    if (info->useConstraint) {
809      if (nFuncs == 1) {
810        comp = array_fetch(ImgComponent_t *, newVector, 0);
811        if (arraySize > 1)
812          func = ImgGetComposedFunction(newVector);
813        else
814          func = comp->func;
815        if (mdd_lequal(from, func, 1, 1)) { /* func | from = 1 */
816          tmp = res;
817          res = mdd_and(tmp, comp->var, 1, 1);
818          mdd_free(tmp);
819        } else if (mdd_lequal(func, from, 1, 0)) { /* func | from = 0 */
820          tmp = res;
821          res = mdd_and(tmp, comp->var, 1, 0);
822          mdd_free(tmp);
823        }
824        if (arraySize > 1)
825          mdd_free(func);
826      }
827    }
828    if (relationArray && newRelationArray != relationArray)
829      mdd_array_free(newRelationArray);
830    if (newCofactorCube)
831      mdd_free(newCofactorCube);
832    if (newAbstractCube)
833      mdd_free(newAbstractCube);
834    ImgVectorFree(newVector);
835    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
836                          (float)depth) / (float)(info->nLeaves + 1);
837    if (depth > info->maxDepth)
838      info->maxDepth = depth;
839    info->nLeaves++;
840    if (findEssential)
841      info->foundEssentialDepth = foundEssentialDepth;
842    if (info->option->debug)
843      assert(TfmCheckImageValidity(info, res));
844    return(res);
845  }
846
847  turnFlag = 0;
848  if (splitMethod == 3 && turnDepth == -1) {
849    if (depth < info->option->splitMinDepth) {
850      info->nSplits++;
851      turnFlag = 0;
852    } else if (depth > info->option->splitMaxDepth) {
853      info->nConjoins++;
854      turnFlag = 1;
855    } else {
856      turnFlag = ImgDecideSplitOrConjoin(info, newVector, from, 0,
857                                         newRelationArray, newCofactorCube,
858                                         newAbstractCube, 0, depth);
859    }
860  } else {
861    if (splitMethod != 0) {
862      if (depth == turnDepth)
863        turnFlag = 1;
864    }
865  }
866  if (turnFlag || nFuncs == 2) {
867    hit = 1;
868    if (!info->imgCache ||
869        !(resPart = ImgCacheLookupTable(info, info->imgCache, newVector,
870                                        from))) {
871      hit = 0;
872      if (nFuncs == 2) {
873        if (info->useConstraint) {
874          ImgVectorConstrain(info, newVector, from, NIL(array_t),
875                             &tmpVector, &resTmp, NIL(array_t *),
876                             NIL(mdd_t *), NIL(mdd_t *), FALSE);
877          if (array_n(tmpVector) <= 1)
878            resPart = resTmp;
879          else {
880            mdd_free(resTmp);
881            resPart = ImageFast2(info, tmpVector);
882          }
883          ImgVectorFree(tmpVector);
884        } else
885          resPart = ImageFast2(info, newVector);
886      } else if (splitMethod == 2) {
887        if (info->useConstraint) {
888          ImgVectorConstrain(info, newVector, from, NIL(array_t),
889                             &tmpVector, &resTmp, NIL(array_t *),
890                             NIL(mdd_t *), NIL(mdd_t *), FALSE);
891          if (array_n(tmpVector) <= 1)
892            resPart = resTmp;
893          else if (array_n(tmpVector) == 2) {
894            mdd_free(resTmp);
895            resPart = ImageFast2(info, tmpVector);
896          } else {
897            tmp = mdd_one(info->manager);
898            resPart = ImageByOutputSplit(info, tmpVector, tmp, depth + 1);
899            mdd_free(tmp);
900            tmp = resPart;
901            resPart = mdd_and(tmp, resTmp, 1, 1);
902            mdd_free(tmp);
903            mdd_free(resTmp);
904          }
905          ImgVectorFree(tmpVector);
906        } else {
907          tmp = mdd_one(info->manager);
908          resPart = ImageByOutputSplit(info, newVector, tmp, depth + 1);
909          mdd_free(tmp);
910        }
911      } else {
912        if (relationArray) {
913          resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
914                                                    newRelationArray,
915                                                    newCofactorCube,
916                                                    newAbstractCube);
917        } else
918          resPart = ImgImageByHybrid(info, newVector, from);
919      }
920      if (info->imgCache) {
921        if (from) {
922          ImgCacheInsertTable(info->imgCache, newVector, mdd_dup(from),
923                                resPart);
924        } else
925          ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t), resPart);
926      }
927    }
928
929    if (relationArray && newRelationArray != relationArray)
930      mdd_array_free(newRelationArray);
931    if (newCofactorCube)
932      mdd_free(newCofactorCube);
933    if (newAbstractCube)
934      mdd_free(newAbstractCube);
935
936    if (info->option->debug) {
937      refResult = ImgImageByHybrid(info, newVector, from);
938      assert(mdd_equal(refResult, resPart));
939      mdd_free(refResult);
940    }
941
942    new_ = mdd_and(res, resPart, 1, 1);
943    if (info->option->verbosity) {
944      size = bdd_size(new_);
945      if (size > info->maxIntermediateSize)
946        info->maxIntermediateSize = size;
947      if (info->option->printBddSize) {
948        fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
949                bdd_size(res), bdd_size(resPart), size);
950      }
951    }
952    mdd_free(res);
953    res = new_;
954    if (!info->imgCache || hit) {
955      mdd_free(resPart);
956      ImgVectorFree(newVector);
957    }
958    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
959                          (float)depth) / (float)(info->nLeaves + 1);
960    if (depth > info->maxDepth)
961      info->maxDepth = depth;
962    info->nLeaves++;
963    if (turnFlag)
964      info->nTurns++;
965    if (findEssential)
966      info->foundEssentialDepth = foundEssentialDepth;
967    if (info->option->debug)
968      assert(TfmCheckImageValidity(info, res));
969    return(res);
970  }
971
972  if (info->imgCache) {
973    resPart = ImgCacheLookupTable(info, info->imgCache, newVector, from);
974    if (resPart) {
975      if (info->option->debug) {
976        refResult = ImgImageByHybrid(info, newVector, from);
977        assert(mdd_equal(refResult, resPart));
978        mdd_free(refResult);
979      }
980      new_ = mdd_and(res, resPart, 1, 1);
981      if (info->option->verbosity) {
982        size = bdd_size(new_);
983        if (size > info->maxIntermediateSize)
984          info->maxIntermediateSize = size;
985        if (info->option->printBddSize) {
986          fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
987                  bdd_size(res), bdd_size(resPart), size);
988        }
989      }
990      mdd_free(res);
991      mdd_free(resPart);
992      res = new_;
993      ImgVectorFree(newVector);
994      if (relationArray && newRelationArray != relationArray)
995        mdd_array_free(newRelationArray);
996      if (newCofactorCube)
997        mdd_free(newCofactorCube);
998      if (newAbstractCube)
999        mdd_free(newAbstractCube);
1000      if (findEssential)
1001        info->foundEssentialDepth = foundEssentialDepth;
1002      if (info->option->debug)
1003        assert(TfmCheckImageValidity(info, res));
1004      return(res);
1005    }
1006  }
1007
1008  if (info->option->splitCubeFunc) {
1009    split = -1;
1010    cubeSize = 0;
1011    for (i = 0; i < array_n(newVector); i++) {
1012      comp = array_fetch(ImgComponent_t *, newVector, i);
1013      if (bdd_is_cube(comp->func)) {
1014        if (split == -1 || info->option->splitCubeFunc == 1 ||
1015            bdd_size(comp->func) > cubeSize) {
1016          split = i;
1017          cubeSize = bdd_size(comp->func);
1018          break;
1019        }
1020      }
1021    }
1022    if (split != -1) {
1023      comp = array_fetch(ImgComponent_t *, newVector, split);
1024      info->nCubeSplits++;
1025      if (info->option->delayedSplit && relationArray) {
1026        ImgVectorConstrain(info, newVector, comp->func, newRelationArray,
1027                           &vectorT, &andT, &relationArrayT,
1028                           &cofactor, &abstract, FALSE);
1029        cofactorCubeT = mdd_and(newCofactorCube, cofactor, 1, 1);
1030        mdd_free(cofactor);
1031        abstractCubeT = mdd_and(newAbstractCube, abstract, 1, 1);
1032        mdd_free(abstract);
1033      } else {
1034        ImgVectorConstrain(info, newVector, comp->func, newRelationArray,
1035                           &vectorT, &andT, &relationArrayT,
1036                           NIL(mdd_t *), NIL(mdd_t *), FALSE);
1037        cofactorCubeT = NIL(mdd_t);
1038        abstractCubeT = NIL(mdd_t);
1039      }
1040      if (from)
1041        newFrom = bdd_cofactor(from, comp->func);
1042      else
1043        newFrom = from;
1044      if (info->option->checkEquivalence &&
1045          relationArray && !info->option->buildPartialTR) {
1046        assert(ImgCheckEquivalence(info, vectorT, relationArrayT,
1047                                   cofactorCubeT, abstractCubeT, 0));
1048      }
1049
1050      one = mdd_one(info->manager);
1051      if (newFrom && bdd_is_tautology(newFrom, 0))
1052        resT = mdd_zero(info->manager);
1053      else {
1054        prevLambda = info->prevLambda;
1055        prevTotal = info->prevTotal;
1056        prevVectorBddSize = info->prevVectorBddSize;
1057        prevVectorSize = info->prevVectorSize;
1058        resT = ImageByInputSplit(info, vectorT, one, newFrom,
1059                              relationArrayT, cofactorCubeT, abstractCubeT,
1060                              splitMethod, turnDepth, depth + 1);
1061        info->prevLambda = prevLambda;
1062        info->prevTotal = prevTotal;
1063        info->prevVectorBddSize = prevVectorBddSize;
1064        info->prevVectorSize = prevVectorSize;
1065      }
1066      ImgVectorFree(vectorT);
1067      if (newFrom)
1068        mdd_free(newFrom);
1069      if (!bdd_is_tautology(andT, 1)) {
1070        tmp = resT;
1071        resT = mdd_and(tmp, andT, 1, 1);
1072        mdd_free(tmp);
1073      }
1074      if (findEssential)
1075        foundEssentialDepthT = info->foundEssentialDepth;
1076      if (relationArrayT && relationArrayT != newRelationArray)
1077        mdd_array_free(relationArrayT);
1078      if (cofactorCubeT && cofactorCubeT != newCofactorCube)
1079        mdd_free(cofactorCubeT);
1080      if (abstractCubeT && abstractCubeT != newAbstractCube)
1081        mdd_free(abstractCubeT);
1082
1083      tmp = mdd_not(comp->func);
1084      if (info->option->delayedSplit && relationArray) {
1085        ImgVectorConstrain(info, newVector, tmp, newRelationArray,
1086                           &vectorE, &andE, &relationArrayE,
1087                           &cofactor, &abstract, FALSE);
1088        cofactorCubeE = mdd_and(newCofactorCube, cofactor, 1, 1);
1089        mdd_free(cofactor);
1090        abstractCubeE = mdd_and(newAbstractCube, abstract, 1, 1);
1091        mdd_free(abstract);
1092      } else {
1093        ImgVectorConstrain(info, newVector, tmp, newRelationArray,
1094                           &vectorE, &andE, &relationArrayE,
1095                           NIL(mdd_t *), NIL(mdd_t *), FALSE);
1096        cofactorCubeE = NIL(mdd_t);
1097        abstractCubeE = NIL(mdd_t);
1098      }
1099      if (from)
1100        newFrom = bdd_cofactor(from, tmp);
1101      else
1102        newFrom = from;
1103      mdd_free(tmp);
1104      if (relationArray && newRelationArray != relationArray)
1105        mdd_array_free(newRelationArray);
1106      if (newCofactorCube)
1107        mdd_free(newCofactorCube);
1108      if (newAbstractCube)
1109        mdd_free(newAbstractCube);
1110      if (info->option->checkEquivalence &&
1111          relationArray && !info->option->buildPartialTR) {
1112        assert(ImgCheckEquivalence(info, vectorE, relationArrayE,
1113                                   cofactorCubeE, abstractCubeE, 0));
1114      }
1115
1116      if (newFrom && bdd_is_tautology(newFrom, 0))
1117        resE = mdd_zero(info->manager);
1118      else {
1119        resE = ImageByInputSplit(info, vectorE, one, newFrom,
1120                              relationArrayE, cofactorCubeE, abstractCubeE,
1121                              splitMethod, turnDepth, depth + 1);
1122      }
1123      ImgVectorFree(vectorE);
1124      if (newFrom)
1125        mdd_free(newFrom);
1126      if (!bdd_is_tautology(andE, 1)) {
1127        tmp = resE;
1128        resE = mdd_and(tmp, andE, 1, 1);
1129        mdd_free(tmp);
1130      }
1131      if (findEssential)
1132        foundEssentialDepthE = info->foundEssentialDepth;
1133      if (relationArrayE && relationArrayE != newRelationArray)
1134        mdd_array_free(relationArrayE);
1135      if (cofactorCubeE && cofactorCubeE != newCofactorCube)
1136        mdd_free(cofactorCubeE);
1137      if (abstractCubeE && abstractCubeE != newAbstractCube)
1138        mdd_free(abstractCubeE);
1139
1140      resPart = bdd_ite(comp->var, resT, resE, 1, 1, 1);
1141      if (info->option->verbosity) {
1142        size = bdd_size(resPart);
1143        if (size > info->maxIntermediateSize)
1144          info->maxIntermediateSize = size;
1145        if (info->option->printBddSize) {
1146          fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n",
1147                  bdd_size(resT), bdd_size(resE), size);
1148        }
1149      }
1150      mdd_free(one);
1151
1152      if (info->imgCache)
1153        ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t), resPart);
1154
1155      if (info->option->debug) {
1156        refResult = ImgImageByHybrid(info, newVector, from);
1157        assert(mdd_equal(refResult, resPart));
1158        mdd_free(refResult);
1159      }
1160
1161      new_ = mdd_and(res, resPart, 1, 1);
1162      if (info->option->verbosity) {
1163        size = bdd_size(new_);
1164        if (size > info->maxIntermediateSize)
1165          info->maxIntermediateSize = size;
1166        if (info->option->printBddSize) {
1167          fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
1168                  bdd_size(res), bdd_size(resPart), size);
1169        }
1170      }
1171      mdd_free(res);
1172      res = new_;
1173
1174      if (info->option->debug) {
1175        refResult = ImgImageByHybrid(info, newVector, from);
1176        assert(mdd_equal(refResult, resPart));
1177        mdd_free(refResult);
1178      }
1179
1180      if (!info->imgCache) {
1181        mdd_free(resPart);
1182        ImgVectorFree(newVector);
1183      }
1184      info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1185                            (float)depth) / (float)(info->nLeaves + 1);
1186      if (depth > info->maxDepth)
1187        info->maxDepth = depth;
1188      info->nLeaves++;
1189      if (turnFlag)
1190        info->nTurns++;
1191      if (findEssential) {
1192        if (foundEssentialDepth == info->option->maxEssentialDepth) {
1193          if (foundEssentialDepthT < foundEssentialDepthE)
1194            foundEssentialDepth = foundEssentialDepthT;
1195          else
1196            foundEssentialDepth = foundEssentialDepthE;
1197        }
1198        info->foundEssentialDepth = foundEssentialDepth;
1199      }
1200      if (info->option->debug)
1201        assert(TfmCheckImageValidity(info, res));
1202      return(res);
1203    }
1204  }
1205
1206  /* compute disconnected component and best variable selection */
1207  vectorArray = array_alloc(array_t *, 0);
1208  varArray = array_alloc(int, 0);
1209  if (info->option->delayedSplit && relationArray) {
1210    nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, from, 0,
1211                                        info->option->inputSplit,
1212                                        info->option->piSplitFlag,
1213                                        vectorArray, varArray, &product,
1214                                        newRelationArray, &tmpRelationArray,
1215                                        &cofactor, &abstract);
1216  } else {
1217    nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, from, 0,
1218                                        info->option->inputSplit,
1219                                        info->option->piSplitFlag,
1220                                        vectorArray, varArray, &product,
1221                                        newRelationArray, &tmpRelationArray,
1222                                        NIL(mdd_t *), NIL(mdd_t *));
1223    cofactor = NIL(mdd_t);
1224    abstract = NIL(mdd_t);
1225
1226    if (info->option->debug && nGroups >= 1) {
1227      if (info->option->verbosity > 1) {
1228        ImgPrintVectorDependency(info, newVector, info->option->verbosity);
1229        PrintVectorDecomposition(info, vectorArray, varArray);
1230      }
1231
1232      refResult = ImgImageByHybrid(info, newVector, from);
1233      resPart = mdd_dup(product);
1234      for (i = 0; i < array_n(vectorArray); i++) {
1235        vector = array_fetch(array_t *, vectorArray, i);
1236        resTmp = ImgImageByHybrid(info, vector, from);
1237        tmp = resPart;
1238        resPart = mdd_and(tmp, resTmp, 1, 1);
1239        mdd_free(tmp);
1240        mdd_free(resTmp);
1241
1242        if (arraySize > nFuncs) {
1243          split = array_fetch(int, varArray, i);
1244          assert(!st_is_member(info->intermediateVarsTable,
1245                 (char *)(long)split));
1246        }
1247      }
1248      assert(mdd_equal(refResult, resPart));
1249      mdd_free(refResult);
1250      mdd_free(resPart);
1251    }
1252  }
1253  vectorSize = array_n(newVector);
1254  if ((!info->imgCache || nGroups <= 1) && !info->option->debug)
1255    ImgVectorFree(newVector);
1256  if (newRelationArray) {
1257    if (newRelationArray != relationArray &&
1258        tmpRelationArray != newRelationArray) {
1259      mdd_array_free(newRelationArray);
1260    }
1261    newRelationArray = tmpRelationArray;
1262  }
1263  if (nGroups == 0) {
1264    if (relationArray && newRelationArray != relationArray)
1265      mdd_array_free(newRelationArray);
1266    if (newCofactorCube)
1267      mdd_free(newCofactorCube);
1268    if (newAbstractCube)
1269      mdd_free(newAbstractCube);
1270    if (cofactor)
1271      mdd_free(cofactor);
1272    if (abstract)
1273      mdd_free(abstract);
1274
1275    array_free(vectorArray);
1276    array_free(varArray);
1277
1278    if (info->option->debug) {
1279      refResult = ImgImageByHybrid(info, newVector, from);
1280      assert(mdd_equal(refResult, product));
1281      mdd_free(refResult);
1282      ImgVectorFree(newVector);
1283    }
1284
1285    new_ = mdd_and(res, product, 1, 1);
1286    if (info->option->verbosity) {
1287      size = bdd_size(new_);
1288      if (size > info->maxIntermediateSize)
1289        info->maxIntermediateSize = size;
1290      if (info->option->printBddSize) {
1291        fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
1292                bdd_size(res), bdd_size(product), size);
1293      }
1294    }
1295    mdd_free(res);
1296    mdd_free(product);
1297    res = new_;
1298
1299    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1300                          (float)depth) / (float)(info->nLeaves + 1);
1301    if (depth > info->maxDepth)
1302      info->maxDepth = depth;
1303    info->nLeaves++;
1304    if (findEssential)
1305      info->foundEssentialDepth = foundEssentialDepth;
1306    if (info->option->debug)
1307      assert(TfmCheckImageValidity(info, res));
1308    return(res);
1309  }
1310
1311  if (info->option->delayedSplit && relationArray) {
1312    tmp = newCofactorCube;
1313    newCofactorCube = mdd_and(tmp, cofactor, 1, 1);
1314    mdd_free(tmp);
1315    mdd_free(cofactor);
1316    tmp = newAbstractCube;
1317    newAbstractCube = mdd_and(tmp, abstract, 1, 1);
1318    mdd_free(tmp);
1319    mdd_free(abstract);
1320  }
1321
1322  if (nGroups > 1) {
1323    if (info->nDecomps == 0 || depth < info->topDecomp)
1324      info->topDecomp = depth;
1325    if (info->nDecomps == 0 || vectorSize > info->maxDecomp)
1326      info->maxDecomp = vectorSize;
1327    info->averageDecomp = (info->averageDecomp * (float)info->nDecomps +
1328                          (float)nGroups) / (float)(info->nDecomps + 1);
1329    info->nDecomps++;
1330  }
1331
1332  if (relationArray && nGroups > 1) {
1333    abstractVars = array_alloc(mdd_t *, 0);
1334    for (i = 0; i < array_n(vectorArray); i++) {
1335      vector = array_fetch(array_t *, vectorArray, i);
1336      cube = mdd_one(info->manager);
1337      for (j = 0; j < nGroups; j++) {
1338        if (j == i)
1339          continue;
1340        tmpVector = array_fetch(array_t *, vectorArray, j);
1341        for (k = 0; k < array_n(tmpVector); k++) {
1342          comp = array_fetch(ImgComponent_t *, tmpVector, k);
1343          tmp = cube;
1344          cube = mdd_and(cube, comp->var, 1, 1);
1345          mdd_free(tmp);
1346        }
1347      }
1348      tmp = ImgSubstitute(cube, info->functionData, Img_D2R_c);
1349      mdd_free(cube);
1350      array_insert_last(mdd_t *, abstractVars, tmp);
1351    }
1352  } else
1353    abstractVars = NIL(array_t);
1354  for (i = 0; i < array_n(vectorArray); i++) {
1355    vector = array_fetch(array_t *, vectorArray, i);
1356    if (from)
1357      newFrom = mdd_dup(from);
1358    else
1359      newFrom = from;
1360
1361    if (relationArray) {
1362      if (nGroups == 1) {
1363        partRelationArray = newRelationArray;
1364        if (info->option->delayedSplit) {
1365          partCofactorCube = newCofactorCube;
1366          partAbstractCube = newAbstractCube;
1367        } else {
1368          partCofactorCube = NIL(mdd_t);
1369          partAbstractCube = NIL(mdd_t);
1370        }
1371      } else {
1372        cube = array_fetch(mdd_t *, abstractVars, i);
1373        if (info->option->delayedSplit) {
1374          partRelationArray = newRelationArray;
1375          partCofactorCube = mdd_dup(newCofactorCube);
1376          partAbstractCube = mdd_and(newAbstractCube, cube, 1, 1);
1377        } else {
1378          partRelationArray = ImgGetAbstractedRelationArray(info->manager,
1379                                                            newRelationArray,
1380                                                            cube);
1381          mdd_free(cube);
1382          partCofactorCube = NIL(mdd_t);
1383          partAbstractCube = NIL(mdd_t);
1384        }
1385      }
1386      if (info->option->debug) {
1387        refResult = ImgImageByHybrid(info, vector, from);
1388        resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from,
1389                                                  partRelationArray,
1390                                                  partCofactorCube,
1391                                                  partAbstractCube);
1392        assert(mdd_equal(refResult, resPart));
1393        mdd_free(refResult);
1394        mdd_free(resPart);
1395      }
1396    } else {
1397      partRelationArray = newRelationArray;
1398      partCofactorCube = NIL(mdd_t);
1399      partAbstractCube = NIL(mdd_t);
1400    }
1401    hit = 1;
1402    if (!info->imgCache || nGroups == 1 ||
1403        !(resPart = ImgCacheLookupTable(info, info->imgCache, vector,
1404                                        newFrom))) {
1405      hit = 0;
1406      if (arraySize > nFuncs)
1407        size = ImgVectorFunctionSize(vector);
1408      else
1409        size = array_n(vector);
1410      if (size == 1) {
1411        comp = array_fetch(ImgComponent_t *, vector, 0);
1412        if (array_n(vector) > 1)
1413          func = ImgGetComposedFunction(vector);
1414        else
1415          func = comp->func;
1416        if (info->useConstraint) {
1417          constConstrain = ImgConstConstrain(func, newFrom);
1418          if (constConstrain == 1)
1419            resPart = mdd_dup(comp->var);
1420          else if (constConstrain == 0)
1421            resPart = mdd_not(comp->var);
1422          else
1423            resPart = mdd_one(info->manager);
1424        } else {
1425          if (bdd_is_tautology(func, 1))
1426            resPart = mdd_dup(comp->var);
1427          else if (bdd_is_tautology(func, 0))
1428            resPart = mdd_not(comp->var);
1429          else
1430            resPart = mdd_one(info->manager);
1431        }
1432        if (array_n(vector) > 1)
1433          mdd_free(func);
1434        info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1435                                (float)depth) / (float)(info->nLeaves + 1);
1436        if (depth > info->maxDepth)
1437          info->maxDepth = depth;
1438        info->nLeaves++;
1439      } else if (size == 2) {
1440        if (info->useConstraint) {
1441          ImgVectorConstrain(info, vector, newFrom, NIL(array_t),
1442                             &newVector, &resTmp, NIL(array_t *),
1443                             NIL(mdd_t *), NIL(mdd_t *), FALSE);
1444          if (array_n(newVector) <= 1)
1445            resPart = resTmp;
1446          else {
1447            mdd_free(resTmp);
1448            resPart = ImageFast2(info, newVector);
1449          }
1450          ImgVectorFree(newVector);
1451        } else
1452          resPart = ImageFast2(info, vector);
1453        info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1454                                (float)depth) / (float)(info->nLeaves + 1);
1455        if (depth > info->maxDepth)
1456          info->maxDepth = depth;
1457        info->nLeaves++;
1458      } else {
1459        nRecur = 0;
1460        split = array_fetch(int, varArray, i);
1461        if (partRelationArray && info->imgKeepPiInTr == FALSE) {
1462          if (st_lookup(info->quantifyVarsTable, (char *)(long)split,
1463                        NIL(char *))) {
1464            int newSplit;
1465
1466            /* checks the splitting is valid */
1467            newSplit = CheckIfValidSplitOrGetNew(info, split, vector,
1468                                                partRelationArray, from);
1469            if (newSplit == -1) {
1470              resPart = ImgImageByHybrid(info, vector, from);
1471              info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1472                                (float)depth) / (float)(info->nLeaves + 1);
1473              if (depth > info->maxDepth)
1474                info->maxDepth = depth;
1475              info->nLeaves++;
1476              info->nTurns++;
1477              goto cache;
1478            }
1479            split = newSplit;
1480          }
1481        }
1482        var = bdd_var_with_index(info->manager, split);
1483        if (newFrom)
1484          fromT = bdd_cofactor(newFrom, var);
1485        else
1486          fromT = NIL(mdd_t);
1487        if (partRelationArray) {
1488          if (info->option->delayedSplit) {
1489            relationArrayT = partRelationArray;
1490            cofactorCubeT = mdd_and(partCofactorCube, var, 1, 1);
1491          } else {
1492            relationArrayT = ImgGetCofactoredRelationArray(partRelationArray,
1493                                                           var);
1494            cofactorCubeT = partCofactorCube;
1495          }
1496        } else {
1497          relationArrayT = NIL(array_t);
1498          cofactorCubeT = NIL(mdd_t);
1499        }
1500        if (!fromT || !bdd_is_tautology(fromT, 0)) {
1501          prevLambda = info->prevLambda;
1502          prevTotal = info->prevTotal;
1503          prevVectorBddSize = info->prevVectorBddSize;
1504          prevVectorSize = info->prevVectorSize;
1505          resT = ImageByInputSplit(info, vector, var, fromT,
1506                                relationArrayT, cofactorCubeT, partAbstractCube,
1507                                splitMethod, turnDepth, depth + 1);
1508          if (info->option->debug) {
1509            refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t),
1510                                                        fromT, relationArrayT,
1511                                                        cofactorCubeT,
1512                                                        partAbstractCube);
1513            assert(mdd_equal(refResult, resT));
1514            mdd_free(refResult);
1515          }
1516          info->prevLambda = prevLambda;
1517          info->prevTotal = prevTotal;
1518          info->prevVectorBddSize = prevVectorBddSize;
1519          info->prevVectorSize = prevVectorSize;
1520          if (findEssential)
1521            foundEssentialDepthT = info->foundEssentialDepth;
1522          nRecur++;
1523        } else
1524          resT = mdd_zero(info->manager);
1525        if (fromT)
1526          mdd_free(fromT);
1527        if (relationArrayT && relationArrayT != partRelationArray)
1528          mdd_array_free(relationArrayT);
1529        if (cofactorCubeT && cofactorCubeT != partCofactorCube)
1530          mdd_free(cofactorCubeT);
1531
1532        if (bdd_is_tautology(resT, 1)) {
1533          mdd_free(var);
1534          resPart = resT;
1535          info->nEmptySubImage++;
1536        } else {
1537          varNot = mdd_not(var);
1538          mdd_free(var);
1539          if (newFrom)
1540            fromE = bdd_cofactor(newFrom, varNot);
1541          else
1542            fromE = NIL(mdd_t);
1543          if (partRelationArray) {
1544            if (info->option->delayedSplit) {
1545              relationArrayE = partRelationArray;
1546              cofactorCubeE = mdd_and(partCofactorCube, varNot, 1, 1);
1547            } else {
1548              relationArrayE = ImgGetCofactoredRelationArray(partRelationArray,
1549                                                             varNot);
1550              cofactorCubeE = partCofactorCube;
1551            }
1552          } else {
1553            relationArrayE = NIL(array_t);
1554            cofactorCubeE = NIL(mdd_t);
1555          }
1556          if (!fromE || !bdd_is_tautology(fromE, 0)) {
1557            resE = ImageByInputSplit(info, vector, varNot, fromE,
1558                          relationArrayE, cofactorCubeE, partAbstractCube,
1559                          splitMethod, turnDepth, depth + 1);
1560            if (info->option->debug) {
1561              refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t),
1562                                                          fromE, relationArrayE,
1563                                                          cofactorCubeE,
1564                                                          partAbstractCube);
1565              assert(mdd_equal(refResult, resE));
1566              mdd_free(refResult);
1567            }
1568            if (findEssential)
1569              foundEssentialDepthE = info->foundEssentialDepth;
1570            nRecur++;
1571          } else
1572            resE = mdd_zero(info->manager);
1573          mdd_free(varNot);
1574          if (fromE)
1575            mdd_free(fromE);
1576          if (relationArrayE && relationArrayE != partRelationArray)
1577            mdd_array_free(relationArrayE);
1578          if (cofactorCubeE && cofactorCubeE != partCofactorCube)
1579            mdd_free(cofactorCubeE);
1580   
1581          resPart = mdd_or(resT, resE, 1, 1);
1582          if (info->option->debug) {
1583            refResult = ImgImageByHybrid(info, vector, from);
1584            assert(mdd_equal(refResult, resPart));
1585            mdd_free(refResult);
1586          }
1587          if (info->option->verbosity) {
1588            size = bdd_size(resPart);
1589            if (size > info->maxIntermediateSize)
1590              info->maxIntermediateSize = size;
1591            if (info->option->printBddSize) {
1592              fprintf(vis_stdout, "** tfm info: bdd_or(%d,%d) = %d\n",
1593                      bdd_size(resT), bdd_size(resE), size);
1594            }
1595          }
1596
1597          mdd_free(resT);
1598          mdd_free(resE);
1599        }
1600        if (nRecur == 0) {
1601          info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1602                                (float)depth) / (float)(info->nLeaves + 1);
1603          if (depth > info->maxDepth)
1604            info->maxDepth = depth;
1605          info->nLeaves++;
1606        }
1607      }
1608cache:
1609      if (info->imgCache) {
1610        ImgCacheInsertTable(info->imgCache, vector, newFrom, resPart);
1611        if (info->option->debug) {
1612          refResult = ImgImageByHybrid(info, vector, newFrom);
1613          assert(mdd_equal(refResult, resPart));
1614          mdd_free(refResult);
1615        }
1616      }
1617    }
1618    if (!info->imgCache || hit) {
1619      ImgVectorFree(vector);
1620      if (newFrom)
1621        mdd_free(newFrom);
1622    }
1623    new_ = mdd_and(product, resPart, 1, 1);
1624    if (info->option->verbosity) {
1625      size = bdd_size(new_);
1626      if (size > info->maxIntermediateSize)
1627        info->maxIntermediateSize = size;
1628      if (info->option->printBddSize) {
1629        fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
1630                bdd_size(product), bdd_size(resPart), size);
1631      }
1632    }
1633    mdd_free(product);
1634    if (!info->imgCache || hit)
1635      mdd_free(resPart);
1636    product = new_;
1637    if (nGroups > 1 && partRelationArray != newRelationArray)
1638      mdd_array_free(partRelationArray);
1639    if (partCofactorCube && partCofactorCube != newCofactorCube)
1640      mdd_free(partCofactorCube);
1641    if (partAbstractCube && partAbstractCube != newAbstractCube)
1642      mdd_free(partAbstractCube);
1643  }
1644  if (abstractVars)
1645    array_free(abstractVars);
1646
1647  if (relationArray && newRelationArray != relationArray)
1648    mdd_array_free(newRelationArray);
1649  if (newCofactorCube)
1650    mdd_free(newCofactorCube);
1651  if (newAbstractCube)
1652    mdd_free(newAbstractCube);
1653
1654  array_free(vectorArray);
1655  array_free(varArray);
1656
1657  if (info->imgCache && nGroups > 1) {
1658    if (from) {
1659      ImgCacheInsertTable(info->imgCache, newVector, mdd_dup(from),
1660                          mdd_dup(product));
1661    } else {
1662      ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t),
1663                          mdd_dup(product));
1664    }
1665  }
1666
1667  if (info->option->debug) {
1668    refResult = ImgImageByHybrid(info, newVector, from);
1669    assert(mdd_equal(refResult, product));
1670    mdd_free(refResult);
1671    if (!info->imgCache || nGroups == 1)
1672      ImgVectorFree(newVector);
1673  }
1674
1675  new_ = mdd_and(res, product, 1, 1);
1676  if (info->option->verbosity) {
1677    size = bdd_size(new_);
1678    if (size > info->maxIntermediateSize)
1679      info->maxIntermediateSize = size;
1680    if (info->option->printBddSize) {
1681      fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
1682              bdd_size(res), bdd_size(product), size);
1683    }
1684  }
1685  mdd_free(res);
1686  mdd_free(product);
1687  res = new_;
1688
1689  if (findEssential) {
1690    if (foundEssentialDepth == info->option->maxEssentialDepth) {
1691      if (foundEssentialDepthT < foundEssentialDepthE)
1692        foundEssentialDepth = foundEssentialDepthT;
1693      else
1694        foundEssentialDepth = foundEssentialDepthE;
1695    }
1696    info->foundEssentialDepth = foundEssentialDepth;
1697  }
1698  if (info->option->debug)
1699    assert(TfmCheckImageValidity(info, res));
1700  return(res);
1701}
1702
1703
1704/**Function********************************************************************
1705
1706  Synopsis    [Computes an image by static input splitting.]
1707
1708  Description [Computes an image by static input splitting.]
1709
1710  SideEffects []
1711
1712******************************************************************************/
1713static mdd_t *
1714ImageByStaticInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from,
1715                        array_t *relationArray, int turnDepth, int depth)
1716{
1717  array_t       *vectorT, *vectorE, *tmpVector;
1718  mdd_t         *resT, *resE, *res, *tmp, *cubeT, *cubeE;
1719  mdd_t         *fromT, *fromE;
1720  mdd_t         *var, *varNot;
1721  array_t       *relationArrayT, *relationArrayE;
1722  array_t       *newRelationArray, *tmpRelationArray;
1723  int           nRecur;
1724  mdd_t         *refResult, *and_;
1725  mdd_t         *essentialCube;
1726  int           findEssential;
1727  int           foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE;
1728  int           turnFlag, size;
1729
1730  info->nRecursion++;
1731
1732  turnFlag = 0;
1733  if (turnDepth == -1) {
1734    if (depth < info->option->splitMinDepth) {
1735      info->nSplits++;
1736      turnFlag = 0;
1737    } else if (depth > info->option->splitMaxDepth) {
1738      info->nConjoins++;
1739      turnFlag = 1;
1740    } else {
1741      turnFlag = ImgDecideSplitOrConjoin(info, vector, from, 0,
1742                                         relationArray, NIL(mdd_t),
1743                                         NIL(mdd_t), 1, depth);
1744    }
1745  } else {
1746    if (depth == turnDepth)
1747      turnFlag = 1;
1748    else
1749      turnFlag = 0;
1750  }
1751  if (turnFlag) {
1752    res = ImgImageByHybridWithStaticSplit(info, vector, from, relationArray,
1753                                          NIL(mdd_t), NIL(mdd_t));
1754    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1755                          (float)depth) / (float)(info->nLeaves + 1);
1756    if (depth > info->maxDepth)
1757      info->maxDepth = depth;
1758    info->nLeaves++;
1759    info->foundEssentialDepth = info->option->maxEssentialDepth;
1760    return(res);
1761  }
1762
1763  if (info->option->findEssential) {
1764    if (info->option->findEssential == 1)
1765      findEssential = 1;
1766    else {
1767      if (depth >= info->lastFoundEssentialDepth)
1768        findEssential = 1;
1769      else
1770        findEssential = 0;
1771    }
1772  } else
1773    findEssential = 0;
1774  if (findEssential) {
1775    essentialCube = bdd_find_essential_cube(from);
1776
1777    if (!bdd_is_tautology(essentialCube, 1)) {
1778      info->averageFoundEssential = (info->averageFoundEssential *
1779        (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) /
1780        (float)(info->nFoundEssentials + 1);
1781      info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth *
1782        (float)info->nFoundEssentials + (float)depth) /
1783        (float)(info->nFoundEssentials + 1);
1784      if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth)
1785        info->topFoundEssentialDepth = depth;
1786      if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH)
1787        info->foundEssentials[depth]++;
1788      info->nFoundEssentials++;
1789      ImgVectorMinimize(info, vector, essentialCube, NIL(mdd_t), relationArray,
1790                        &tmpVector, &and_,
1791                        &tmpRelationArray, NIL(mdd_t *), NIL(mdd_t *));
1792      foundEssentialDepth = depth;
1793    } else {
1794      tmpVector = vector;
1795      tmpRelationArray = relationArray;
1796      and_ = NIL(mdd_t);
1797      foundEssentialDepth = info->option->maxEssentialDepth;
1798    }
1799    mdd_free(essentialCube);
1800    foundEssentialDepthT = info->option->maxEssentialDepth;
1801    foundEssentialDepthE = info->option->maxEssentialDepth;
1802  } else {
1803    tmpVector = vector;
1804    tmpRelationArray = relationArray;
1805    and_ = NIL(mdd_t);
1806    /* To remove compiler warnings */
1807    foundEssentialDepth = -1;
1808    foundEssentialDepthT = -1;
1809    foundEssentialDepthE = -1;
1810  }
1811
1812  var = ImgChooseTrSplitVar(info, tmpVector, tmpRelationArray,
1813                            info->option->trSplitMethod,
1814                            info->option->piSplitFlag);
1815  if (!var) {
1816    res = ImgImageByHybridWithStaticSplit(info, vector, from, relationArray,
1817                                          NIL(mdd_t), NIL(mdd_t));
1818    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1819                          (float)depth) / (float)(info->nLeaves + 1);
1820    if (depth > info->maxDepth)
1821      info->maxDepth = depth;
1822    info->nLeaves++;
1823    info->foundEssentialDepth = info->option->maxEssentialDepth;
1824    return(res);
1825  }
1826
1827  nRecur = 0;
1828  if (tmpVector) {
1829    ImgVectorConstrain(info, tmpVector, var, tmpRelationArray,
1830                        &vectorT, &cubeT, &newRelationArray,
1831                        NIL(mdd_t *), NIL(mdd_t *), TRUE);
1832  } else {
1833    vectorT = NIL(array_t);
1834    cubeT = NIL(mdd_t);
1835    newRelationArray = tmpRelationArray;
1836  }
1837  fromT = bdd_cofactor(from, var);
1838  relationArrayT = ImgGetCofactoredRelationArray(newRelationArray, var);
1839  if (relationArray && newRelationArray != tmpRelationArray)
1840    mdd_array_free(newRelationArray);
1841  if (!bdd_is_tautology(fromT, 0)) {
1842    resT = ImageByStaticInputSplit(info, vectorT, fromT,
1843                             relationArrayT, turnDepth, depth + 1);
1844    if (findEssential)
1845      foundEssentialDepthT = info->foundEssentialDepth;
1846    if (vectorT) {
1847      ImgVectorFree(vectorT);
1848      if (!bdd_is_tautology(cubeT, 1)) {
1849        tmp = resT;
1850        resT = mdd_and(tmp, cubeT, 1, 1);
1851        mdd_free(tmp);
1852      }
1853      mdd_free(cubeT);
1854    }
1855    nRecur++;
1856  } else {
1857    resT = mdd_zero(info->manager);
1858    if (vectorT) {
1859      ImgVectorFree(vectorT);
1860      mdd_free(cubeT);
1861    }
1862  }
1863  mdd_free(fromT);
1864  mdd_array_free(relationArrayT);
1865
1866  if (bdd_is_tautology(resT, 1)) {
1867    mdd_free(var);
1868    if (vector && newRelationArray != relationArray)
1869      mdd_array_free(newRelationArray);
1870    res = resT;
1871    info->nEmptySubImage++;
1872  } else {
1873    varNot = mdd_not(var);
1874    mdd_free(var);
1875    if (tmpVector) {
1876      ImgVectorConstrain(info, tmpVector, varNot, tmpRelationArray,
1877                         &vectorE, &cubeE, &newRelationArray,
1878                         NIL(mdd_t *), NIL(mdd_t *), TRUE);
1879    } else {
1880      vectorE = NIL(array_t);
1881      cubeE = NIL(mdd_t);
1882      newRelationArray = tmpRelationArray;
1883    }
1884    fromE = bdd_cofactor(from, varNot);
1885    relationArrayE = ImgGetCofactoredRelationArray(newRelationArray, varNot);
1886    if (vector && newRelationArray != tmpRelationArray)
1887      mdd_array_free(newRelationArray);
1888    if (!bdd_is_tautology(fromE, 0)) {
1889      resE = ImageByStaticInputSplit(info, vectorE, fromE,
1890                               relationArrayE, turnDepth, depth + 1);
1891      if (findEssential)
1892        foundEssentialDepthE = info->foundEssentialDepth;
1893      if (vectorE) {
1894        ImgVectorFree(vectorE);
1895        if (!bdd_is_tautology(cubeE, 1)) {
1896          tmp = resE;
1897          resE = mdd_and(tmp, cubeE, 1, 1);
1898          mdd_free(tmp);
1899        }
1900        mdd_free(cubeE);
1901      }
1902      nRecur++;
1903    } else {
1904      resE = mdd_zero(info->manager);
1905      if (vectorE) {
1906        ImgVectorFree(vectorE);
1907        mdd_free(cubeE);
1908      }
1909    }
1910    mdd_free(fromE);
1911    mdd_array_free(relationArrayE);
1912   
1913    res = mdd_or(resT, resE, 1, 1);
1914    if (info->option->verbosity) {
1915      size = bdd_size(res);
1916      if (size > info->maxIntermediateSize)
1917        info->maxIntermediateSize = size;
1918      if (info->option->printBddSize) {
1919        fprintf(vis_stdout, "** tfm info: bdd_or(%d,%d) = %d\n",
1920                bdd_size(resT), bdd_size(resE), size);
1921      }
1922    }
1923    mdd_free(resT);
1924    mdd_free(resE);
1925    mdd_free(varNot);
1926  }
1927
1928  if (tmpVector && tmpVector != vector)
1929    ImgVectorFree(tmpVector);
1930  if (tmpRelationArray && tmpRelationArray != relationArray)
1931    mdd_array_free(tmpRelationArray);
1932
1933  if (and_) {
1934    tmp = res;
1935    res = mdd_and(tmp, and_, 1, 1);
1936    if (info->option->verbosity) {
1937      size = bdd_size(res);
1938      if (size > info->maxIntermediateSize)
1939        info->maxIntermediateSize = size;
1940      if (info->option->printBddSize) {
1941        fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
1942                bdd_size(tmp), bdd_size(and_), size);
1943      }
1944    }
1945    mdd_free(tmp);
1946  }
1947
1948  if (info->option->debug) {
1949    refResult = ImgImageByHybridWithStaticSplit(info, vector, from,
1950                                                relationArray,
1951                                                NIL(mdd_t), NIL(mdd_t));
1952    assert(mdd_equal(refResult, res));
1953    mdd_free(refResult);
1954  }
1955
1956  if (nRecur == 0) {
1957    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
1958                          (float)depth) / (float)(info->nLeaves + 1);
1959    if (depth > info->maxDepth)
1960      info->maxDepth = depth;
1961    info->nLeaves++;
1962  }
1963
1964  if (findEssential) {
1965    if (foundEssentialDepth == info->option->maxEssentialDepth) {
1966      if (foundEssentialDepthT < foundEssentialDepthE)
1967        foundEssentialDepth = foundEssentialDepthT;
1968      else
1969        foundEssentialDepth = foundEssentialDepthE;
1970    }
1971    info->foundEssentialDepth = foundEssentialDepth;
1972  }
1973  return(res);
1974}
1975
1976
1977/**Function********************************************************************
1978
1979  Synopsis    [Computes an image by output splitting.]
1980
1981  Description [Computes an image by output splitting.]
1982
1983  SideEffects []
1984
1985******************************************************************************/
1986static mdd_t *
1987ImageByOutputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint,
1988                   int depth)
1989{
1990  array_t               *newVector;
1991  mdd_t                 *new_, *resT, *resE, *res, *resPart;
1992  mdd_t                 *constrain, *tmp, *func;
1993  int                   size, i, vectorSize;
1994  array_t               *vectorArray, *varArray;
1995  ImgComponent_t        *comp;
1996  int                   hit;
1997  int                   split, nGroups;
1998  mdd_t                 *product, *refResult;
1999
2000  ImgVectorConstrain(info, vector, constraint, NIL(array_t),
2001                     &newVector, &res, NIL(array_t *),
2002                     NIL(mdd_t *), NIL(mdd_t *), FALSE);
2003
2004  info->nRecursion++;
2005  if (info->nIntermediateVars)
2006    size = ImgVectorFunctionSize(newVector);
2007  else
2008    size = array_n(newVector);
2009  if (size <= 1) {
2010    ImgVectorFree(newVector);
2011    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
2012                          (float)depth) / (float)(info->nLeaves + 1);
2013    if (depth > info->maxDepth)
2014      info->maxDepth = depth;
2015    info->nLeaves++;
2016    return(res);
2017  }
2018
2019  if (size == 2) {
2020    hit = 1;
2021    if (!info->imgCache ||
2022        !(resPart = ImgCacheLookupTable(info, info->imgCache, newVector,
2023                                        NIL(bdd_t)))) {
2024      hit = 0;
2025      resPart = ImageFast2(info, newVector);
2026      if (info->imgCache)
2027        ImgCacheInsertTable(info->imgCache, newVector, NIL(bdd_t), resPart);
2028    }
2029
2030    if (info->option->debug) {
2031      refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
2032      assert(mdd_equal(refResult, resPart));
2033      mdd_free(refResult);
2034    }
2035    new_ = mdd_and(res, resPart, 1, 1);
2036    if (info->option->verbosity) {
2037      size = bdd_size(new_);
2038      if (size > info->maxIntermediateSize)
2039        info->maxIntermediateSize = size;
2040      if (info->option->printBddSize) {
2041        fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
2042                bdd_size(res), bdd_size(resPart), size);
2043      }
2044    }
2045    mdd_free(res);
2046    if (!info->imgCache || hit) {
2047      mdd_free(resPart);
2048      ImgVectorFree(newVector);
2049    }
2050    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
2051                          (float)depth) / (float)(info->nLeaves + 1);
2052    if (depth > info->maxDepth)
2053      info->maxDepth = depth;
2054    info->nLeaves++;
2055    return(new_);
2056  }
2057
2058  if (info->imgCache) {
2059    resPart = ImgCacheLookupTable(info, info->imgCache, newVector, NIL(mdd_t));
2060    if (resPart) {
2061      if (info->option->debug) {
2062        refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
2063        assert(mdd_equal(refResult, resPart));
2064        mdd_free(refResult);
2065      }
2066      new_ = mdd_and(res, resPart, 1, 1);
2067      if (info->option->verbosity) {
2068        size = bdd_size(new_);
2069        if (size > info->maxIntermediateSize)
2070          info->maxIntermediateSize = size;
2071        if (info->option->printBddSize) {
2072          fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
2073                  bdd_size(res), bdd_size(resPart), size);
2074        }
2075      }
2076      mdd_free(res);
2077      mdd_free(resPart);
2078      res = new_;
2079      ImgVectorFree(newVector);
2080      return(res);
2081    }
2082  }
2083
2084  /* compute disconnected component and best variable selection */
2085  vectorArray = array_alloc(array_t *, 0);
2086  varArray = array_alloc(array_t *, 0);
2087  nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, NIL(mdd_t), 1,
2088                                            info->option->outputSplit, 0,
2089                                            vectorArray, varArray, &product,
2090                                            NIL(array_t), NIL(array_t *),
2091                                            NIL(mdd_t *), NIL(mdd_t *));
2092  vectorSize = array_n(newVector);
2093  if ((!info->imgCache || nGroups <= 1) && !info->option->debug)
2094    ImgVectorFree(newVector);
2095  if (nGroups == 0) {
2096    array_free(vectorArray);
2097    array_free(varArray);
2098
2099    if (info->option->debug) {
2100      refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
2101      assert(mdd_equal(refResult, product));
2102      mdd_free(refResult);
2103      ImgVectorFree(newVector);
2104    }
2105
2106    new_ = mdd_and(res, product, 1, 1);
2107    if (info->option->verbosity) {
2108      size = bdd_size(new_);
2109      if (size > info->maxIntermediateSize)
2110        info->maxIntermediateSize = size;
2111      if (info->option->printBddSize) {
2112        fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
2113                bdd_size(res), bdd_size(product), size);
2114      }
2115    }
2116    mdd_free(res);
2117    mdd_free(product);
2118    res = new_;
2119
2120    info->averageDepth = (info->averageDepth * (float)info->nLeaves +
2121                          (float)depth) / (float)(info->nLeaves + 1);
2122    if (depth > info->maxDepth)
2123      info->maxDepth = depth;
2124    info->nLeaves++;
2125    return(res);
2126  } else if (nGroups > 1) {
2127    if (info->nDecomps == 0 || depth < info->topDecomp)
2128      info->topDecomp = depth;
2129    if (info->nDecomps == 0 || vectorSize > info->maxDecomp)
2130      info->maxDecomp = vectorSize;
2131    info->averageDecomp = (info->averageDecomp * (float)info->nDecomps +
2132                          (float)nGroups) / (float)(info->nDecomps + 1);
2133    info->nDecomps++;
2134  }
2135
2136  product = mdd_one(info->manager);
2137  for (i = 0; i < array_n(vectorArray); i++) {
2138    vector = array_fetch(array_t *, vectorArray, i);
2139
2140    hit = 1;
2141    if (!info->imgCache || nGroups == 1 ||
2142        !(resPart = ImgCacheLookupTable(info, info->imgCache, vector,
2143                                        NIL(bdd_t)))) {
2144      hit = 0;
2145      if (info->nIntermediateVars)
2146        size = ImgVectorFunctionSize(vector);
2147      else
2148        size = array_n(vector);
2149      if (size == 1) {
2150        comp = array_fetch(ImgComponent_t *, vector, 0);
2151        if (array_n(vector) > 1)
2152          func = ImgGetComposedFunction(vector);
2153        else
2154          func = comp->func;
2155        if (bdd_is_tautology(func, 1))
2156          resPart = mdd_dup(comp->var);
2157        else if (bdd_is_tautology(func, 0))
2158          resPart = mdd_not(comp->var);
2159        else
2160          resPart = mdd_one(info->manager);
2161        if (array_n(vector) > 1)
2162          mdd_free(func);
2163        info->averageDepth = (info->averageDepth * (float)info->nLeaves +
2164                                (float)depth) / (float)(info->nLeaves + 1);
2165        if (depth > info->maxDepth)
2166          info->maxDepth = depth;
2167        info->nLeaves++;
2168      } else if (size == 2) {
2169        resPart = ImageFast2(info, vector);
2170        info->averageDepth = (info->averageDepth * (float)info->nLeaves +
2171                                (float)depth) / (float)(info->nLeaves + 1);
2172        if (depth > info->maxDepth)
2173          info->maxDepth = depth;
2174        info->nLeaves++;
2175      } else {
2176        split = array_fetch(int, varArray, i);
2177        comp = array_fetch(ImgComponent_t *, vector, split);
2178        constrain = comp->func;
2179        resT = ImageByOutputSplit(info, vector, constrain, depth + 1);
2180        tmp = mdd_not(constrain);
2181        resE = ImageByOutputSplit(info, vector, tmp, depth + 1);
2182        mdd_free(tmp);
2183 
2184        resPart = bdd_ite(comp->var, resT, resE, 1, 1, 1);
2185        if (info->option->verbosity) {
2186          size = bdd_size(resPart);
2187          if (size > info->maxIntermediateSize)
2188            info->maxIntermediateSize = size;
2189          if (info->option->printBddSize) {
2190            fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n",
2191                    bdd_size(resT), bdd_size(resE), size);
2192          }
2193        }
2194        mdd_free(resT);
2195        mdd_free(resE);
2196      }
2197      if (info->imgCache)
2198        ImgCacheInsertTable(info->imgCache, vector, NIL(bdd_t), resPart);
2199    }
2200    if (!info->imgCache || hit)
2201      ImgVectorFree(vector);
2202    new_ = mdd_and(product, resPart, 1, 1);
2203    if (info->option->verbosity) {
2204      size = bdd_size(new_);
2205      if (size > info->maxIntermediateSize)
2206        info->maxIntermediateSize = size;
2207      if (info->option->printBddSize) {
2208        fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
2209                bdd_size(product), bdd_size(resPart), size);
2210      }
2211    }
2212    mdd_free(product);
2213    if (!info->imgCache || hit)
2214      mdd_free(resPart);
2215    product = new_;
2216  }
2217
2218  array_free(vectorArray);
2219  array_free(varArray);
2220
2221  if (info->imgCache && nGroups > 1) {
2222    ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t),
2223                        mdd_dup(product));
2224  }
2225
2226  if (info->option->debug) {
2227    refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t));
2228    assert(mdd_equal(refResult, product));
2229    mdd_free(refResult);
2230    if (!info->imgCache || nGroups == 1)
2231      ImgVectorFree(newVector);
2232  }
2233
2234  new_ = mdd_and(res, product, 1, 1);
2235  if (info->option->verbosity) {
2236    size = bdd_size(new_);
2237    if (size > info->maxIntermediateSize)
2238      info->maxIntermediateSize = size;
2239    if (info->option->printBddSize) {
2240      fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n",
2241              bdd_size(res), bdd_size(product), size);
2242    }
2243  }
2244  mdd_free(res);
2245  mdd_free(product);
2246  res = new_;
2247
2248  return(res);
2249}
2250
2251
2252/**Function********************************************************************
2253
2254  Synopsis    [Try to decompose function vector and find a splitting variable
2255  for each decomposed block.]
2256
2257  Description [Try to decompose function vector and find a splitting variable
2258  for each decomposed block.]
2259
2260  SideEffects []
2261
2262******************************************************************************/
2263static int
2264ImageDecomposeAndChooseSplitVar(ImgTfmInfo_t *info, array_t *vector,
2265                                mdd_t *from, int splitMethod, int split,
2266                                int piSplitFlag,
2267                                array_t *vectorArray, array_t *varArray,
2268                                mdd_t **singles, array_t *relationArray,
2269                                array_t **newRelationArray,
2270                                mdd_t **cofactorCube, mdd_t **abstractCube)
2271{
2272  int                   i, j, f, index;
2273  int                   nGroups, nSingles, nChosen;
2274  int                   nVars, nFuncs, arraySize;
2275  char                  *varFlag;
2276  int                   *funcGroup;
2277  int                   *varOccur;
2278  int                   bestVar;
2279  int                   *stack, size;
2280  ImgComponent_t        *comp, *newComp;
2281  array_t               *partVector;
2282  char                  *stackFlag;
2283  char                  *support;
2284  mdd_t                 *func;
2285  int                   *varCost;
2286  int                   decompose;
2287  int                   res, constConstrain;
2288  mdd_t                 *tmp, *cofactor, *abstract, *nsVar;
2289  array_t               *tmpRelationArray;
2290  char                  *intermediateVarFlag;
2291  int                   *intermediateVarFuncMap;
2292
2293  if (info->useConstraint && from && splitMethod == 0)
2294    decompose = 0;
2295  else
2296    decompose = 1;
2297
2298  arraySize = array_n(vector);
2299  if (info->nIntermediateVars)
2300    nFuncs = ImgVectorFunctionSize(vector);
2301  else
2302    nFuncs = arraySize;
2303  nVars = info->nVars;
2304
2305  *singles = mdd_one(info->manager);
2306  if (relationArray) {
2307    cofactor = mdd_one(info->manager);
2308    abstract = mdd_one(info->manager);
2309  } else {
2310    cofactor = NIL(mdd_t);
2311    abstract = NIL(mdd_t);
2312  }
2313
2314  if (decompose) {
2315    funcGroup = ALLOC(int, arraySize);
2316    memset(funcGroup, 0, sizeof(int) * arraySize);
2317    varFlag = ALLOC(char, nVars);
2318    memset(varFlag, 0, sizeof(char) * nVars);
2319    stack = ALLOC(int, arraySize);
2320    stackFlag = ALLOC(char, arraySize);
2321    memset(stackFlag, 0, sizeof(char) * arraySize);
2322    if (arraySize > nFuncs) {
2323      intermediateVarFlag = ALLOC(char, nVars);
2324      memset(intermediateVarFlag, 0, sizeof(char) * nVars);
2325      intermediateVarFuncMap = ALLOC(int, nVars);
2326      memset(intermediateVarFuncMap, 0, sizeof(int) * nVars);
2327      for (i = 0; i < arraySize; i++) {
2328        comp = array_fetch(ImgComponent_t *, vector, i);
2329        if (comp->intermediate) {
2330          index = (int)bdd_top_var_id(comp->var);
2331          intermediateVarFlag[index] = 1;
2332          intermediateVarFuncMap[index] = i;
2333        }
2334      }
2335    } else {
2336      /* To remove compiler warnings */
2337      intermediateVarFlag = NIL(char);
2338      intermediateVarFuncMap = NIL(int);
2339    }
2340  } else {
2341    /* To remove compiler warnings */
2342    funcGroup = NIL(int);
2343    varFlag = NIL(char);
2344    stack = NIL(int);
2345    stackFlag = NIL(char);
2346    intermediateVarFlag = NIL(char);
2347    intermediateVarFuncMap = NIL(int);
2348  }
2349  varOccur = ALLOC(int, nVars);
2350  if (splitMethod == 0 && split > 0)
2351    varCost = ALLOC(int, nVars);
2352  else
2353    varCost = NIL(int);
2354
2355  nGroups = 0;
2356  nSingles = 0;
2357  nChosen = 0;
2358  while (nChosen < nFuncs) {
2359    bestVar = -1;
2360    memset(varOccur, 0, sizeof(int) * nVars);
2361    if (varCost)
2362      memset(varCost, 0, sizeof(int) * nVars);
2363
2364    if (decompose) {
2365      size = 0;
2366      for (i = 0; i < arraySize; i++) {
2367        if (funcGroup[i] == 0) {
2368          stack[0] = i;
2369          size = 1;
2370          stackFlag[i] = 1;
2371          break;
2372        }
2373      }
2374      assert(size == 1);
2375 
2376      while (size) {
2377        size--;
2378        f = stack[size];
2379        funcGroup[f] = nGroups + 1;
2380        comp = array_fetch(ImgComponent_t *, vector, f);
2381        nChosen++;
2382        if (nChosen == arraySize)
2383          break;
2384        support = comp->support;
2385        if (comp->intermediate) {
2386          index = (int)bdd_top_var_id(comp->var);
2387          support[index] = 1;
2388        }
2389        for (i = 0; i < nVars; i++) {
2390          if (!support[i])
2391            continue;
2392          varOccur[i]++;
2393          if (varFlag[i])
2394            continue;
2395          varFlag[i] = 1;
2396          for (j = 0; j < arraySize; j++) {
2397            if (j == f || stackFlag[j])
2398              continue;
2399            comp = array_fetch(ImgComponent_t *, vector, j);
2400            if (arraySize != nFuncs) {
2401              if (intermediateVarFlag[i] && comp->intermediate) {
2402                index = (int)bdd_top_var_id(comp->var);
2403                if (index == i) {
2404                  if (funcGroup[j] == 0) {
2405                    stack[size] = j;
2406                    size++;
2407                    stackFlag[j] = 1;
2408                  }
2409                  FindIntermediateSupport(vector, comp, nVars, nGroups,
2410                                          stack, stackFlag, funcGroup, &size,
2411                                          intermediateVarFlag,
2412                                          intermediateVarFuncMap);
2413                  continue;
2414                }
2415              }
2416            }
2417            if (funcGroup[j])
2418              continue;
2419            if (comp->support[i]) {
2420              stack[size] = j;
2421              size++;
2422              stackFlag[j] = 1;
2423            }
2424          }
2425        }
2426        if (comp->intermediate) {
2427          index = (int)bdd_top_var_id(comp->var);
2428          support[index] = 0;
2429        }
2430      }
2431    } else {
2432      for (i = 0; i < arraySize; i++) {
2433        comp = array_fetch(ImgComponent_t *, vector, i);
2434        support = comp->support;
2435        for (j = 0; j < nVars; j++) {
2436          if (support[j])
2437            varOccur[j]++;
2438        }
2439      }
2440      nChosen = nFuncs;
2441    }
2442
2443    nGroups++;
2444
2445    /* Collect the functions which belong to the current group */
2446    partVector = array_alloc(ImgComponent_t *, 0);
2447    for (i = 0; i < arraySize; i++) {
2448      if (decompose == 0 || funcGroup[i] == nGroups) {
2449        comp = array_fetch(ImgComponent_t *, vector, i);
2450        newComp = ImgComponentCopy(info, comp);
2451        array_insert_last(ImgComponent_t *, partVector, newComp);
2452      }
2453    }
2454    if (arraySize == nFuncs)
2455      size = array_n(partVector);
2456    else
2457      size = ImgVectorFunctionSize(partVector);
2458    if (size == 1) {
2459      nSingles++;
2460      if (size == array_n(partVector)) {
2461        comp = array_fetch(ImgComponent_t *, partVector, 0);
2462        func = comp->func;
2463      } else {
2464        comp = ImgGetLatchComponent(partVector);
2465        func = ImgGetComposedFunction(partVector);
2466      }
2467      if (from) {
2468        constConstrain = ImgConstConstrain(func, from);
2469        if (constConstrain == 1)
2470          res = 1;
2471        else if (constConstrain == 0)
2472          res = 0;
2473        else
2474          res = 2;
2475      } else {
2476        if (bdd_is_tautology(func, 1))
2477          res = 1;
2478        else if (bdd_is_tautology(func, 0))
2479          res = 0;
2480        else
2481          res = 2;
2482      }
2483      if (size != array_n(partVector))
2484        mdd_free(func);
2485      if (res == 1) {
2486        tmp = *singles;
2487        *singles = mdd_and(tmp, comp->var, 1, 1);
2488        mdd_free(tmp);
2489      } else if (res == 0) {
2490        tmp = *singles;
2491        *singles = mdd_and(tmp, comp->var, 1, 0);
2492        mdd_free(tmp);
2493      }
2494      if (abstract) {
2495        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
2496        tmp = abstract;
2497        abstract = mdd_and(tmp, nsVar, 1, 1);
2498        mdd_free(tmp);
2499        mdd_free(nsVar);
2500      }
2501
2502      ImgVectorFree(partVector);
2503      continue;
2504    }
2505
2506    array_insert_last(array_t *, vectorArray, partVector);
2507
2508    if (splitMethod == 0) { /* input splitting */
2509      if (decompose) {
2510        if (info->option->findDecompVar) {
2511          bestVar = FindDecomposableVariable(info, partVector);
2512          if (bestVar != -1)
2513            split = -1;
2514        }
2515      } else if (from) {
2516        comp = ImgComponentAlloc(info);
2517        comp->func = from;
2518        ImgComponentGetSupport(comp);
2519        for (i = 0; i < nVars; i++) {
2520          if (comp->support[i])
2521            varOccur[i]++;
2522        }
2523        comp->func = NIL(mdd_t);
2524        ImgComponentFree(comp);
2525      }
2526
2527      if (split != -1) {
2528        bestVar = ChooseInputSplittingVariable(info, partVector, from,
2529                        info->option->inputSplit, decompose,
2530                        info->option->piSplitFlag, varOccur);
2531
2532      }
2533    } else { /* output splitting */
2534      bestVar = ChooseOutputSplittingVariable(info, partVector,
2535                        info->option->outputSplit);
2536    }
2537    assert(bestVar != -1);
2538    array_insert_last(int, varArray, bestVar);
2539  }
2540
2541  if (newRelationArray)
2542    *newRelationArray = relationArray;
2543  if (cofactorCube && abstractCube) {
2544    if (cofactor)
2545      *cofactorCube = cofactor;
2546    if (abstract)
2547      *abstractCube = abstract;
2548  } else {
2549    if (cofactor) {
2550      if (bdd_is_tautology(cofactor, 1))
2551        mdd_free(cofactor);
2552      else {
2553        *newRelationArray = ImgGetCofactoredRelationArray(relationArray,
2554                                                          cofactor);
2555        mdd_free(cofactor);
2556      }
2557    }
2558    if (abstract) {
2559      if (bdd_is_tautology(abstract, 1))
2560        mdd_free(abstract);
2561      else {
2562        tmpRelationArray = *newRelationArray;
2563        *newRelationArray = ImgGetAbstractedRelationArray(info->manager,
2564                                                          tmpRelationArray,
2565                                                          abstract);
2566        mdd_free(abstract);
2567        if (tmpRelationArray != relationArray)
2568          mdd_array_free(tmpRelationArray);
2569      }
2570    }
2571  }
2572
2573  if (decompose) {
2574    FREE(stackFlag);
2575    FREE(stack);
2576    FREE(funcGroup);
2577    FREE(varFlag);
2578    if (arraySize > nFuncs) {
2579      FREE(intermediateVarFlag);
2580      FREE(intermediateVarFuncMap);
2581    }
2582  }
2583  FREE(varOccur);
2584  if (varCost)
2585    FREE(varCost);
2586  nGroups -= nSingles;
2587  return(nGroups);
2588}
2589
2590
2591/**Function********************************************************************
2592
2593  Synopsis    [Fast image computation when function vector contains only two
2594  functions.]
2595
2596  Description [Fast image computation when function vector contains only two
2597  functions.]
2598
2599  SideEffects []
2600
2601******************************************************************************/
2602static mdd_t *
2603ImageFast2(ImgTfmInfo_t *info, array_t *vector)
2604{
2605  mdd_t                 *f1, *f2;
2606  int                   f21n, f21p;
2607  mdd_t                 *res, *resp, *resn;
2608  mdd_t                 *i1, *i2;
2609  ImgComponent_t        *comp;
2610  mdd_t                 *refResult;
2611  int                   i, freeFlag, size;
2612  array_t               *varArray, *funcArray;
2613
2614  assert(ImgVectorFunctionSize(vector) == 2);
2615
2616  if (info->option->debug)
2617    refResult = ImgImageByHybrid(info, vector, NIL(mdd_t));
2618  else
2619    refResult = NIL(mdd_t);
2620
2621  if (array_n(vector) == 2) {
2622    comp = array_fetch(ImgComponent_t *, vector, 0);
2623    f1 = comp->func;
2624    i1 = comp->var;
2625
2626    comp = array_fetch(ImgComponent_t *, vector, 1);
2627    f2 = comp->func;
2628    i2 = comp->var;
2629
2630    freeFlag = 0;
2631  } else {
2632    varArray = array_alloc(mdd_t *, 0);
2633    funcArray = array_alloc(mdd_t *, 0);
2634
2635    i1 = NIL(mdd_t);
2636    i2 = NIL(mdd_t);
2637    f1 = NIL(mdd_t);
2638    f2 = NIL(mdd_t);
2639
2640    for (i = 0; i < array_n(vector); i++) {
2641      comp = array_fetch(ImgComponent_t *, vector, i);
2642      if (comp->intermediate) {
2643        array_insert_last(mdd_t *, varArray, comp->var);
2644        array_insert_last(mdd_t *, funcArray, comp->func);
2645        continue;
2646      }
2647      if (f1) {
2648        f2 = comp->func;
2649        i2 = comp->var;
2650      } else {
2651        f1 = comp->func;
2652        i1 = comp->var;
2653      }
2654    }
2655
2656    f1 = bdd_vector_compose(f1, varArray, funcArray);
2657    f2 = bdd_vector_compose(f2, varArray, funcArray);
2658    array_free(varArray);
2659    array_free(funcArray);
2660    freeFlag = 1;
2661  }
2662
2663  ImgCheckConstConstrain(f1, f2, &f21p, &f21n);
2664
2665  if (f21p == 1)
2666    resp = mdd_dup(i2);
2667  else if (f21p == 0)
2668    resp = mdd_not(i2);
2669  else
2670    resp = mdd_one(info->manager);
2671
2672  if (f21n == 1)
2673    resn = mdd_dup(i2);
2674  else if (f21n == 0)
2675    resn = mdd_not(i2);
2676  else
2677    resn = mdd_one(info->manager);
2678
2679  /* merge final result */
2680  res = bdd_ite(i1, resp, resn, 1, 1, 1);
2681  if (info->option->verbosity) {
2682    size = bdd_size(res);
2683    if (size > info->maxIntermediateSize)
2684      info->maxIntermediateSize = size;
2685    if (info->option->printBddSize) {
2686      fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n",
2687                bdd_size(resp), bdd_size(resn), size);
2688    }
2689  }
2690  mdd_free(resp);
2691  mdd_free(resn);
2692  if (freeFlag) {
2693    mdd_free(f1);
2694    mdd_free(f2);
2695  }
2696
2697  if (info->option->debug) {
2698    assert(mdd_equal(refResult, res));
2699    mdd_free(refResult);
2700  }
2701
2702  return(res);
2703}
2704
2705
2706/**Function********************************************************************
2707
2708  Synopsis    [Finds a decomposable variable (articulation)]
2709
2710  Description [Finds a decomposable variable (articulation)]
2711
2712  SideEffects []
2713
2714******************************************************************************/
2715static int
2716FindDecomposableVariable(ImgTfmInfo_t *info, array_t *vector)
2717{
2718  int                   i, j, f, split;
2719  int                   nChosen, index, varId;
2720  int                   nVars, nFuncs;
2721  char                  *varFlag;
2722  int                   *funcGroup;
2723  int                   *stack, size;
2724  ImgComponent_t        *comp;
2725  char                  *stackFlag;
2726  char                  *support;
2727  int                   arraySize;
2728  char                  *intermediateVarFlag;
2729  int                   *intermediateVarFuncMap;
2730
2731  arraySize = array_n(vector);
2732  if (info->nIntermediateVars)
2733    nFuncs = ImgVectorFunctionSize(vector);
2734  else
2735    nFuncs = arraySize;
2736  nVars = info->nVars;
2737
2738  funcGroup = ALLOC(int, arraySize);
2739  varFlag = ALLOC(char, nVars);
2740  stack = ALLOC(int, arraySize);
2741  stackFlag = ALLOC(char, arraySize);
2742
2743  if (arraySize > nFuncs) {
2744    intermediateVarFlag = ALLOC(char, nVars);
2745    memset(intermediateVarFlag, 0, sizeof(char) * nVars);
2746    intermediateVarFuncMap = ALLOC(int, nVars);
2747    memset(intermediateVarFuncMap, 0, sizeof(int) * nVars);
2748    for (i = 0; i < arraySize; i++) {
2749      comp = array_fetch(ImgComponent_t *, vector, i);
2750      if (comp->intermediate) {
2751        index = (int)bdd_top_var_id(comp->var);
2752        intermediateVarFlag[index] = 1;
2753        intermediateVarFuncMap[index] = i;
2754      }
2755    }
2756  } else {
2757    intermediateVarFlag = NIL(char);
2758    intermediateVarFuncMap = NIL(int);
2759  }
2760
2761  varId = -1;
2762  for (split = 0; split < nVars; split++) {
2763    if (intermediateVarFlag[split])
2764      continue;
2765
2766    memset(funcGroup, 0, sizeof(int) * arraySize);
2767    memset(varFlag, 0, sizeof(char) * nVars);
2768    memset(stackFlag, 0, sizeof(char) * arraySize);
2769
2770    varFlag[split] = 1;
2771    nChosen = 0;
2772 
2773    stack[0] = 0;
2774    size = 1;
2775    stackFlag[0] = 1;
2776 
2777    while (size) {
2778      size--;
2779      f = stack[size];
2780      funcGroup[f] = 1;
2781      comp = array_fetch(ImgComponent_t *, vector, f);
2782      nChosen++;
2783      if (nChosen == arraySize)
2784        break;
2785      support = comp->support;
2786      if (comp->intermediate) {
2787        index = (int)bdd_top_var_id(comp->var);
2788        support[index] = 1;
2789      }
2790      for (i = 0; i < nVars; i++) {
2791        if (!support[i])
2792          continue;
2793        if (varFlag[i])
2794          continue;
2795        varFlag[i] = 1;
2796        for (j = 0; j < nFuncs; j++) {
2797          if (j == f || stackFlag[j])
2798            continue;
2799          comp = array_fetch(ImgComponent_t *, vector, j);
2800          if (arraySize != nFuncs) {
2801            if (intermediateVarFlag[i] && comp->intermediate) {
2802              index = (int)bdd_top_var_id(comp->var);
2803              if (index == i) {
2804                if (funcGroup[j] == 0) {
2805                  stack[size] = j;
2806                  size++;
2807                  stackFlag[j] = 1;
2808                }
2809                FindIntermediateSupport(vector, comp, nVars, 0,
2810                                        stack, stackFlag, funcGroup, &size,
2811                                        intermediateVarFlag,
2812                                        intermediateVarFuncMap);
2813                continue;
2814              }
2815            }
2816          }
2817          if (funcGroup[j])
2818            continue;
2819          if (comp->support[i]) {
2820            stack[size] = j;
2821            size++;
2822            stackFlag[j] = 1;
2823          }
2824        }
2825      }
2826      if (comp->intermediate) {
2827        index = (int)bdd_top_var_id(comp->var);
2828        support[index] = 0;
2829      }
2830    }
2831
2832    if (nChosen < nFuncs) {
2833      varId = split;
2834      break;
2835    }
2836  }
2837
2838  FREE(stackFlag);
2839  FREE(stack);
2840  FREE(funcGroup);
2841  FREE(varFlag);
2842  if (arraySize > nFuncs) {
2843    FREE(intermediateVarFlag);
2844    FREE(intermediateVarFuncMap);
2845  }
2846
2847  return(varId);
2848}
2849
2850
2851/**Function********************************************************************
2852
2853  Synopsis    [Checks the support of image.]
2854
2855  Description [Checks the support of image.]
2856
2857  SideEffects []
2858
2859******************************************************************************/
2860static int
2861TfmCheckImageValidity(ImgTfmInfo_t *info, mdd_t *image)
2862{
2863  int           i, id;
2864  array_t       *supportIds;
2865  int           status = 1;
2866
2867  supportIds = mdd_get_bdd_support_ids(info->manager, image);
2868  for (i = 0; i < array_n(supportIds); i++) {
2869    id = array_fetch(int, supportIds, i);
2870    if (st_lookup(info->quantifyVarsTable, (char *)(long)id, NIL(char *))) {
2871      fprintf(vis_stderr,
2872              "** tfm error: image contains a primary input variable (%d)\n",
2873              id);
2874      status = 0;
2875    }
2876    if (st_lookup(info->rangeVarsTable, (char *)(long)id, NIL(char *))) {
2877      fprintf(vis_stderr,
2878              "** tfm error: image contains a range variable (%d)\n", id);
2879      status = 0;
2880    }
2881    if (info->intermediateVarsTable &&
2882        st_lookup(info->intermediateVarsTable, (char *)(long)id, NIL(char *))) {
2883      fprintf(vis_stderr,
2884              "** tfm error: image contains an intermediate variable (%d)\n",
2885              id);
2886      status = 0;
2887    }
2888  }
2889  array_free(supportIds);
2890  return(status);
2891}
2892
2893
2894/**Function********************************************************************
2895
2896  Synopsis    [Finds all other fanin intermediate functions of a given
2897  intermediate function.]
2898
2899  Description [Finds all other fanin intermediate functions of a given
2900  intermediate function. Adds the only intermediate functions are not in
2901  the stack. Updates the stack information.]
2902
2903  SideEffects []
2904
2905******************************************************************************/
2906static void
2907FindIntermediateSupport(array_t *vector, ImgComponent_t *comp,
2908                        int nVars, int nGroups,
2909                        int *stack, char *stackFlag, int *funcGroup, int *size,
2910                        char *intermediateVarFlag, int *intermediateVarFuncMap)
2911{
2912  int                   i, f;
2913  ImgComponent_t        *intermediateComp;
2914
2915  for (i = 0; i < nVars; i++) {
2916    if (comp->support[i]) {
2917      if (intermediateVarFlag[i]) {
2918        f = intermediateVarFuncMap[i];
2919        if (stackFlag[f] || funcGroup[f] == nGroups + 1)
2920          continue;
2921        stack[*size] = f;
2922        (*size)++;
2923        stackFlag[f] = 1;
2924
2925        intermediateComp = array_fetch(ImgComponent_t *, vector, f);
2926        FindIntermediateSupport(vector, intermediateComp, nVars, nGroups,
2927                                stack, stackFlag, funcGroup, size,
2928                                intermediateVarFlag, intermediateVarFuncMap);
2929      }
2930    }
2931  }
2932}
2933
2934
2935/**Function********************************************************************
2936
2937  Synopsis    [Print the information of the decomposition.]
2938
2939  Description [Print the information of the decomposition.]
2940
2941  SideEffects []
2942
2943******************************************************************************/
2944static void
2945PrintVectorDecomposition(ImgTfmInfo_t *info, array_t *vectorArray,
2946                         array_t *varArray)
2947{
2948  int                   i, j, n;
2949  int                   var, index;
2950  ImgComponent_t        *comp;
2951  array_t               *vector;
2952
2953  fprintf(vis_stdout, "** tfm info: vector decomposition\n");
2954  n = array_n(vectorArray);
2955  for (i = 0; i < n; i++) {
2956    vector = array_fetch(array_t *, vectorArray, i);
2957    var = array_fetch(int, varArray, i);
2958    fprintf(vis_stdout, "Group[%d] : num = %d, split = %d\n",
2959            i, array_n(vector), var);
2960    for (j = 0; j < array_n(vector); j++) {
2961      comp = array_fetch(ImgComponent_t *, vector, j);
2962      index = (int)bdd_top_var_id(comp->var);
2963      fprintf(vis_stdout, " %d", index);
2964    }
2965    fprintf(vis_stdout, "\n");
2966  }
2967}
2968
2969
2970/**Function********************************************************************
2971
2972  Synopsis    [Checks the splitting variable is valid and chooses new one
2973  if not valid.]
2974
2975  Description [Checks the splitting variable is already quantified from
2976  the transition relation. If yes, chooses new splitting variable. If there
2977  is no valid splitting variable, returns -1.]
2978
2979  SideEffects []
2980
2981******************************************************************************/
2982static int
2983CheckIfValidSplitOrGetNew(ImgTfmInfo_t *info, int split, array_t *vector,
2984                        array_t *relationArray, mdd_t *from)
2985{
2986  int newSplit = split;
2987  int i, j, nVars;
2988  ImgComponent_t *comp;
2989  char *support;
2990  int *varOccur;
2991  int decompose;
2992
2993  nVars = info->nVars;
2994  support = ALLOC(char, sizeof(char) * nVars);
2995  memset(support, 0, sizeof(char) * nVars);
2996
2997  comp = ImgComponentAlloc(info);
2998  for (i = 0; i < array_n(relationArray); i++) {
2999    comp->func = array_fetch(mdd_t *, relationArray, i);;
3000    ImgSupportClear(info, comp->support);
3001    ImgComponentGetSupport(comp);
3002    for (j = 0; j < nVars; j++) {
3003      if (comp->support[j]) {
3004        if (j == split) {
3005          comp->func = NIL(mdd_t);
3006          ImgComponentFree(comp);
3007          FREE(support);
3008          return(split);
3009        }
3010        support[j] = 1;
3011      }
3012    }
3013  }
3014
3015  comp->func = NIL(mdd_t);
3016  ImgComponentFree(comp);
3017
3018  if (info->useConstraint && from)
3019    decompose = 0;
3020  else
3021    decompose = 1;
3022
3023  varOccur = ALLOC(int, nVars);
3024  memset(varOccur, 0, sizeof(int) * nVars);
3025
3026  if (from) {
3027    comp = ImgComponentAlloc(info);
3028    comp->func = from;
3029    ImgComponentGetSupport(comp);
3030    for (i = 0; i < nVars; i++) {
3031      if (comp->support[i])
3032        varOccur[i]++;
3033    }
3034    comp->func = NIL(mdd_t);
3035    ImgComponentFree(comp);
3036  }
3037
3038  FREE(support);
3039
3040  newSplit = ChooseInputSplittingVariable(info, vector, from,
3041                info->option->inputSplit, decompose,
3042                info->option->piSplitFlag, varOccur);
3043
3044  FREE(varOccur);
3045
3046  return(newSplit);
3047}
3048
3049
3050/**Function********************************************************************
3051
3052  Synopsis    [Finds a splitting variable for input splitting.]
3053
3054  Description [Finds a splitting variable for input splitting.]
3055
3056  SideEffects []
3057
3058******************************************************************************/
3059static int
3060ChooseInputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, mdd_t *from,
3061                int splitMethod, int decompose, int piSplitFlag, int *varOccur)
3062{
3063  int nVars = info->nVars;
3064  int bestVar = -1;
3065  int secondBestVar = -1;
3066  int bestCost, newCost;
3067  int bestOccur, tieCount;
3068  int secondBestOccur, secondTieCount;
3069  int i, j;
3070  ImgComponent_t *comp;
3071  mdd_t *var, *varNot, *pcFunc, *ncFunc;
3072  int *varCost;
3073  int size = ImgVectorFunctionSize(vector);
3074
3075  if (info->option->inputSplit > 0) {
3076    varCost = ALLOC(int, nVars);
3077    memset(varCost, 0, sizeof(int) * nVars);
3078  } else
3079    varCost = NIL(int);
3080
3081  switch (splitMethod) {
3082  case 0:
3083    /* Find the most frequently occurred variable */
3084    bestOccur = 0;
3085    tieCount = 0;
3086    secondBestOccur = 0;
3087    secondTieCount = 0;
3088 
3089    for (i = 0; i < nVars; i++) {
3090      if (varOccur[i] == 0)
3091        continue;
3092      if (piSplitFlag == 0) {
3093        if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
3094                      NIL(char *))) {
3095          if ((bestOccur == 0 && secondBestOccur == 0) ||
3096              (varOccur[i] > bestOccur && varOccur[i] > secondBestOccur)) {
3097            secondBestOccur = varOccur[i];
3098            secondBestVar = i;
3099            secondTieCount = 1;
3100          } else if (secondBestOccur > bestOccur &&
3101                     varOccur[i] == secondBestOccur) {
3102            secondTieCount++;
3103            if (info->option->tieBreakMode == 0 &&
3104                bdd_get_level_from_id(info->manager, i) <
3105                bdd_get_level_from_id(info->manager, secondBestVar)) {
3106              secondBestVar = i;
3107            }
3108          }
3109          continue;
3110        }
3111      }
3112      if (size < array_n(vector) &&
3113          st_lookup(info->intermediateVarsTable, (char *)(long)i,
3114                    NIL(char *))) {
3115        continue;
3116      }
3117      if (bestOccur == 0 || varOccur[i] > bestOccur) {
3118        bestOccur = varOccur[i];
3119        bestVar = i;
3120        tieCount = 1;
3121      } else if (varOccur[i] == bestOccur) {
3122        tieCount++;
3123        if (info->option->tieBreakMode == 0 &&
3124            bdd_get_level_from_id(info->manager, i) <
3125            bdd_get_level_from_id(info->manager, bestVar)) {
3126          bestVar = i;
3127        }
3128      }
3129    }
3130
3131    if (piSplitFlag == 0 && bestVar == -1) {
3132      bestVar = secondBestVar;
3133      bestOccur = secondBestOccur;
3134      tieCount = secondTieCount;
3135    }
3136 
3137    if (info->option->tieBreakMode == 1 && tieCount > 1) {
3138      bestCost = IMG_TF_MAX_INT;
3139      for (i = bestVar; i < nVars; i++) {
3140        if (varOccur[i] != bestOccur)
3141          continue;
3142        if (size < array_n(vector) &&
3143            st_lookup(info->intermediateVarsTable, (char *)(long)i,
3144                      NIL(char *))) {
3145          continue;
3146        }
3147        var = bdd_var_with_index(info->manager, i);
3148        newCost = 0;
3149        for (j = 0; j < array_n(vector); j++) {
3150          comp = array_fetch(ImgComponent_t *, vector, j);
3151          newCost += bdd_estimate_cofactor(comp->func, var, 1);
3152          newCost += bdd_estimate_cofactor(comp->func, var, 0);
3153        }
3154        if (decompose == 0) {
3155          newCost += bdd_estimate_cofactor(from, var, 1);
3156          newCost += bdd_estimate_cofactor(from, var, 0);
3157        }
3158        mdd_free(var);
3159 
3160        if (newCost < bestCost) {
3161          bestVar = i;
3162          bestCost = newCost;
3163        } else if (newCost == bestCost) {
3164          if (bdd_get_level_from_id(info->manager, i) <
3165              bdd_get_level_from_id(info->manager, bestVar)) {
3166            bestVar = i;
3167          }
3168        }
3169      }
3170    }
3171    break;
3172  case 1:
3173    /* Find the variable which makes the smallest support after splitting */
3174    bestCost = IMG_TF_MAX_INT;
3175    for (i = 0; i < nVars; i++) {
3176      if (varOccur[i] == 0)
3177        continue;
3178      if (size < array_n(vector) &&
3179          st_lookup(info->intermediateVarsTable, (char *)(long)i,
3180                    NIL(char *))) {
3181        continue;
3182      }
3183      var = bdd_var_with_index(info->manager, i);
3184      varNot = mdd_not(var);
3185      for (j = 0; j < array_n(vector); j++) {
3186        comp = array_fetch(ImgComponent_t *, vector, j);
3187        pcFunc = bdd_cofactor(comp->func, var);
3188        varCost[i] += ImgCountBddSupports(pcFunc);
3189        mdd_free(pcFunc);
3190        ncFunc = bdd_cofactor(comp->func, varNot);
3191        varCost[i] += ImgCountBddSupports(ncFunc);
3192        mdd_free(ncFunc);
3193      }
3194      if (decompose == 0) {
3195        pcFunc = bdd_cofactor(from, var);
3196        varCost[i] += ImgCountBddSupports(pcFunc);
3197        mdd_free(pcFunc);
3198        ncFunc = bdd_cofactor(from, varNot);
3199        varCost[i] += ImgCountBddSupports(ncFunc);
3200        mdd_free(ncFunc);
3201      }
3202      mdd_free(var);
3203      mdd_free(varNot);
3204 
3205      if (varCost[i] < bestCost) {
3206        bestCost = varCost[i];
3207        bestVar = i;
3208      } else if (varCost[i] == bestCost) {
3209        if (varOccur[i] < varOccur[bestVar]) {
3210          bestVar = i;
3211        } else if (varOccur[i] == varOccur[bestVar]) {
3212          if (bdd_get_level_from_id(info->manager, i) <
3213              bdd_get_level_from_id(info->manager, bestVar)) {
3214            bestVar = i;
3215          }
3216        }
3217      }
3218    }
3219    break;
3220  case 2:
3221    /* Find the variable which makes the smallest BDDs of all functions
3222       after splitting */
3223    bestCost = IMG_TF_MAX_INT;
3224    for (i = 0; i < nVars; i++) {
3225      if (varOccur[i] == 0)
3226        continue;
3227      if (size < array_n(vector) &&
3228          st_lookup(info->intermediateVarsTable, (char *)(long)i,
3229                    NIL(char *))) {
3230        continue;
3231      }
3232      var = bdd_var_with_index(info->manager, i);
3233      for (j = 0; j < array_n(vector); j++) {
3234        comp = array_fetch(ImgComponent_t *, vector, j);
3235        varCost[i] += bdd_estimate_cofactor(comp->func, var, 1);
3236        varCost[i] += bdd_estimate_cofactor(comp->func, var, 0);
3237      }
3238      if (decompose == 0) {
3239        varCost[i] += bdd_estimate_cofactor(from, var, 1);
3240        varCost[i] += bdd_estimate_cofactor(from, var, 0);
3241      }
3242      mdd_free(var);
3243 
3244      if (varCost[i] < bestCost) {
3245        bestCost = varCost[i];
3246        bestVar = i;
3247      } else if (varCost[i] == bestCost) {
3248        if (varOccur[i] < varOccur[bestVar]) {
3249          bestVar = i;
3250        } else if (varOccur[i] == varOccur[bestVar]) {
3251          if (bdd_get_level_from_id(info->manager, i) <
3252              bdd_get_level_from_id(info->manager, bestVar)) {
3253            bestVar = i;
3254          }
3255        }
3256      }
3257    }
3258    break;
3259  case 3: /* top variable */
3260    for (i = 0; i < nVars; i++) {
3261      if (varOccur[i] == 0)
3262        continue;
3263      if (size < array_n(vector) &&
3264          st_lookup(info->intermediateVarsTable, (char *)(long)i,
3265                    NIL(char *))) {
3266        continue;
3267      }
3268      if (piSplitFlag == 0) {
3269        if (st_lookup(info->quantifyVarsTable, (char *)(long)i,
3270                      NIL(char *))) {
3271          if (bestVar == -1 && secondBestVar == -1)
3272            secondBestVar = i;
3273          else if (bdd_get_level_from_id(info->manager, i) <
3274                   bdd_get_level_from_id(info->manager, secondBestVar)) {
3275            secondBestVar = i;
3276          }
3277          continue;
3278        }
3279      }
3280      if (bestVar == -1 ||
3281          bdd_get_level_from_id(info->manager, i) <
3282          bdd_get_level_from_id(info->manager, bestVar)) {
3283        bestVar = i;
3284      }
3285    }
3286
3287    if (piSplitFlag == 0 && bestVar == -1)
3288      bestVar = secondBestVar;
3289    break;
3290  default:
3291    break;
3292  }
3293
3294  if (varCost)
3295    FREE(varCost);
3296
3297  return(bestVar);
3298}
3299
3300
3301/**Function********************************************************************
3302
3303  Synopsis    [Finds a splitting variable for output splitting.]
3304
3305  Description [Finds a splitting variable for output splitting.]
3306
3307  SideEffects []
3308
3309******************************************************************************/
3310static int
3311ChooseOutputSplittingVariable(ImgTfmInfo_t *info, array_t *vector,
3312                        int splitMethod)
3313{
3314  int bestVar = -1;
3315  int bestCost, newCost;
3316  int i;
3317  ImgComponent_t *comp;
3318  int size = ImgVectorFunctionSize(vector);
3319  int index;
3320
3321  switch (splitMethod) {
3322  case 0: /* smallest */
3323    bestCost = IMG_TF_MAX_INT;
3324    for (i = 0; i < array_n(vector); i++) {
3325      comp = array_fetch(ImgComponent_t *, vector, i);
3326      if (size < array_n(vector) &&
3327          st_lookup(info->intermediateVarsTable,
3328                    (char *)(long)bdd_top_var_id(comp->var), NIL(char *))) {
3329        continue;
3330      }
3331      newCost = bdd_size(comp->func);
3332      if (newCost < bestCost) {
3333        bestVar = i;
3334        bestCost = newCost;
3335      }
3336    }
3337    break;
3338  case 1: /* largest */
3339    bestCost = 0;
3340    for (i = 0; i < array_n(vector); i++) {
3341      comp = array_fetch(ImgComponent_t *, vector, i);
3342      if (size < array_n(vector) &&
3343          st_lookup(info->intermediateVarsTable,
3344                    (char *)(long)bdd_top_var_id(comp->var), NIL(char *))) {
3345        continue;
3346      }
3347      newCost = bdd_size(comp->func);
3348      if (newCost > bestCost) {
3349        bestVar = i;
3350        bestCost = newCost;
3351      }
3352    }
3353    break;
3354  case 2: /* top variable */
3355  default:
3356    comp = array_fetch(ImgComponent_t *, vector, 0);
3357    bestVar = (int)bdd_top_var_id(comp->var);
3358    for (i = 0; i < array_n(vector); i++) {
3359      comp = array_fetch(ImgComponent_t *, vector, i);
3360      index = (int)bdd_top_var_id(comp->var);
3361      if (size < array_n(vector) &&
3362          st_lookup(info->intermediateVarsTable, (char *)(long)index,
3363                    NIL(char *))) {
3364        continue;
3365      }
3366      if (bestVar == -1 ||
3367          bdd_get_level_from_id(info->manager, index) <
3368          bdd_get_level_from_id(info->manager, bestVar)) {
3369        bestVar = i;
3370      }
3371    }
3372    break;
3373  }
3374
3375  return(bestVar);
3376}
Note: See TracBrowser for help on using the repository browser.