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

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

vis2.3
File size: 60.6 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [imgTfmUtil.c]
4
5  PackageName [img]
6
7  Synopsis    [Routines for image computation using transition function method.]
8
9  SeeAlso     []
10
11  Author      [In-Ho Moon]
12
13  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado.
14  All rights reserved.
15
16  Permission is hereby granted, without written agreement and without license
17  or royalty fees, to use, copy, modify, and distribute this software and its
18  documentation for any purpose, provided that the above copyright notice and
19  the following two paragraphs appear in all copies of this software.
20
21  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
22  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
23  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
24  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
25
26  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
27  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
28  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
29  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
30  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
31
32******************************************************************************/
33#include "imgInt.h"
34
35static char rcsid[] UNUSED = "$Id: imgTfmUtil.c,v 1.23 2005/04/23 14:30:55 jinh Exp $";
36
37/*---------------------------------------------------------------------------*/
38/* Constant declarations                                                     */
39/*---------------------------------------------------------------------------*/
40
41/*---------------------------------------------------------------------------*/
42/* Type declarations                                                         */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Structure declarations                                                    */
47/*---------------------------------------------------------------------------*/
48
49/*---------------------------------------------------------------------------*/
50/* Variable declarations                                                     */
51/*---------------------------------------------------------------------------*/
52
53static  double  *signatures; /* used in finding dependent variables */
54
55/*---------------------------------------------------------------------------*/
56/* Macro declarations                                                        */
57/*---------------------------------------------------------------------------*/
58
59/**AutomaticStart*************************************************************/
60
61/*---------------------------------------------------------------------------*/
62/* Static function prototypes                                                */
63/*---------------------------------------------------------------------------*/
64
65static int SignatureCompare(int *ptrX, int *ptrY);
66static int CompareBddPointer(const void *e1, const void *e2);
67
68/**AutomaticEnd***************************************************************/
69
70
71/*---------------------------------------------------------------------------*/
72/* Definition of exported functions                                          */
73/*---------------------------------------------------------------------------*/
74
75
76/*---------------------------------------------------------------------------*/
77/* Definition of internal functions                                          */
78/*---------------------------------------------------------------------------*/
79
80
81/**Function********************************************************************
82
83  Synopsis    [Constrains a function vector with respect to a constraint.]
84
85  Description [Constrains a function vector with respect to a constraint.]
86
87  SideEffects []
88
89******************************************************************************/
90void
91ImgVectorConstrain(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint,
92                   array_t *relationArray, array_t **newVector, mdd_t **cube,
93                   array_t **newRelationArray, mdd_t **cofactorCube,
94                   mdd_t **abstractCube, boolean singleVarFlag)
95{
96  mdd_t                 *new_, *res, *old, *tmp;
97  ImgComponent_t        *comp, *comp1;
98  array_t               *vector1;
99  int                   i, index;
100  int                   dynStatus, dynOff;
101  bdd_reorder_type_t    dynMethod;
102  st_table              *equivTable;
103  int                   *ptr, *regularPtr;
104  int                   n, pos;
105  mdd_t                 *cofactor, *abstract, *nsVar, *constIntermediate;
106  array_t               *tmpRelationArray;
107  int                   size;
108
109  old = mdd_one(info->manager);
110  vector1 = array_alloc(ImgComponent_t *, 0);
111  dynStatus = 0;
112
113  if (singleVarFlag)
114    dynOff = 0;
115  else
116    dynOff = 1;
117  if (dynOff) {
118    dynStatus = bdd_reordering_status(info->manager, &dynMethod);
119    if (dynStatus != 0)
120      bdd_dynamic_reordering_disable(info->manager);
121  }
122
123  if (relationArray) {
124    cofactor = mdd_one(info->manager);
125    abstract = mdd_one(info->manager);
126  } else {
127    cofactor = NIL(mdd_t);
128    abstract = NIL(mdd_t);
129  }
130
131  if (info->nIntermediateVars) {
132    size = ImgVectorFunctionSize(vector);
133    if (size == array_n(vector))
134      constIntermediate = NIL(mdd_t);
135    else
136      constIntermediate = mdd_one(info->manager);
137  } else
138    constIntermediate = NIL(mdd_t);
139
140  n = 0;
141  equivTable = st_init_table(st_ptrcmp, st_ptrhash);
142  index = (int)bdd_top_var_id(constraint);
143  for (i = 0; i < array_n(vector); i++) {
144    comp = array_fetch(ImgComponent_t *, vector, i);
145    if (!bdd_is_tautology(constraint, 1)) {
146      if (singleVarFlag) {
147        if (comp->support[index])
148          res = bdd_cofactor(comp->func, constraint);
149        else
150          res = mdd_dup(comp->func);
151      } else
152        res = bdd_cofactor(comp->func, constraint);
153    } else
154      res = mdd_dup(comp->func);
155    if (bdd_is_tautology(res, 1)) {
156      if (comp->intermediate) {
157        tmp = constIntermediate;
158        constIntermediate = mdd_and(tmp, comp->var, 1, 1);
159        mdd_free(tmp);
160        mdd_free(res);
161        continue;
162      }
163      new_ = mdd_and(comp->var, old, 1, 1);
164      mdd_free(old);
165      mdd_free(res);
166      old = new_;
167      if (cofactor) {
168        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
169        tmp = cofactor;
170        cofactor = mdd_and(tmp, nsVar, 1, 1);
171        mdd_free(tmp);
172        mdd_free(nsVar);
173      }
174    } else if (bdd_is_tautology(res, 0)) {
175      if (comp->intermediate) {
176        tmp = constIntermediate;
177        constIntermediate = mdd_and(tmp, comp->var, 1, 0);
178        mdd_free(tmp);
179        mdd_free(res);
180        continue;
181      }
182      new_ = mdd_and(comp->var, old, 0, 1);
183      mdd_free(old);
184      mdd_free(res);
185      old = new_;
186      if (cofactor) {
187        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
188        tmp = cofactor;
189        cofactor = mdd_and(tmp, nsVar, 1, 0);
190        mdd_free(tmp);
191        mdd_free(nsVar);
192      }
193    } else {
194      if (comp->intermediate) {
195        comp1 = ImgComponentAlloc(info);
196        comp1->var = mdd_dup(comp->var);
197        comp1->func = res;
198        comp1->intermediate = 1;
199        if (mdd_equal(res, comp->func))
200          ImgSupportCopy(info, comp1->support, comp->support);
201        else
202          ImgComponentGetSupport(comp1);
203        array_insert_last(ImgComponent_t *, vector1, comp1);
204        n++;
205        continue;
206      }
207      ptr = (int *)bdd_pointer(res);
208      regularPtr = (int *)((unsigned long)ptr & ~01);
209      if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
210        comp1 = array_fetch(ImgComponent_t *, vector1, pos);
211        if (mdd_equal(res, comp1->func))
212          tmp = mdd_xnor(comp->var, comp1->var);
213        else
214          tmp = mdd_xor(comp->var, comp1->var);
215        new_ = mdd_and(tmp, old, 1, 1);
216        mdd_free(tmp);
217        mdd_free(old);
218        mdd_free(res);
219        old = new_;
220        if (abstract) {
221          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
222          tmp = abstract;
223          abstract = mdd_and(tmp, nsVar, 1, 1);
224          mdd_free(tmp);
225          mdd_free(nsVar);
226        }
227      } else {
228        comp1 = ImgComponentAlloc(info);
229        comp1->var = mdd_dup(comp->var);
230        comp1->func = res;
231        if (mdd_equal(res, comp->func))
232          ImgSupportCopy(info, comp1->support, comp->support);
233        else
234          ImgComponentGetSupport(comp1);
235        array_insert_last(ImgComponent_t *, vector1, comp1);
236        st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
237        n++;
238      }
239    }
240  }
241  st_free_table(equivTable);
242
243  if (dynOff && dynStatus != 0) {
244    bdd_dynamic_reordering(info->manager, dynMethod,
245                           BDD_REORDER_VERBOSITY_DEFAULT);
246  }
247
248  if (constIntermediate) {
249    if (!bdd_is_tautology(constIntermediate, 1)) {
250      mdd_t     *tmpCofactor, *tmpAbstract;
251
252      if (relationArray) {
253        vector1 = ImgComposeConstIntermediateVars(info, vector1,
254                                                  constIntermediate,
255                                                  &tmpCofactor, &tmpAbstract,
256                                                  &old, NIL(mdd_t *));
257        if (!bdd_is_tautology(tmpCofactor, 1)) {
258          tmp = cofactor;
259          cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
260          mdd_free(tmp);
261        }
262        mdd_free(tmpCofactor);
263        if (!bdd_is_tautology(tmpAbstract, 1)) {
264          tmp = abstract;
265          abstract = mdd_and(tmp, tmpAbstract, 1, 1);
266          mdd_free(tmp);
267        }
268        mdd_free(tmpAbstract);
269        tmp = cofactor;
270        cofactor = mdd_and(tmp, constIntermediate, 1, 1);
271        mdd_free(tmp);
272      } else {
273        vector1 = ImgComposeConstIntermediateVars(info, vector1,
274                                                  constIntermediate,
275                                                  NIL(mdd_t *), NIL(mdd_t *),
276                                                  &old, NIL(mdd_t *));
277      }
278    }
279    mdd_free(constIntermediate);
280  }
281
282  if (info->option->sortVectorFlag)
283    array_sort(vector1, CompareBddPointer);
284
285  if (relationArray && newRelationArray) {
286    if (singleVarFlag) {
287      *newRelationArray = relationArray;
288      tmp = cofactor;
289      cofactor = mdd_and(tmp, constraint, 1, 1);
290      mdd_free(tmp);
291    } else
292      *newRelationArray = ImgGetConstrainedRelationArray(info, relationArray,
293                                                         constraint);
294  }
295  if (cofactorCube && abstractCube) {
296    if (cofactor)
297      *cofactorCube = cofactor;
298    if (abstract)
299      *abstractCube = abstract;
300  } else {
301    if (cofactor) {
302      if (bdd_is_tautology(cofactor, 1))
303        mdd_free(cofactor);
304      else {
305        tmpRelationArray = *newRelationArray;
306        *newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray,
307                                                          cofactor);
308        mdd_free(cofactor);
309        if (tmpRelationArray != relationArray)
310          mdd_array_free(tmpRelationArray);
311      }
312    }
313    if (abstract) {
314      if (bdd_is_tautology(abstract, 1))
315        mdd_free(abstract);
316      else {
317        tmpRelationArray = *newRelationArray;
318        *newRelationArray = ImgGetAbstractedRelationArray(info->manager,
319                                                          tmpRelationArray,
320                                                        abstract);
321        mdd_free(abstract);
322        if (tmpRelationArray != relationArray)
323          mdd_array_free(tmpRelationArray);
324      }
325    }
326  }
327
328  *newVector = vector1;
329  *cube = old;
330}
331
332
333/**Function********************************************************************
334
335  Synopsis    [Minimizes a function vector and a from set with respect to an
336  essential cube.]
337
338  Description [Minimizes a function vector and a from set with respect to an
339  essential cube. This function is called during eliminating dependent
340  variables.]
341
342  SideEffects []
343
344******************************************************************************/
345mdd_t *
346ImgVectorMinimize(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint,
347                  mdd_t *from, array_t *relationArray, array_t **newVector,
348                  mdd_t **cube, array_t **newRelationArray,
349                  mdd_t **cofactorCube, mdd_t **abstractCube)
350{
351  mdd_t                 *new_, *res, *old, *tmp, *newFrom;
352  ImgComponent_t        *comp, *comp1;
353  array_t               *vector1;
354  int                   i;
355  st_table              *equivTable;
356  int                   *ptr, *regularPtr;
357  int                   n, pos;
358  mdd_t                 *cofactor, *abstract, *nsVar, *constIntermediate;
359  array_t               *tmpRelationArray;
360  int                   size;
361
362  if (from)
363    newFrom = mdd_dup(from);
364  else
365    newFrom = NIL(mdd_t);
366  if (cube)
367    old = mdd_one(info->manager);
368  else
369    old = NIL(mdd_t);
370  assert(newVector)
371  vector1 = array_alloc(ImgComponent_t *, 0);
372
373  if (relationArray) {
374    cofactor = mdd_one(info->manager);
375    abstract = mdd_one(info->manager);
376  } else {
377    cofactor = NIL(mdd_t);
378    abstract = NIL(mdd_t);
379  }
380
381  if (info->nIntermediateVars) {
382    size = ImgVectorFunctionSize(vector);
383    if (size == array_n(vector))
384      constIntermediate = NIL(mdd_t);
385    else
386      constIntermediate = mdd_one(info->manager);
387  } else
388    constIntermediate = NIL(mdd_t);
389
390  n = 0;
391  equivTable = st_init_table(st_ptrcmp, st_ptrhash);
392  for (i = 0; i < array_n(vector); i++) {
393    comp = array_fetch(ImgComponent_t *, vector, i);
394    res = bdd_minimize(comp->func, constraint);
395    if (bdd_is_tautology(res, 1)) {
396      if (comp->intermediate) {
397        tmp = constIntermediate;
398        constIntermediate = mdd_and(tmp, comp->var, 1, 1);
399        mdd_free(tmp);
400        mdd_free(res);
401        continue;
402      }
403      if (newFrom) {
404        tmp = newFrom;
405        newFrom = bdd_cofactor(tmp, comp->var);
406        mdd_free(tmp);
407      }
408      if (old) {
409        new_ = mdd_and(comp->var, old, 1, 1);
410        mdd_free(old);
411        mdd_free(res);
412        old = new_;
413      }
414      if (cofactor) {
415        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
416        tmp = cofactor;
417        cofactor = mdd_and(tmp, nsVar, 1, 1);
418        mdd_free(tmp);
419        mdd_free(nsVar);
420      }
421    } else if (bdd_is_tautology(res, 0)) {
422      if (comp->intermediate) {
423        tmp = constIntermediate;
424        constIntermediate = mdd_and(tmp, comp->var, 1, 0);
425        mdd_free(tmp);
426        mdd_free(res);
427        continue;
428      }
429      if (newFrom) {
430        tmp = newFrom;
431        new_ = mdd_not(comp->var);
432        newFrom = bdd_cofactor(tmp, new_);
433        mdd_free(tmp);
434        mdd_free(new_);
435      }
436      if (old) {
437        new_ = mdd_and(comp->var, old, 0, 1);
438        mdd_free(old);
439        mdd_free(res);
440        old = new_;
441      }
442      if (cofactor) {
443        nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
444        tmp = cofactor;
445        cofactor = mdd_and(tmp, nsVar, 1, 0);
446        mdd_free(tmp);
447        mdd_free(nsVar);
448      }
449    } else {
450      if (comp->intermediate) {
451        comp1 = ImgComponentAlloc(info);
452        comp1->var = mdd_dup(comp->var);
453        comp1->func = res;
454        comp1->intermediate = 1;
455        if (mdd_equal(res, comp->func))
456          ImgSupportCopy(info, comp1->support, comp->support);
457        else
458          ImgComponentGetSupport(comp1);
459        array_insert_last(ImgComponent_t *, vector1, comp1);
460        n++;
461        continue;
462      }
463      ptr = (int *)bdd_pointer(res);
464      regularPtr = (int *)((unsigned long)ptr & ~01);
465      if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
466        comp1 = array_fetch(ImgComponent_t *, vector1, pos);
467        if (newFrom) {
468          if (mdd_equal(res, comp1->func)) {
469            tmp = newFrom;
470            newFrom = bdd_compose(tmp, comp->var, comp1->var);
471            mdd_free(tmp);
472          } else {
473            tmp = newFrom;
474            new_ = mdd_not(comp1->var);
475            newFrom = bdd_compose(tmp, comp->var, new_);
476            mdd_free(tmp);
477            mdd_free(new_);
478          }
479        }
480        if (old) {
481          if (mdd_equal(res, comp1->func))
482            tmp = mdd_xnor(comp->var, comp1->var);
483          else
484            tmp = mdd_xor(comp->var, comp1->var);
485          new_ = mdd_and(tmp, old, 1, 1);
486          mdd_free(tmp);
487          mdd_free(old);
488          old = new_;
489        }
490        mdd_free(res);
491        if (abstract) {
492          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
493          tmp = abstract;
494          abstract = mdd_and(tmp, nsVar, 1, 1);
495          mdd_free(tmp);
496          mdd_free(nsVar);
497        }
498      } else {
499        comp1 = ImgComponentAlloc(info);
500        comp1->var = mdd_dup(comp->var);
501        comp1->func = res;
502        if (mdd_equal(res, comp->func))
503          ImgSupportCopy(info, comp1->support, comp->support);
504        else
505          ImgComponentGetSupport(comp1);
506        array_insert_last(ImgComponent_t *, vector1, comp1);
507        st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
508        n++;
509      }
510    }
511  }
512  st_free_table(equivTable);
513
514  if (constIntermediate) {
515    if (!bdd_is_tautology(constIntermediate, 1)) {
516      mdd_t     *tmpCofactor, *tmpAbstract;
517
518      if (relationArray) {
519        vector1 = ImgComposeConstIntermediateVars(info, vector1,
520                                                  constIntermediate,
521                                                  &tmpCofactor, &tmpAbstract,
522                                                  &old, NIL(mdd_t *));
523        if (!bdd_is_tautology(tmpCofactor, 1)) {
524          tmp = cofactor;
525          cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
526          mdd_free(tmp);
527        }
528        mdd_free(tmpCofactor);
529        if (!bdd_is_tautology(tmpAbstract, 1)) {
530          tmp = abstract;
531          abstract = mdd_and(tmp, tmpAbstract, 1, 1);
532          mdd_free(tmp);
533        }
534        mdd_free(tmpAbstract);
535        tmp = cofactor;
536        cofactor = mdd_and(tmp, constIntermediate, 1, 1);
537        mdd_free(tmp);
538      } else {
539        vector1 = ImgComposeConstIntermediateVars(info, vector1,
540                                                  constIntermediate,
541                                                  NIL(mdd_t *), NIL(mdd_t *),
542                                                  &old, NIL(mdd_t *));
543      }
544    }
545    mdd_free(constIntermediate);
546  }
547
548  if (info->option->sortVectorFlag)
549    array_sort(vector1, CompareBddPointer);
550
551  if (newRelationArray)
552    *newRelationArray = relationArray;
553  if (cofactorCube && abstractCube) {
554    if (cofactor) {
555      if (bdd_is_tautology(cofactor, 1)) {
556        *cofactorCube = mdd_dup(constraint);
557        mdd_free(cofactor);
558      } else {
559        tmp = cofactor;
560        cofactor = mdd_and(tmp, constraint, 1, 1);
561        mdd_free(tmp);
562        *cofactorCube = cofactor;
563      }
564    }
565    if (abstract)
566      *abstractCube = abstract;
567  } else {
568    if (cofactor) {
569      if (bdd_is_tautology(cofactor, 1))
570        mdd_free(cofactor);
571      else {
572        tmp = cofactor;
573        cofactor = mdd_and(tmp, constraint, 1, 1);
574        mdd_free(tmp);
575        if (newRelationArray) {
576          *newRelationArray = ImgGetCofactoredRelationArray(relationArray,
577                                                            cofactor);
578        } else
579          ImgCofactorRelationArray(relationArray, cofactor);
580        mdd_free(cofactor);
581      }
582    }
583    if (abstract) {
584      if (bdd_is_tautology(abstract, 1))
585        mdd_free(abstract);
586      else {
587        if (newRelationArray) {
588          tmpRelationArray = *newRelationArray;
589          *newRelationArray = ImgGetAbstractedRelationArray(info->manager,
590                                                            tmpRelationArray,
591                                                            abstract);
592          if (tmpRelationArray != relationArray)
593            mdd_array_free(tmpRelationArray);
594        } else
595          ImgAbstractRelationArray(info->manager, relationArray, abstract);
596        mdd_free(abstract);
597      }
598    }
599  }
600
601  if (*newVector == vector)
602    ImgVectorFree(vector);
603  *newVector = vector1;
604  if (cube)
605    *cube = old;
606
607  return(newFrom);
608}
609
610
611/**Function********************************************************************
612
613  Synopsis    [Frees a function vector.]
614
615  Description [Frees a function vector.]
616
617  SideEffects []
618
619******************************************************************************/
620void
621ImgVectorFree(array_t *vector)
622{
623  int                   i;
624  ImgComponent_t        *comp;
625
626  for (i = 0; i < array_n(vector); i++) {
627    comp = array_fetch(ImgComponent_t *, vector, i);
628    ImgComponentFree(comp);
629  }
630  array_free(vector);
631}
632
633
634/**Function********************************************************************
635
636  Synopsis    [Returns the number of functions in a vector.]
637
638  Description [Returns the number of functions in a vector. Excludes the
639  number of intermediate functions.]
640
641  SideEffects []
642
643******************************************************************************/
644int
645ImgVectorFunctionSize(array_t *vector)
646{
647  ImgComponent_t        *comp;
648  int                   i, size;
649
650  size = 0;
651  for (i = 0; i < array_n(vector); i++) {
652    comp = array_fetch(ImgComponent_t *, vector, i);
653    if (!comp->intermediate)
654      size++;
655  }
656
657  return(size);
658}
659
660
661/**Function********************************************************************
662
663  Synopsis    [Returns the shared BDD size of a vector.]
664
665  Description [Returns the shared BDD size of a vector.]
666
667  SideEffects []
668
669******************************************************************************/
670long
671ImgVectorBddSize(array_t *vector)
672{
673  array_t               *nodeArray;
674  ImgComponent_t        *comp;
675  int                   i, size;
676
677  nodeArray = array_alloc(mdd_t *, 0);
678  for (i = 0; i < array_n(vector); i++) {
679    comp = array_fetch(ImgComponent_t *, vector, i);
680    array_insert_last(mdd_t *, nodeArray, comp->func);
681  }
682  size = bdd_size_multiple(nodeArray);
683  array_free(nodeArray);
684
685  return(size);
686}
687
688
689/**Function********************************************************************
690
691  Synopsis    [Copies a vector.]
692
693  Description [Copies a vector.]
694
695  SideEffects []
696
697******************************************************************************/
698array_t *
699ImgVectorCopy(ImgTfmInfo_t *info, array_t *vector)
700{
701  array_t               *newVector;
702  ImgComponent_t        *comp, *newComp;
703  int                   i;
704
705  newVector = array_alloc(ImgComponent_t *, 0);
706  for (i = 0; i < array_n(vector); i++) {
707    comp = array_fetch(ImgComponent_t *, vector, i);
708    newComp = ImgComponentCopy(info, comp);
709    array_insert_last(ImgComponent_t *, newVector, newComp);
710  }
711  return(newVector);
712}
713
714
715/**Function********************************************************************
716
717  Synopsis    [Allocates a component.]
718
719  Description [Allocates a component.]
720
721  SideEffects []
722
723******************************************************************************/
724ImgComponent_t *
725ImgComponentAlloc(ImgTfmInfo_t *info)
726{
727  ImgComponent_t        *comp;
728
729  comp = ALLOC(ImgComponent_t, 1);
730  memset(comp, 0, sizeof(ImgComponent_t));
731  comp->support = ALLOC(char, info->nVars);
732  ImgSupportClear(info, comp->support);
733  comp->id = info->nComponents++;
734  return(comp);
735}
736
737
738/**Function********************************************************************
739
740  Synopsis    [Copies a component]
741
742  Description [Copies a component]
743
744  SideEffects []
745
746******************************************************************************/
747ImgComponent_t *
748ImgComponentCopy(ImgTfmInfo_t *info, ImgComponent_t *comp)
749{
750  ImgComponent_t        *newComp;
751
752  newComp = ImgComponentAlloc(info);
753  newComp->func = mdd_dup(comp->func);
754  newComp->var = mdd_dup(comp->var);
755  ImgSupportCopy(info, newComp->support, comp->support);
756  newComp->intermediate = comp->intermediate;
757  return(newComp);
758}
759
760
761/**Function********************************************************************
762
763  Synopsis    [Frees a component.]
764
765  Description [Frees a component.]
766
767  SideEffects []
768
769******************************************************************************/
770void
771ImgComponentFree(ImgComponent_t *comp)
772{
773  if (comp->func)
774    mdd_free(comp->func);
775  if (comp->var != NULL)
776    mdd_free(comp->var);
777  FREE(comp->support);
778  FREE(comp);
779}
780
781
782/**Function********************************************************************
783
784  Synopsis    [Gets the supports of a component.]
785
786  Description [Gets the supports of a component.]
787
788  SideEffects []
789
790******************************************************************************/
791void
792ImgComponentGetSupport(ImgComponent_t *comp)
793{
794  int           index;
795  var_set_t     *supportVarSet;
796
797  supportVarSet = bdd_get_support(comp->func);
798  for (index = 0; index < supportVarSet->n_elts; index++) {
799    if (var_set_get_elt(supportVarSet, index) == 1)
800      comp->support[index] = 1;
801  }
802  var_set_free(supportVarSet);
803}
804
805
806/**Function********************************************************************
807
808  Synopsis    [Copies the supports of a component.]
809
810  Description [Copies the supports of a component. Here support is an array
811  of char.]
812
813  SideEffects []
814
815******************************************************************************/
816void
817ImgSupportCopy(ImgTfmInfo_t *info, char *dsupport, char *ssupport)
818{
819  memcpy(dsupport, ssupport, sizeof(char) * info->nVars);
820}
821
822
823/**Function********************************************************************
824
825  Synopsis    [Clears a support array.]
826
827  Description [Clears a support array.]
828
829  SideEffects []
830
831******************************************************************************/
832void
833ImgSupportClear(ImgTfmInfo_t *info, char *support)
834{
835  memset(support, 0, sizeof(char) * info->nVars);
836}
837
838
839/**Function********************************************************************
840
841  Synopsis    [Prints a support array.]
842
843  Description [Prints a support array.]
844
845  SideEffects []
846
847******************************************************************************/
848void
849ImgSupportPrint(ImgTfmInfo_t *info, char *support)
850{
851  int   i;
852
853  for (i = 0; i < info->nVars; i++) {
854   if (support[i])
855     printf("*");
856   else
857     printf(".");
858  }
859  printf("\n");
860}
861
862
863/**Function********************************************************************
864
865  Synopsis    [Returns the number of support of a support array.]
866
867  Description [Returns the number of support of a support array.]
868
869  SideEffects []
870
871******************************************************************************/
872int
873ImgSupportCount(ImgTfmInfo_t *info, char *support)
874{
875  int   i, nSupports;
876
877  nSupports = 0;
878  for (i = 0; i < info->nVars; i++) {
879   if (support[i])
880     nSupports++;
881  }
882  return(nSupports);
883}
884
885
886/**Function********************************************************************
887
888  Synopsis    [Constrains a relation array with respect to a constraint.]
889
890  Description [Constrains a relation array with respect to a constraint.
891  Returns new relation array.]
892
893  SideEffects []
894
895******************************************************************************/
896array_t *
897ImgGetConstrainedRelationArray(ImgTfmInfo_t *info, array_t *relationArray,
898                                mdd_t *constraint)
899{
900  array_t               *constrainedRelationArray;
901  int                   dynStatus;
902  bdd_reorder_type_t    dynMethod;
903
904  dynStatus = bdd_reordering_status(info->manager, &dynMethod);
905  if (dynStatus != 0)
906    bdd_dynamic_reordering_disable(info->manager);
907
908  constrainedRelationArray = ImgGetCofactoredRelationArray(relationArray,
909                                                           constraint);
910
911  if (dynStatus != 0) {
912    bdd_dynamic_reordering(info->manager, dynMethod,
913                           BDD_REORDER_VERBOSITY_DEFAULT);
914  }
915
916  return(constrainedRelationArray);
917}
918
919
920/**Function********************************************************************
921
922  Synopsis    [Cofactors a relation array with respect to a function.]
923
924  Description [Cofactors a relation array with respect to a function.
925  Returns new relation array.]
926
927  SideEffects []
928
929******************************************************************************/
930array_t *
931ImgGetCofactoredRelationArray(array_t *relationArray, mdd_t *func)
932{
933  int           i;
934  array_t       *cofactoredRelationArray;
935  mdd_t         *relation, *cofactoredRelation;
936
937  if (bdd_is_tautology(func, 1))
938    return(mdd_array_duplicate(relationArray));
939
940  cofactoredRelationArray = array_alloc(mdd_t *, 0);
941
942  for (i = 0; i < array_n(relationArray); i++) {
943    relation = array_fetch(mdd_t *, relationArray, i);
944    cofactoredRelation = bdd_cofactor(relation, func);
945    if (bdd_is_tautology(cofactoredRelation, 1))
946      mdd_free(cofactoredRelation);
947    else
948      array_insert_last(mdd_t *, cofactoredRelationArray, cofactoredRelation);
949  }
950
951  return(cofactoredRelationArray);
952}
953
954
955/**Function********************************************************************
956
957  Synopsis    [Cofactors a relation array with respect to a function.]
958
959  Description [Cofactors a relation array with respect to a function.]
960
961  SideEffects []
962
963******************************************************************************/
964void
965ImgCofactorRelationArray(array_t *relationArray, mdd_t *func)
966{
967  int           i;
968  mdd_t         *relation, *cofactoredRelation;
969
970  if (bdd_is_tautology(func, 1))
971    return;
972
973  for (i = 0; i < array_n(relationArray); i++) {
974    relation = array_fetch(mdd_t *, relationArray, i);
975    cofactoredRelation = bdd_cofactor(relation, func);
976    if (mdd_equal(cofactoredRelation, relation))
977      mdd_free(cofactoredRelation);
978    else {
979      mdd_free(relation);
980      array_insert(mdd_t *, relationArray, i, cofactoredRelation);
981    }
982  }
983}
984
985
986/**Function********************************************************************
987
988  Synopsis    [Smoothes a relation array with respect to a cube.]
989
990  Description [Smoothes a relation array with respect to a cube.]
991
992  SideEffects []
993
994******************************************************************************/
995array_t *
996ImgGetAbstractedRelationArray(mdd_manager *manager, array_t *relationArray,
997                              mdd_t *cube)
998{
999  int           i;
1000  array_t       *abstractedRelationArray;
1001  mdd_t         *relation, *abstractedRelation;
1002  array_t       *varsArray;
1003
1004  if (bdd_is_tautology(cube, 1))
1005    return(mdd_array_duplicate(relationArray));
1006
1007  abstractedRelationArray = array_alloc(mdd_t *, 0);
1008
1009  if (bdd_get_package_name() != CUDD)
1010    varsArray = mdd_get_bdd_support_vars(manager, cube);
1011  else /* to remove uninitialized variable warning*/
1012    varsArray = NIL(array_t);
1013  for (i = 0; i < array_n(relationArray); i++) {
1014    relation = array_fetch(mdd_t *, relationArray, i);
1015    if (bdd_get_package_name() == CUDD)
1016      abstractedRelation = bdd_smooth_with_cube(relation, cube);
1017    else
1018      abstractedRelation = bdd_smooth(relation, varsArray);
1019    if (bdd_is_tautology(abstractedRelation, 1))
1020      mdd_free(abstractedRelation);
1021    else
1022      array_insert_last(mdd_t *, abstractedRelationArray, abstractedRelation);
1023  }
1024  if (bdd_get_package_name() != CUDD)
1025    mdd_array_free(varsArray);
1026
1027  return(abstractedRelationArray);
1028}
1029
1030
1031/**Function********************************************************************
1032
1033  Synopsis    [Smoothes a relation array with respect to a cube.]
1034
1035  Description [Smoothes a relation array with respect to a cube.]
1036
1037  SideEffects []
1038
1039******************************************************************************/
1040void
1041ImgAbstractRelationArray(mdd_manager *manager, array_t *relationArray,
1042                         mdd_t *cube)
1043{
1044  int           i;
1045  mdd_t         *relation, *abstractedRelation;
1046  array_t       *varsArray;
1047
1048  if (bdd_is_tautology(cube, 1))
1049    return;
1050
1051  if (bdd_get_package_name() != CUDD)
1052    varsArray = mdd_get_bdd_support_vars(manager, cube);
1053  else /* to remove uninitialized variable warning*/
1054    varsArray = NIL(array_t);
1055  for (i = 0; i < array_n(relationArray); i++) {
1056    relation = array_fetch(mdd_t *, relationArray, i);
1057    if (bdd_get_package_name() == CUDD)
1058      abstractedRelation = bdd_smooth_with_cube(relation, cube);
1059    else
1060      abstractedRelation = bdd_smooth(relation, varsArray);
1061    if (mdd_equal(abstractedRelation, relation))
1062      mdd_free(abstractedRelation);
1063    else {
1064      mdd_free(relation);
1065      array_insert(mdd_t *, relationArray, i, abstractedRelation);
1066    }
1067  }
1068  if (bdd_get_package_name() != CUDD)
1069    mdd_array_free(varsArray);
1070}
1071
1072
1073/**Function********************************************************************
1074
1075  Synopsis    [Cofactors and smooths a relation array.]
1076
1077  Description [Cofactors and smooths a relation array. Returns new
1078  relation array.]
1079
1080  SideEffects []
1081
1082******************************************************************************/
1083array_t *
1084ImgGetCofactoredAbstractedRelationArray(mdd_manager *manager,
1085                                        array_t *relationArray,
1086                                        mdd_t *cofactorCube,
1087                                        mdd_t *abstractCube)
1088{
1089  int           i;
1090  array_t       *newRelationArray = array_alloc(mdd_t *, 0);
1091  mdd_t         *relation, *newRelation, *tmpRelation;
1092  array_t       *varsArray;
1093
1094  if (bdd_get_package_name() != CUDD)
1095    varsArray = mdd_get_bdd_support_vars(manager, abstractCube);
1096  else /* to remove uninitialized variable warning*/
1097    varsArray = NIL(array_t);
1098  for (i = 0; i < array_n(relationArray); i++) {
1099    relation = array_fetch(mdd_t *, relationArray, i);
1100    tmpRelation = bdd_cofactor(relation, cofactorCube);
1101    if (bdd_get_package_name() == CUDD)
1102      newRelation = bdd_smooth_with_cube(tmpRelation, abstractCube);
1103    else
1104      newRelation = bdd_smooth(tmpRelation, varsArray);
1105    mdd_free(tmpRelation);
1106    if (bdd_is_tautology(newRelation, 1))
1107      mdd_free(newRelation);
1108    else
1109      array_insert_last(mdd_t *, newRelationArray, newRelation);
1110  }
1111  if (bdd_get_package_name() != CUDD)
1112    mdd_array_free(varsArray);
1113
1114  return(newRelationArray);
1115}
1116
1117
1118/**Function********************************************************************
1119
1120  Synopsis    [Smothes and cofactors a relation array.]
1121
1122  Description [Smothes and cofactors a relation array. Returns new
1123  relation array.]
1124
1125  SideEffects []
1126
1127******************************************************************************/
1128array_t *
1129ImgGetAbstractedCofactoredRelationArray(mdd_manager *manager,
1130                                        array_t *relationArray,
1131                                        mdd_t *cofactorCube,
1132                                        mdd_t *abstractCube)
1133{
1134  int           i;
1135  array_t       *newRelationArray = array_alloc(mdd_t *, 0);
1136  mdd_t         *relation, *newRelation, *tmpRelation;
1137  array_t       *varsArray;
1138
1139  if (bdd_get_package_name() != CUDD)
1140    varsArray = mdd_get_bdd_support_vars(manager, abstractCube);
1141  else /* to remove uninitialized variable warning*/
1142    varsArray = NIL(array_t);
1143  for (i = 0; i < array_n(relationArray); i++) {
1144    relation = array_fetch(mdd_t *, relationArray, i);
1145    if (bdd_get_package_name() == CUDD)
1146      tmpRelation = bdd_smooth_with_cube(relation, abstractCube);
1147    else
1148      tmpRelation = bdd_smooth(relation, varsArray);
1149    newRelation = bdd_cofactor(tmpRelation, cofactorCube);
1150    mdd_free(tmpRelation);
1151    if (bdd_is_tautology(newRelation, 1))
1152      mdd_free(newRelation);
1153    else
1154      array_insert_last(mdd_t *, newRelationArray, newRelation);
1155  }
1156  if (bdd_get_package_name() != CUDD)
1157    mdd_array_free(varsArray);
1158
1159  return(newRelationArray);
1160}
1161
1162
1163/**Function********************************************************************
1164
1165  Synopsis    [Constrains a function vector with respect to a constraint.]
1166
1167  Description [Constrains a function vector with respect to a constraint.
1168  Returns new function vector.]
1169
1170  SideEffects []
1171
1172******************************************************************************/
1173array_t *
1174ImgGetConstrainedVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint)
1175{
1176  array_t               *constrainedVector;
1177  int                   dynStatus;
1178  bdd_reorder_type_t    dynMethod;
1179
1180  dynStatus = bdd_reordering_status(info->manager, &dynMethod);
1181  if (dynStatus != 0)
1182    bdd_dynamic_reordering_disable(info->manager);
1183
1184  constrainedVector = ImgGetCofactoredVector(info, vector, constraint);
1185
1186  if (dynStatus != 0) {
1187    bdd_dynamic_reordering(info->manager, dynMethod,
1188                           BDD_REORDER_VERBOSITY_DEFAULT);
1189  }
1190
1191  return(constrainedVector);
1192}
1193
1194
1195/**Function********************************************************************
1196
1197  Synopsis    [Cofactors a function vector with respect to a function.]
1198
1199  Description [Cofactors a function vector with respect to a function.
1200  Returns new function vector.]
1201
1202  SideEffects []
1203
1204******************************************************************************/
1205array_t *
1206ImgGetCofactoredVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *func)
1207{
1208  int                   i;
1209  array_t               *cofactoredVector = array_alloc(ImgComponent_t *, 0);
1210  ImgComponent_t        *comp, *cofactoredComp;
1211  mdd_t                 *cofactoredFunc;
1212
1213  if (bdd_is_tautology(func, 1))
1214    return(ImgVectorCopy(info, vector));
1215
1216  for (i = 0; i < array_n(vector); i++) {
1217    comp = array_fetch(ImgComponent_t *, vector, i);
1218    cofactoredFunc = bdd_cofactor(comp->func, func);
1219    cofactoredComp = ImgComponentAlloc(info);
1220    cofactoredComp->var = mdd_dup(comp->var);
1221    cofactoredComp->func = cofactoredFunc;
1222    cofactoredComp->intermediate = comp->intermediate;
1223    if (mdd_equal(cofactoredFunc, comp->func))
1224      ImgSupportCopy(info, cofactoredComp->support, comp->support);
1225    else
1226      ImgComponentGetSupport(cofactoredComp);
1227    array_insert_last(ImgComponent_t *, cofactoredVector, cofactoredComp);
1228  }
1229
1230  return(cofactoredVector);
1231}
1232
1233
1234/**Function********************************************************************
1235
1236  Synopsis    [Cofactors a function vector with respect to a function.]
1237
1238  Description [Cofactors a function vector with respect to a function.]
1239
1240  SideEffects []
1241
1242******************************************************************************/
1243void
1244ImgCofactorVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *func)
1245{
1246  int                   i;
1247  ImgComponent_t        *comp;
1248  mdd_t                 *cofactoredFunc;
1249
1250  if (bdd_is_tautology(func, 1))
1251    return;
1252
1253  for (i = 0; i < array_n(vector); i++) {
1254    comp = array_fetch(ImgComponent_t *, vector, i);
1255    cofactoredFunc = bdd_cofactor(comp->func, func);
1256    if (mdd_equal(cofactoredFunc, comp->func))
1257      mdd_free(cofactoredFunc);
1258    else {
1259      mdd_free(comp->func);
1260      comp->func = cofactoredFunc;
1261      ImgSupportClear(info, comp->support);
1262      ImgComponentGetSupport(comp);
1263    }
1264  }
1265}
1266
1267
1268/**Function********************************************************************
1269
1270  Synopsis    [Eliminates dependent variables from transition function.]
1271
1272  Description [Eliminates dependent variables from a transition
1273  function.  Returns a simplified copy of the given states if successful;
1274  NULL otherwise.]
1275
1276  SideEffects [vector is also modified.]
1277
1278  SeeAlso     []
1279
1280******************************************************************************/
1281mdd_t *
1282ImgTfmEliminateDependVars(ImgTfmInfo_t *info, array_t *vector,
1283                          array_t *relationArray, mdd_t *states,
1284                          array_t **newVector,
1285                          mdd_t **dependRelations)
1286{
1287  int                   i, j;
1288  int                   howMany = 0;
1289                        /* number of latches that can be eliminated */
1290  mdd_t                 *var, *newStates, *abs, *positive, *phi;
1291  mdd_t                 *tmp, *relation;
1292  int                   nVars;
1293  int                   nSupports; /* vars in the support of the state set */
1294  int                   *candidates; /* vars to be considered for elimination */
1295  double                minStates;
1296  ImgComponent_t        *comp, *newComp;
1297
1298  if (dependRelations) {
1299    *dependRelations = mdd_one(info->manager);
1300    *newVector = array_alloc(ImgComponent_t *, 0);
1301  }
1302  newStates = mdd_dup(states);
1303  nVars = info->nVars;
1304
1305  candidates = ALLOC(int, nVars);
1306  if (candidates == NULL)
1307    return(NULL);
1308
1309  comp = ImgComponentAlloc(info);
1310  comp->func = newStates;
1311  ImgComponentGetSupport(comp);
1312  nSupports = 0;
1313  for (i = 0 ; i < nVars; i++) {
1314    if (comp->support[i]) {
1315      candidates[nSupports] = i;
1316      nSupports++;
1317    }
1318  }
1319  comp->func = NIL(mdd_t);
1320  ImgComponentFree(comp);
1321
1322  /* The signatures of the variables in a function are the number
1323  ** of minterms of the positive cofactors with respect to the
1324  ** variables themselves. */
1325  signatures = bdd_cof_minterm(newStates);
1326  if (signatures == NULL) {
1327    FREE(candidates);
1328    return(NULL);
1329  }
1330  /* We now extract a positive quantity which is higher for those
1331  ** variables that are closer to being essential. */
1332  minStates = signatures[nSupports];
1333  for (i = 0; i < nSupports; i++) {
1334    double z = signatures[i] / minStates - 1.0;
1335    signatures[i] = (z < 0.0) ? -z : z;    /* make positive */
1336  }
1337  qsort((void *)candidates, nSupports, sizeof(int),
1338      (int (*)(const void *, const void *))SignatureCompare);
1339  FREE(signatures);
1340
1341  /* Now process the candidates in the given order. */
1342  for (i = 0; i < nSupports; i++) {
1343    var = bdd_var_with_index(info->manager, candidates[i]);
1344    if (bdd_var_is_dependent(newStates, var)) {
1345      abs = bdd_smooth_with_cube(newStates, var);
1346      if (abs == NULL)
1347        return(NULL);
1348      positive = bdd_cofactor(newStates, var);
1349      if (positive == NULL)
1350        return(NULL);
1351      phi = Img_MinimizeImage(positive, abs, Img_DefaultMinimizeMethod_c,
1352                              TRUE); 
1353      if (phi == NULL)
1354        return(NULL);
1355      mdd_free(positive);
1356      if (bdd_size(phi) < IMG_MAX_DEP_SIZE) {
1357        howMany++;
1358        if (dependRelations) {
1359          for (j = 0; j < array_n(vector); j++) {
1360            comp = array_fetch(ImgComponent_t *, vector, j);
1361            if (mdd_equal(comp->var, var))
1362              continue;
1363            newComp = ImgComponentCopy(info, comp);
1364            array_insert_last(ImgComponent_t *, *newVector, newComp);
1365          }
1366        } else {
1367          for (j = 0; j < array_n(vector); j++) {
1368            comp = array_fetch(ImgComponent_t *, vector, j);
1369            tmp = bdd_compose(comp->func, var, phi);
1370            if (tmp == NULL)
1371              return(NULL);
1372            mdd_free(comp->func);
1373            comp->func = tmp;
1374            ImgSupportClear(info, comp->support);
1375            ImgComponentGetSupport(comp);
1376          }
1377        }
1378        if (relationArray) {
1379          for (j = 0; j < array_n(relationArray); j++) {
1380            relation = array_fetch(mdd_t *, relationArray, j);
1381            if (dependRelations)
1382              tmp = bdd_smooth_with_cube(relation, var);
1383            else
1384              tmp = bdd_compose(relation, var, phi);
1385            mdd_free(relation);
1386            array_insert(mdd_t *, relationArray, j, tmp);
1387          }
1388        }
1389        mdd_free(newStates);
1390        newStates = abs;
1391        if (dependRelations) {
1392          relation = mdd_xnor(var, phi);
1393          tmp = mdd_and(*dependRelations, relation, 1, 1);
1394          mdd_free(*dependRelations);
1395          mdd_free(relation);
1396          *dependRelations = tmp;
1397        }
1398      } else {
1399        mdd_free(abs);
1400      }
1401      mdd_free(phi);
1402    }
1403  }
1404  FREE(candidates);
1405
1406  if (howMany) {
1407    if (info->imageVerbosity > 0)
1408      (void)fprintf(vis_stdout, "Eliminated %d vars.\n", howMany);
1409    info->averageFoundDependVars = (info->averageFoundDependVars *
1410                        (float)info->nFoundDependVars + (float)howMany) /
1411                        (float)(info->nFoundDependVars + 1);
1412    info->nFoundDependVars++;
1413  }
1414
1415  info->nPrevEliminatedFwd = howMany;
1416  return(newStates);
1417} /* end of TfmEliminateDependVars */
1418
1419
1420/**Function********************************************************************
1421
1422  Synopsis    [Checks whether there is a constant function of intermediate
1423  variables.]
1424
1425  Description [Checks whether there is a constant function of intermediate
1426  variables.]
1427
1428  SideEffects []
1429
1430******************************************************************************/
1431int
1432ImgExistConstIntermediateVar(array_t *vector)
1433{
1434  int                   i;
1435  ImgComponent_t        *comp;
1436
1437  for (i = 0; i < array_n(vector); i++) {
1438    comp = array_fetch(ImgComponent_t *, vector, i);
1439    if (comp->intermediate) {
1440      if (mdd_is_tautology(comp->func, 1) || mdd_is_tautology(comp->func, 0))
1441        return(1);
1442    }
1443  }
1444  return(0);
1445}
1446
1447
1448/**Function********************************************************************
1449
1450  Synopsis    [Returns a function composed all intermediate variables.]
1451
1452  Description [Returns a function composed all intermediate variables.]
1453
1454  SideEffects []
1455
1456******************************************************************************/
1457mdd_t *
1458ImgGetComposedFunction(array_t *vector)
1459{
1460  ImgComponent_t        *comp;
1461  mdd_t                 *func, *newFunc;
1462  int                   i;
1463  array_t               *varArray, *funcArray;
1464
1465  assert(ImgVectorFunctionSize(vector) == 1);
1466
1467  /* no intermediate variables */
1468  if (array_n(vector) == 1) {
1469    comp = array_fetch(ImgComponent_t *, vector, 0);
1470    newFunc = mdd_dup(comp->func);
1471    return(newFunc);
1472  }
1473
1474  func = NIL(mdd_t);
1475  varArray = array_alloc(mdd_t *, 0);
1476  funcArray = array_alloc(mdd_t *, 0);
1477
1478  for (i = 0; i < array_n(vector); i++) {
1479    comp = array_fetch(ImgComponent_t *, vector, i);
1480    if (comp->intermediate) {
1481      array_insert_last(mdd_t *, varArray, comp->var);
1482      array_insert_last(mdd_t *, funcArray, comp->func);
1483      continue;
1484    }
1485    func = comp->func;
1486  }
1487
1488  newFunc = bdd_vector_compose(func, varArray, funcArray);
1489  array_free(varArray);
1490  array_free(funcArray);
1491  return(newFunc);
1492}
1493
1494
1495/**Function********************************************************************
1496
1497  Synopsis    [Returns the first latch component.]
1498
1499  Description [Returns the first latch component.]
1500
1501  SideEffects []
1502
1503******************************************************************************/
1504ImgComponent_t *
1505ImgGetLatchComponent(array_t *vector)
1506{
1507  ImgComponent_t        *comp;
1508  int                   i;
1509
1510  for (i = 0; i < array_n(vector); i++) {
1511    comp = array_fetch(ImgComponent_t *, vector, i);
1512    if (!comp->intermediate)
1513      return(comp);
1514  }
1515  return(NIL(ImgComponent_t));
1516}
1517
1518
1519/**Function********************************************************************
1520
1521  Synopsis    [Compose the constant intermediate variable functions.]
1522
1523  Description [Compose the constant intermediate variable functions.]
1524
1525  SideEffects []
1526
1527******************************************************************************/
1528array_t *
1529ImgComposeConstIntermediateVars(ImgTfmInfo_t *info, array_t *vector,
1530                                mdd_t *constIntermediate,
1531                                mdd_t **cofactorCube, mdd_t **abstractCube,
1532                                mdd_t **and_, mdd_t **from)
1533{
1534  int                   i, n, pos;
1535  array_t               *tmpVector, *cofactoredVector;
1536  mdd_t                 *cofactor, *abstract;
1537  mdd_t                 *curConstIntermediate, *newConstIntermediate;
1538  mdd_t                 *tmp, *new_, *func, *varNot, *nsVar;
1539  ImgComponent_t        *comp, *comp1;
1540  st_table              *equivTable;
1541  int                   *ptr, *regularPtr;
1542
1543  if (cofactorCube)
1544    cofactor = mdd_one(info->manager);
1545  else
1546    cofactor = NIL(mdd_t);
1547  if (abstractCube)
1548    abstract = mdd_one(info->manager);
1549  else
1550    abstract = NIL(mdd_t);
1551
1552  cofactoredVector = vector;
1553  tmpVector = cofactoredVector;
1554  curConstIntermediate = constIntermediate;
1555
1556  while (!bdd_is_tautology(curConstIntermediate, 1)) {
1557    newConstIntermediate = mdd_one(info->manager);
1558    n = 0;
1559    equivTable = st_init_table(st_ptrcmp, st_ptrhash);
1560    cofactoredVector = array_alloc(ImgComponent_t *, 0);
1561    for (i = 0; i < array_n(tmpVector); i++) {
1562      comp = array_fetch(ImgComponent_t *, tmpVector, i);
1563      func = bdd_cofactor(comp->func, curConstIntermediate);
1564
1565      if (comp->intermediate) {
1566        if (mdd_is_tautology(func, 1)) {
1567          tmp = newConstIntermediate;
1568          newConstIntermediate = mdd_and(tmp, comp->var, 1, 1);
1569          mdd_free(tmp);
1570          mdd_free(func);
1571          continue;
1572        } else if (mdd_is_tautology(func, 0)) {
1573          tmp = newConstIntermediate;
1574          newConstIntermediate = mdd_and(tmp, comp->var, 1, 0);
1575          mdd_free(tmp);
1576          mdd_free(func);
1577          continue;
1578        }
1579
1580        comp1 = ImgComponentAlloc(info);
1581        comp1->var = mdd_dup(comp->var);
1582        comp1->func = func;
1583        comp1->intermediate = 1;
1584        if (mdd_equal(func, comp->func))
1585          ImgSupportCopy(info, comp1->support, comp->support);
1586        else
1587          ImgComponentGetSupport(comp1);
1588        array_insert_last(ImgComponent_t *, cofactoredVector, comp1);
1589        n++;
1590        continue;
1591      }
1592
1593      if (mdd_is_tautology(func, 1)) {
1594        if (cofactor) {
1595          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1596          tmp = cofactor;
1597          cofactor = mdd_and(tmp, nsVar, 1, 1);
1598          mdd_free(tmp);
1599          mdd_free(nsVar);
1600        }
1601        if (and_) {
1602          tmp = *and_;
1603          *and_ = mdd_and(tmp, comp->var, 1, 1);
1604          mdd_free(tmp);
1605        }
1606        if (from) {
1607          tmp = *from;
1608          *from = bdd_cofactor(tmp, comp->var);
1609          mdd_free(tmp);
1610        }
1611        mdd_free(func);
1612      } else if (mdd_is_tautology(func, 0)) {
1613        if (cofactor) {
1614          nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1615          tmp = cofactor;
1616          cofactor = mdd_and(tmp, nsVar, 1, 0);
1617          mdd_free(tmp);
1618          mdd_free(nsVar);
1619        }
1620        if (and_) {
1621          tmp = *and_;
1622          *and_ = mdd_and(tmp, comp->var, 1, 0);
1623          mdd_free(tmp);
1624        }
1625        if (from) {
1626          tmp = *from;
1627          varNot = bdd_not(comp->var);
1628          *from = bdd_cofactor(tmp, varNot);
1629          mdd_free(tmp);
1630          mdd_free(varNot);
1631        }
1632        mdd_free(func);
1633      } else {
1634        ptr = (int *)bdd_pointer(func);
1635        regularPtr = (int *)((unsigned long)ptr & ~01);
1636        if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
1637          comp1 = array_fetch(ImgComponent_t *, cofactoredVector, pos);
1638          if (and_) {
1639            if (mdd_equal(func, comp1->func))
1640              tmp = mdd_xnor(comp->var, comp1->var);
1641            else
1642              tmp = mdd_xor(comp->var, comp1->var);
1643            new_ = mdd_and(tmp, *and_, 1, 1);
1644            mdd_free(tmp);
1645            mdd_free(*and_);
1646            mdd_free(func);
1647            *and_ = new_;
1648          }
1649          if (abstract) {
1650            nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
1651            tmp = abstract;
1652            abstract = mdd_and(tmp, nsVar, 1, 1);
1653            mdd_free(tmp);
1654            mdd_free(nsVar);
1655          }
1656          if (from) {
1657            tmp = *from;
1658            *from = bdd_compose(tmp, comp->var, comp1->var);
1659            mdd_free(tmp);
1660          }
1661        } else {
1662          comp1 = ImgComponentAlloc(info);
1663          comp1->var = mdd_dup(comp->var);
1664          comp1->func = func;
1665          if (mdd_equal(func, comp->func))
1666            ImgSupportCopy(info, comp1->support, comp->support);
1667          else
1668            ImgComponentGetSupport(comp1);
1669          array_insert_last(ImgComponent_t *, cofactoredVector, comp1);
1670          st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
1671          n++;
1672        }
1673      }
1674    }
1675
1676    if (curConstIntermediate != constIntermediate)
1677      mdd_free(curConstIntermediate);
1678    curConstIntermediate = newConstIntermediate;
1679
1680    if (cofactor) {
1681      tmp = cofactor;
1682      cofactor = mdd_and(tmp, curConstIntermediate, 1, 1);
1683      mdd_free(tmp);
1684    }
1685
1686    st_free_table(equivTable);
1687    ImgVectorFree(tmpVector);
1688    tmpVector = cofactoredVector;
1689  }
1690
1691  if (curConstIntermediate != constIntermediate)
1692    mdd_free(curConstIntermediate);
1693
1694  if (cofactorCube)
1695    *cofactorCube = cofactor;
1696  if (abstractCube)
1697    *abstractCube = abstract;
1698
1699  return(cofactoredVector);
1700}
1701
1702
1703/**Function********************************************************************
1704
1705  Synopsis    [Returns the number of BDD supports in a function.]
1706
1707  Description [Returns the number of BDD supports in a function.]
1708
1709  SideEffects []
1710
1711******************************************************************************/
1712int
1713ImgCountBddSupports(mdd_t *func)
1714{
1715  int           index, nSupports = 0;
1716  var_set_t     *supportVarSet;
1717
1718  supportVarSet = bdd_get_support(func);
1719  for (index = 0; index < supportVarSet->n_elts; index++) {
1720    if (var_set_get_elt(supportVarSet, index) == 1)
1721      nSupports++;
1722  }
1723  var_set_free(supportVarSet);
1724  return(nSupports);
1725}
1726
1727
1728/**Function********************************************************************
1729
1730  Synopsis    [Quick checking whether the results of constrain between two
1731  functions are constant.]
1732
1733  Description [Quick checking whether the results of constrain between two
1734  functions are constant. Assumes that 1) f1 != f2 and f1 != f2', and
1735  2) neither f1 nor f2 is constant.]
1736
1737  SideEffects []
1738
1739******************************************************************************/
1740void
1741ImgCheckConstConstrain(mdd_t *f1, mdd_t *f2, int *f21p, int *f21n)
1742{
1743  if (mdd_lequal(f1, f2, 1, 1)) { /* f2 > f1 */
1744    *f21p = 1;
1745    *f21n = 2;
1746  } else if (mdd_lequal(f2, f1, 1, 0)) { /* f2&f1=0 -> f2 < f1' */
1747    *f21p = 0;
1748    *f21n = 2;
1749  } else if (mdd_lequal(f1, f2, 0, 1)) { /* f2 > f1' */
1750    *f21p = 2;
1751    *f21n = 1;
1752  } else if (mdd_lequal(f2, f1, 1, 1)) { /* f2&f1'=0 -> f2 < f1 */
1753    *f21p = 2;
1754    *f21n = 0;
1755  } else {
1756    *f21p = 2;
1757    *f21n = 2;
1758  }
1759}
1760
1761
1762/**Function********************************************************************
1763
1764  Synopsis    [Checks whether the result of constrain is constant.]
1765
1766  Description [Checks whether the result of constrain is constant.]
1767
1768  SideEffects []
1769
1770******************************************************************************/
1771int
1772ImgConstConstrain(mdd_t *func, mdd_t *constraint)
1773{
1774  if (mdd_lequal(constraint, func, 1, 1)) /* func | constraint = 1 */
1775    return(1);
1776  if (mdd_lequal(func, constraint, 1, 0)) /* func | constraint = 0 */
1777    return(0);
1778  return(2); /* non-constant */
1779}
1780
1781
1782/**Function********************************************************************
1783
1784  Synopsis    [Prints vector dependencies with support.]
1785
1786  Description [Prints vector dependencies with support.]
1787
1788  SideEffects []
1789
1790******************************************************************************/
1791void
1792ImgPrintVectorDependency(ImgTfmInfo_t *info, array_t *vector, int verbosity)
1793{
1794  int                   i, j, index, nFuncs, nSupports;
1795  int                   nLambdaLatches, nConstLatches, nIntermediateVars;
1796  int                   count, countStates, total;
1797  int                   start, end;
1798  char                  *support, line[80];
1799  ImgComponent_t        *comp;
1800
1801  if (verbosity == 0 || (!vector))
1802    return;
1803
1804  support = ALLOC(char, sizeof(char) * info->nVars);
1805  memset(support, 0, sizeof(char) * info->nVars);
1806
1807  count = countStates = 0;
1808  nFuncs = array_n(vector);
1809  for (i = 0; i < nFuncs; i++) {
1810    comp = array_fetch(ImgComponent_t *, vector, i);
1811    for (j = 0; j < info->nVars; j++) {
1812      if (comp->support[j]) {
1813        support[j] = 1;
1814        count++;
1815        if (!st_lookup(info->quantifyVarsTable, (char *)(long)j, NIL(char *)))
1816          countStates++;
1817      }
1818    }
1819  }
1820  nSupports = 0;
1821  for (i = 0; i < info->nVars; i++) {
1822    if (support[i])
1823      nSupports++;
1824  }
1825  nLambdaLatches = 0;
1826  nConstLatches = 0;
1827  nIntermediateVars = 0;
1828  for (i = 0; i < nFuncs; i++) {
1829    comp = array_fetch(ImgComponent_t *, vector, i);
1830    index = bdd_top_var_id(comp->var);
1831    if (!support[index])
1832      nLambdaLatches++;
1833    if (ImgSupportCount(info, comp->support) == 0)
1834      nConstLatches++;
1835    if (comp->intermediate)
1836      nIntermediateVars++;
1837  }
1838  fprintf(vis_stdout, "** tfm info: #vars = %d(%d)\n",
1839          info->nVars - nFuncs + nIntermediateVars, info->nVars);
1840  fprintf(vis_stdout, "** tfm info: #input vars = %d\n",
1841          info->nVars - (nFuncs - nIntermediateVars) * 2 - nIntermediateVars);
1842  fprintf(vis_stdout, "** tfm info: #funcs = %d\n", nFuncs);
1843  fprintf(vis_stdout, "** tfm info: #lambda funcs = %d\n", nLambdaLatches);
1844  fprintf(vis_stdout, "** tfm info: #constant funcs = %d\n", nConstLatches);
1845  fprintf(vis_stdout, "** tfm info: #intermediate funcs = %d\n",
1846          nIntermediateVars);
1847  fprintf(vis_stdout,
1848          "Shared size of transition function vector is %10ld BDD nodes\n",
1849          ImgVectorBddSize(vector));
1850  total = nFuncs * nFuncs;
1851  fprintf(vis_stdout,
1852"** tfm info: support distribution (state variables) = %.2f%%(%d out of %d)\n",
1853          (float)countStates / (float)total * 100.0, countStates, total);
1854  total = nFuncs * nSupports;
1855  fprintf(vis_stdout,
1856"** tfm info: support distribution (all variables) = %.2f%% (%d out of %d)\n",
1857          (float)count / (float)total * 100.0, count, total);
1858
1859  if (verbosity < 3) {
1860    FREE(support);
1861    return;
1862  }
1863
1864  fprintf(vis_stdout, "*** function list ***\n");
1865  for (i = 0; i < nFuncs; i++) {
1866    comp = array_fetch(ImgComponent_t *, vector, i);
1867    index = bdd_top_var_id(comp->var);
1868    fprintf(vis_stdout, "[%d] index = %d\n", i, index);
1869  }
1870
1871  start = 0;
1872  end = 74;
1873  if (end >= nFuncs)
1874    end = nFuncs - 1;
1875  while (1) {
1876    fprintf(vis_stdout, "========================================");
1877    fprintf(vis_stdout, "========================================\n");
1878    fprintf(vis_stdout, "     1234567890123456789012345678901234567890");
1879    fprintf(vis_stdout, "12345678901234567890123456789012345\n");
1880    fprintf(vis_stdout, "----------------------------------------");
1881    fprintf(vis_stdout, "----------------------------------------\n");
1882    for (i = 0; i < info->nVars; i++) {
1883      if (!support[i])
1884        continue;
1885      if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
1886        continue;
1887      for (j = start; j <= end; j++) {
1888        comp = array_fetch(ImgComponent_t *, vector, j);
1889        if (comp->support[i])
1890          line[j - start] = '1';
1891        else
1892          line[j - start] = '.';
1893      }
1894      line[j - start] = '\0';
1895      fprintf(vis_stdout, "%4d %s\n", i, line);
1896    }
1897    if (end >= nFuncs - 1)
1898      break;
1899    start += 75;
1900    end += 75;
1901    if (end >= nFuncs)
1902      end = nFuncs - 1;
1903  }
1904  FREE(support);
1905}
1906
1907
1908/**Function********************************************************************
1909
1910  Synopsis    [Returns the percent of non-zero elements in dependency matrix.]
1911
1912  Description [Returns the percent of non-zero elements in dependency matrix.]
1913
1914  SideEffects []
1915
1916******************************************************************************/
1917float
1918ImgPercentVectorDependency(ImgTfmInfo_t *info, array_t *vector, int length,
1919                           int *nLongs)
1920{
1921  int                   i, j, index, nFuncs, nSupports, nLambdaLatches;
1922  int                   count, total;
1923  char                  *support;
1924  ImgComponent_t        *comp;
1925  float                 percent;
1926  int                   *occurs;
1927
1928  support = ALLOC(char, sizeof(char) * info->nVars);
1929  memset(support, 0, sizeof(char) * info->nVars);
1930  occurs = ALLOC(int, sizeof(int) * info->nVars);
1931  memset(occurs, 0, sizeof(int) * info->nVars);
1932
1933  count = 0;
1934  nFuncs = array_n(vector);
1935  for (i = 0; i < nFuncs; i++) {
1936    comp = array_fetch(ImgComponent_t *, vector, i);
1937    for (j = 0; j < info->nVars; j++) {
1938      if (comp->support[j]) {
1939        support[j] = 1;
1940        count++;
1941        occurs[i]++;
1942      }
1943    }
1944  }
1945  nSupports = 0;
1946  for (i = 0; i < info->nVars; i++) {
1947    if (support[i])
1948      nSupports++;
1949  }
1950  nLambdaLatches = 0;
1951  for (i = 0; i < nFuncs; i++) {
1952    comp = array_fetch(ImgComponent_t *, vector, i);
1953    index = bdd_top_var_id(comp->var);
1954    if (!support[index])
1955      nLambdaLatches++;
1956  }
1957  FREE(support);
1958
1959  *nLongs = 0;
1960  for (i = 0; i < info->nVars; i++) {
1961    if (occurs[i] >= length)
1962      (*nLongs)++;
1963  }
1964
1965  total = (nFuncs - nLambdaLatches) * nSupports;
1966  percent = (float)count / (float)total * 100.0;
1967  return(percent);
1968}
1969
1970
1971/**Function********************************************************************
1972
1973  Synopsis    [Writes a gnuplot file with support matrix.]
1974
1975  Description [Writes a gnuplot file with support matrix.]
1976
1977  SideEffects []
1978
1979******************************************************************************/
1980void
1981ImgWriteSupportMatrix(ImgTfmInfo_t *info, array_t *vector,
1982                      array_t *relationArray, char *string)
1983{
1984  int                   i, j, id, nFuncs, nRelations, nRows, nSupports;
1985  int                   *row, col, varType;
1986  char                  *support, **relationSupport;
1987  ImgComponent_t        *comp;
1988  FILE                  *fout;
1989  mdd_t                 *relation, *var;
1990  char                  *filename;
1991
1992  support = ALLOC(char, sizeof(char) * info->nVars);
1993  memset(support, 0, sizeof(char) * info->nVars);
1994  nRows = 0;
1995  if (vector)
1996    nRows += array_n(vector);
1997  if (relationArray)
1998    nRows += array_n(relationArray);
1999  row = ALLOC(int, sizeof(int) * nRows);
2000  if (string)
2001    filename = string;
2002  else
2003    filename = "support.mat";
2004  fout = fopen(filename, "w");
2005
2006  nRows = 0;
2007  if (vector) {
2008    nFuncs = array_n(vector);
2009    for (i = 0; i < nFuncs; i++) {
2010      comp = array_fetch(ImgComponent_t *, vector, i);
2011      if (ImgSupportCount(info, comp->support) == 0) {
2012        row[i] = -1;
2013        continue;
2014      }
2015      row[i] = nRows;
2016      nRows++;
2017      if (info->option->writeSupportMatrixWithYvars) {
2018        var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
2019        id = (int)bdd_top_var_id(var);
2020        support[id] = 1;
2021        mdd_free(var);
2022      }
2023      for (j = 0; j < info->nVars; j++) {
2024        if (comp->support[j])
2025          support[j] = 1;
2026      }
2027    }
2028  } else
2029    nFuncs = 0;
2030
2031  relationSupport = 0;
2032  if (relationArray && array_n(relationArray) > 0) {
2033    comp = ImgComponentAlloc(info);
2034    nRelations = 0;
2035    relationSupport = ALLOC(char *, sizeof(char *) * array_n(relationArray));
2036    for (i = 0; i < array_n(relationArray); i++) {
2037      relation = array_fetch(mdd_t *, relationArray, i);
2038      comp->func = relation;
2039      ImgSupportClear(info, comp->support);
2040      ImgComponentGetSupport(comp);
2041      if (ImgSupportCount(info, comp->support) <= 1) {
2042        row[i + nFuncs] = -1;
2043        relationSupport[i] = NIL(char);
2044        continue;
2045      }
2046      row[i + nFuncs] = nRows;
2047      nRows++;
2048      for (j = 0; j < info->nVars; j++) {
2049        if (comp->support[j])
2050          support[j] = 1;
2051      }
2052      relationSupport[i] = ALLOC(char, sizeof(char) * info->nVars);
2053      memcpy(relationSupport[i], comp->support, sizeof(char) * info->nVars);
2054      nRelations++;
2055    }
2056    comp->func = NIL(mdd_t);
2057    ImgComponentFree(comp);
2058  } else
2059    nRelations = 0;
2060
2061  nSupports = 0;
2062  for (i = 0; i < info->nVars; i++) {
2063    if (support[i]) {
2064      if (!info->option->writeSupportMatrixWithYvars &&
2065          st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
2066        continue;
2067      }
2068      nSupports++;
2069    }
2070  }
2071
2072  col = 0;
2073  for (i = 0; i < info->nVars; i++) {
2074    if (!support[i])
2075      continue;
2076    if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
2077      if (info->option->writeSupportMatrixWithYvars)
2078        varType = 3;
2079      else
2080        continue;
2081    } else if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
2082      varType = 2;
2083    else
2084      varType = 1;
2085    for (j = 0; j < nFuncs; j++) {
2086      comp = array_fetch(ImgComponent_t *, vector, j);
2087      if (comp->support[i]) {
2088        if (info->option->writeSupportMatrixReverseRow) {
2089          if (info->option->writeSupportMatrixReverseCol) {
2090            fprintf(fout, "%d %d %d\n", nSupports - col, nRows - row[j],
2091                    varType);
2092          } else
2093            fprintf(fout, "%d %d %d\n", col + 1, nRows - row[j], varType);
2094        } else {
2095          if (info->option->writeSupportMatrixReverseCol)
2096            fprintf(fout, "%d %d %d\n", nSupports - col, row[j] + 1, varType);
2097          else
2098            fprintf(fout, "%d %d %d\n", col + 1, row[j] + 1, varType);
2099        }
2100      } else if (varType == 3) {
2101        var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
2102        id = (int)bdd_top_var_id(var);
2103        mdd_free(var);
2104        if (id == i) {
2105          if (info->option->writeSupportMatrixReverseRow) {
2106            if (info->option->writeSupportMatrixReverseCol)
2107              fprintf(fout, "%d %d 3\n", nSupports - col, nRows - row[j]);
2108            else
2109              fprintf(fout, "%d %d 3\n", col + 1, nRows - row[j]);
2110          } else {
2111            if (info->option->writeSupportMatrixReverseCol)
2112              fprintf(fout, "%d %d 3\n", nSupports - col, row[j] + 1);
2113            else
2114              fprintf(fout, "%d %d 3\n", col + 1, row[j] + 1);
2115          }
2116        }
2117      }
2118    }
2119    if (relationArray) {
2120      for (j = 0; j < array_n(relationArray); j++) {
2121        if (relationSupport[j] && relationSupport[j][i]) {
2122          if (info->option->writeSupportMatrixReverseRow) {
2123            if (info->option->writeSupportMatrixReverseCol) {
2124              fprintf(fout, "%d %d %d\n", nSupports - col,
2125                      nRows - row[j + nFuncs], varType);
2126            } else {
2127              fprintf(fout, "%d %d %d\n", col + 1, nRows - row[j + nFuncs],
2128                      varType);
2129            }
2130          } else {
2131            if (info->option->writeSupportMatrixReverseCol) {
2132              fprintf(fout, "%d %d %d\n", nSupports - col, row[j + nFuncs] + 1,
2133                      varType);
2134            } else {
2135              fprintf(fout, "%d %d %d\n", col + 1, row[j + nFuncs] + 1,
2136                      varType);
2137            }
2138          }
2139        }
2140      }
2141    }
2142    col++;
2143  }
2144  fclose(fout);
2145  FREE(support);
2146  FREE(row);
2147  if (nRelations) {
2148    for (i = 0; i < nRelations; i++)
2149      FREE(relationSupport[i]);
2150    FREE(relationSupport);
2151  }
2152}
2153
2154
2155/*---------------------------------------------------------------------------*/
2156/* Definition of static functions                                            */
2157/*---------------------------------------------------------------------------*/
2158
2159
2160/**Function********************************************************************
2161
2162  Synopsis    [Comparison function used by qsort.]
2163
2164  Description [Comparison function used by qsort to order the
2165  variables according to their signatures.]
2166
2167  SideEffects [None]
2168
2169******************************************************************************/
2170static int
2171SignatureCompare(int *ptrX, int *ptrY)
2172{
2173  if (signatures[*ptrY] > signatures[*ptrX])
2174    return(1);
2175  if (signatures[*ptrY] < signatures[*ptrX])
2176    return(-1);
2177  return(0);
2178} /* end of SignatureCompare */
2179
2180
2181/**Function********************************************************************
2182
2183  Synopsis    [Compares two function BDD pointers of components.]
2184
2185  Description [Compares two function BDD pointers of components.]
2186
2187  SideEffects []
2188
2189******************************************************************************/
2190static int
2191CompareBddPointer(const void *e1, const void *e2)
2192{
2193  ImgComponent_t        *c1, *c2;
2194  unsigned long         ptr1, ptr2;
2195
2196  c1 = *((ImgComponent_t **)e1);
2197  c2 = *((ImgComponent_t **)e2);
2198
2199  ptr1 = (unsigned long)bdd_pointer(c1->func);
2200  ptr2 = (unsigned long)bdd_pointer(c2->func);
2201
2202  if (ptr1 > ptr2)
2203    return(1);
2204  else if (ptr1 < ptr2)
2205    return(-1);
2206  else
2207    return(0);
2208}
Note: See TracBrowser for help on using the repository browser.