source: vis_dev/vis-2.3/src/mvf/mvfMvf.c @ 14

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

vis2.3
File size: 32.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [mvfMvf.c]
4
5  PackageName [mvf]
6
7  Synopsis    [Routines to create, manipulate and free multi-valued functions.]
8
9  SeeAlso     [mvf.h]
10
11  Author      [Tom Shiple]
12
13  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
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 CALIFORNIA 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  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
25
26  THE UNIVERSITY OF CALIFORNIA 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 CALIFORNIA HAS NO OBLIGATION TO PROVIDE
30  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
31
32******************************************************************************/
33
34#include "mvfInt.h"
35
36static char rcsid[] UNUSED = "$Id: mvfMvf.c,v 1.6 2002/09/08 21:48:24 fabio Exp $";
37
38/**AutomaticStart*************************************************************/
39
40/*---------------------------------------------------------------------------*/
41/* Static function prototypes                                                */
42/*---------------------------------------------------------------------------*/
43
44
45/**AutomaticEnd***************************************************************/
46
47
48/*---------------------------------------------------------------------------*/
49/* Definition of exported functions                                          */
50/*---------------------------------------------------------------------------*/
51
52/**Function********************************************************************
53
54  Synopsis    [Initializes the mvf package.]
55
56  SideEffects []
57
58  SeeAlso     [Mvf_End]
59
60******************************************************************************/
61void
62Mvf_Init(void)
63{
64}
65
66
67/**Function********************************************************************
68
69  Synopsis    [Ends the mvf package.]
70
71  SideEffects []
72
73  SeeAlso     [Mvf_Init]
74
75******************************************************************************/
76void
77Mvf_End(void)
78{
79}
80
81
82/**Function********************************************************************
83
84  Synopsis    [Allocates a multi-valued function of n components.]
85
86  Description [Allocates a multi-valued function of n components.  Each
87  component is initialized to the zero MDD.]
88
89  SideEffects []
90
91  SeeAlso     [Mvf_FunctionAddMintermsToComponent Mvf_FunctionCreateFromVariable]
92
93******************************************************************************/
94Mvf_Function_t *
95Mvf_FunctionAlloc(
96  mdd_manager *mddManager,
97  int n)
98{
99  int      i;
100  array_t *mddArray = array_alloc(mdd_t *, n);
101
102  for (i = 0; i < n; i++) {
103    array_insert(mdd_t *, mddArray, i, mdd_zero(mddManager));
104  }
105  return ((Mvf_Function_t *) mddArray);
106}
107
108
109/**Function********************************************************************
110
111  Synopsis    [Adds a set of minterms to the ith component of a function.]
112
113  Description [Adds a set of minterms, represented by the onset of an MDD g,
114  to the onset of the ith component of a function.  The MDD g is not freed.]
115
116  SideEffects []
117
118  SeeAlso     [Mvf_FunctionAlloc]
119
120******************************************************************************/
121void
122Mvf_FunctionAddMintermsToComponent(
123  Mvf_Function_t *function,
124  int             i,
125  mdd_t          *g)
126{
127  mdd_t   *oldComponent;
128  mdd_t   *newComponent;
129  array_t *mddArray = (array_t *) function;
130
131  assert((i >= 0) && (i < array_n(mddArray)));
132
133  oldComponent = array_fetch(mdd_t *, mddArray, i);
134  newComponent = mdd_or(oldComponent, g, 1, 1);
135  mdd_free(oldComponent);
136  array_insert(mdd_t *, mddArray, i, newComponent);
137}
138
139
140/**Function********************************************************************
141
142  Synopsis [Returns the MDD representation of the relation (var == function).]
143
144  Description [Given a variable x, represented by MDD var "mddId", and a
145  function f:y->z, represented by "function", where x and z take the same
146  number of values, returns the MDD for a (binary) function F(x,y) such that
147  F(x,y) = 1 iff x = f(y).  In the binary case it reduces to F(x,y) = x XNOR
148  f(y).  Intuitively it describes a function of multi-valued variables by the
149  characteristic function of its input-output relation.]
150
151  SideEffects []
152
153******************************************************************************/
154mdd_t *
155Mvf_FunctionBuildRelationWithVariable(
156  Mvf_Function_t *function,
157  int mddId)
158{
159  int          i;
160  mvar_type    mddVar;
161  array_t     *mddArray     = (array_t *) function;
162  mdd_manager *mddManager   = Mvf_FunctionReadMddManager(function);
163  mdd_t       *sumOfFactors = mdd_zero(mddManager);
164 
165  mddVar = array_fetch(mvar_type, mdd_ret_mvar_list(mddManager), mddId);
166  assert(mddVar.values == Mvf_FunctionReadNumComponents(function));
167
168  for (i = 0; i < array_n(mddArray); i++) {
169    mdd_t *varLiteral;
170    mdd_t *factor;
171    mdd_t *tmp;
172    mdd_t *fComponent = array_fetch(mdd_t *, mddArray, i);
173
174    varLiteral = mdd_eq_c(mddManager, mddId, i);
175    factor = mdd_and(fComponent, varLiteral, 1, 1);
176    mdd_free(varLiteral);
177
178    /* Take the or of the sumOfFactors so far and the new factor */
179    tmp = mdd_or(sumOfFactors, factor, 1, 1);
180    mdd_free(factor);
181    mdd_free(sumOfFactors);
182    sumOfFactors = tmp;
183  } 
184
185  return sumOfFactors;
186} 
187
188
189/**Function********************************************************************
190
191  Synopsis    [Returns the number of components of a multi-valued function.]
192
193  Description [Returns the number of components of a multi-valued function.
194  This is the same number as the value of the parameter passed to
195  Mvf_FunctionAlloc.]
196
197  SideEffects []
198
199  SeeAlso     [Mvf_FunctionAlloc]
200
201******************************************************************************/
202int
203Mvf_FunctionReadNumComponents(
204  Mvf_Function_t *function)
205{
206  return (array_n((array_t *) function));
207}
208
209
210/**Function********************************************************************
211
212  Synopsis    [Returns the MDD manager of a multi-valued function.]
213
214  Description [Returns the MDD manager of a multi-valued function.  This
215  procedure assumes that the function has at least one component.]
216
217  SideEffects []
218
219  SeeAlso     [Mvf_FunctionAlloc]
220
221******************************************************************************/
222mdd_manager *
223Mvf_FunctionReadMddManager(
224  Mvf_Function_t *function)
225{
226  mdd_t *component = array_fetch(mdd_t *, (array_t *) function, 0);
227 
228  return (mdd_get_manager(component));
229}
230
231
232/**Function********************************************************************
233
234  Synopsis    [Duplicates a multi-valued output function.]
235
236  Description [Returns a new multi-valued output function, whose constituent
237  MDDs have been duplicated. Assumes that function is not NULL.]
238
239  SideEffects []
240
241  SeeAlso     [Mvf_FunctionFree]
242
243******************************************************************************/
244Mvf_Function_t *
245Mvf_FunctionDuplicate(
246  Mvf_Function_t *function)
247{
248  return ((Mvf_Function_t *) mdd_array_duplicate((array_t *) function));
249}
250
251
252/**Function********************************************************************
253
254  Synopsis    [Frees a multi-valued output function.]
255
256  Description [Frees a multi-valued output function. Does nothing if
257  function is NULL.]
258 
259  SideEffects []
260
261  SeeAlso     [Mvf_FunctionAlloc]
262
263******************************************************************************/
264void
265Mvf_FunctionFree(
266  Mvf_Function_t *function)
267{
268  mdd_array_free((array_t *) function);
269}
270
271
272/**Function********************************************************************
273
274  Synopsis    [Frees an array of multi-valued output functions.]
275
276  Description [Frees an array of multi-valued output functions.  Does nothing
277  if functionArray is NULL.]
278
279  SideEffects []
280
281  SeeAlso     [Mvf_FunctionFree]
282
283******************************************************************************/
284void
285Mvf_FunctionArrayFree(
286  array_t *functionArray)
287{
288  int i;
289
290  if (functionArray != NIL(array_t)) {
291    for (i = 0; i < array_n(functionArray); i++) {
292      Mvf_Function_t *function = array_fetch(Mvf_Function_t *, functionArray, i);
293      Mvf_FunctionFree(function);
294    }
295    array_free(functionArray);
296  }
297}
298
299/**Function********************************************************************
300
301  Synopsis [Returns a copy of the ith component of a multi-valued function.]
302
303  Synopsis [Returns a copy of the MDD giving the minterms for which a
304  multi-valued function evaluates to its ith value.]
305
306  SideEffects []
307
308  SeeAlso     [Mvf_FunctionAlloc Mvf_FunctionCreateFromVariable]
309
310******************************************************************************/
311mdd_t *
312Mvf_FunctionObtainComponent(
313  Mvf_Function_t *function,
314  int i)
315{
316  mdd_t *component = array_fetch(mdd_t *, (array_t *) function, i);
317  return (mdd_dup(component));
318}
319
320/**Function********************************************************************
321
322  Synopsis [Returns the ith component of a multi-valued function.]
323
324  Synopsis [Returns the MDD giving the minterms for which a
325  multi-valued function evaluates to its ith value. The user should not free
326  this MDD.]
327
328  SideEffects []
329
330  SeeAlso     [Mvf_FunctionObtainComponent Mvf_FunctionAlloc
331  Mvf_FunctionCreateFromVariable]
332
333******************************************************************************/
334mdd_t *
335Mvf_FunctionReadComponent(
336  Mvf_Function_t *function,
337  int i)
338{
339  mdd_t *component = array_fetch(mdd_t *, (array_t *) function, i);
340  return (component);
341}
342
343
344/**Function********************************************************************
345
346  Synopsis [Creates the multi-output function for a variable.]
347
348  Description [Given a variable, creates a function with as many components as
349  values of the variable.  The ith component of the function is true exactly
350  when the variable is equal to the ith value (i.e. fi(x) = (x==i), where x is
351  the variable specified by mddId).  For the case where x is binary valued,
352  the result is \[!x, x\]. Assumes that mddId is non-negative.]
353
354  SideEffects []
355
356  SeeAlso [Mvf_FunctionAlloc]
357
358******************************************************************************/
359Mvf_Function_t *
360Mvf_FunctionCreateFromVariable(
361  mdd_manager *mddManager,
362  int mddId)
363{
364  int        i;
365  array_t   *mvar_list = mdd_ret_mvar_list(mddManager);
366  mvar_type  varInfo;
367  array_t   *result;
368
369  assert(mddId >= 0);
370
371  varInfo   = array_fetch(mvar_type, mvar_list, mddId);
372  result    = array_alloc(mdd_t *, varInfo.values);
373
374  for(i = 0; i < varInfo.values; i++) {
375    mdd_t *literal;
376
377    literal = mdd_eq_c(mddManager, mddId, i);
378    array_insert(mdd_t *, result, i, literal);
379  } 
380
381  return ((Mvf_Function_t *) result);
382} 
383
384
385/**Function********************************************************************
386
387  Synopsis [Substitutes a set of variables by a set of functions in a function.]
388
389  Description [Given a multi-valued function f, an array of variables
390  x1,...,xk, and an array of multi-valued functions g1,...,gk, iteratively
391  calls Mvf_MddComposeWithFunction to substitute each xi by gi.  The
392  parameters of the ith call to Mvf_MddComposeWithFunction are the result of
393  composing the first i-1 variables, xi, and gi.  The multi-valued function gi
394  must not depend on xi.]
395
396  SideEffects []
397
398  SeeAlso     [Mvf_MddComposeWithFunction]
399
400******************************************************************************/
401Mvf_Function_t *
402Mvf_FunctionComposeWithFunctionArray(
403  Mvf_Function_t *f,
404  array_t        *mddIdArray /* of int */,   
405  array_t        *functionArray /* of Mvf_Function_t* */)
406{
407  Mvf_Function_t *result;
408  int i;
409
410  assert(array_n(mddIdArray) == array_n(functionArray));
411
412  /* Make an initial copy of the function */
413  result = Mvf_FunctionDuplicate(f);
414
415  for(i = 0; i < array_n(mddIdArray); i++) {
416    Mvf_Function_t *tmp;
417    int             mddId = array_fetch(int, mddIdArray, i);
418    Mvf_Function_t *g     = array_fetch(Mvf_Function_t *, functionArray, i);
419   
420    tmp = Mvf_FunctionComposeWithFunction(result, mddId, g);
421
422    Mvf_FunctionFree(result);
423    result = tmp;
424  } 
425
426  return result;
427}
428
429
430/**Function********************************************************************
431
432  Synopsis [Substitutes a variable by a function in a function.]
433
434  Description [Given a multi-valued function f, a variable x (mddId), and a
435  multi-valued function g, the procedure replaces every appearance of x in f
436  by function g.  That is, if the function f is f(..., x, ...), then the
437  result is f(..., g(), ...).  The number of values that x can take and the
438  number of components of g must be equal. The algorithm first computes the
439  sum of factors (x==i)*gi for every value i in the domain of x, where gi is
440  the ith component of g.  Then, for each component fi of f, the sum of
441  factors is conjuncted with fi, and x is existentially quantified. The
442  function g must not depend on x.  The result depends on all the variables of
443  g and all the variables of f, except for x.]
444
445  SideEffects []
446
447  SeeAlso     [Mvf_MddComposeWithFunction]
448
449******************************************************************************/
450Mvf_Function_t *
451Mvf_FunctionComposeWithFunction(
452  Mvf_Function_t *f,
453  int             mddId,
454  Mvf_Function_t *g)
455{
456  mdd_t   *sumOfFactors;
457  array_t *result;
458  array_t *values;
459  int      i;
460  mdd_manager *mddManager = Mvf_FunctionReadMddManager(f);
461
462  /* Allocate array to hold values for the literal and the result */
463  result = array_alloc(mdd_t *, array_n(f));
464
465  /*
466   * Create the sum of factors (x==i * gi). This function will verify that the
467   * domain of x and the range of g have the same cardinality.
468   */
469  sumOfFactors = Mvf_FunctionBuildRelationWithVariable(g, mddId);
470
471  /*
472   * Result is an array of mdd_t * , result[i] = Exists(x) (f[i] * sumOfFactors)
473   * The array values holds now the index of the variable to smooth out.
474   */
475  values = array_alloc(int, 1);
476  array_insert(int, values, 0, mddId);
477  for(i = 0; i < array_n(f); i++) {
478    mdd_t *functionUnit = array_fetch(mdd_t *, f, i);
479    mdd_t *tmp          = mdd_and_smooth(mddManager, functionUnit, sumOfFactors, values);
480
481    array_insert(mdd_t *, result, i, tmp);
482  } 
483
484  /* Clean up */
485  array_free(values);
486  mdd_free(sumOfFactors);
487
488  return ((Mvf_Function_t *) result);
489}
490
491
492/**Function********************************************************************
493
494  Synopsis    [Substitutes a variable by a function in an mdd_t *.]
495
496  Description [Given a binary-valued function f, a variable x, and a
497  multi-valued function g, the procedure replaces every appearance of x in f
498  by function g.  That is, if the function f is f(..., x, ...), then the
499  result is f(..., g(), ...). The number of values that x can take and the
500  number of components of g must be equal. The algorithm first computes the
501  sum of factors (x==i)*gi for every value i in the domain of x, where gi is
502  the ith component of g, then conjuncts this with f, and finally
503  existentially quantifies x.  The function g must not depend on x.  The
504  result depends on all the variables of g and all the variables of f, except
505  for x.]
506
507  SideEffects []
508
509******************************************************************************/
510mdd_t *
511Mvf_MddComposeWithFunction(
512  mdd_t          *f,
513  int             mddId,
514  Mvf_Function_t *g)
515{
516  mdd_t       *sumOfFactors;
517  mdd_t       *result;
518  array_t     *values;
519  mdd_manager *mddManager = mdd_get_manager(f);
520 
521  /*
522   * Create the sum of factors (x==i * gi). This function will verify that the
523   * domain of x and the range of g have the same cardinality.
524   */
525  sumOfFactors = Mvf_FunctionBuildRelationWithVariable(g, mddId);
526
527  /* Result is an mdd_t * , result = Exists(x) (f * sumOfFactors) */
528  values = array_alloc(int, 1);
529  array_insert(int, values, 0, mddId);
530  result = mdd_and_smooth(mddManager, f, sumOfFactors, values);
531
532  /* Clean up */
533  array_free(values);
534  mdd_free(sumOfFactors);
535
536  return result;
537} 
538
539
540/**Function********************************************************************
541
542  Synopsis [Returns true if a multi-valued function is deterministic, else
543  false.]
544
545  Description [Returns true if a multi-valued function is deterministic, else
546  false.  A function is deterministic if, for every minterm over the input
547  space of the function, the function takes at most one value. The complexity
548  of this procedure is linear in the number of values the function can
549  take.]
550
551  SideEffects []
552
553  SeeAlso     [Mvf_FunctionTestIsCompletelySpecified Mvf_FunctionTestIsWellFormed]
554
555******************************************************************************/
556boolean
557Mvf_FunctionTestIsDeterministic(
558  Mvf_Function_t *function)
559{
560  int      i;
561  array_t *mddArray      = (array_t *) function;
562  int      numComponents = array_n(mddArray);
563  mdd_t   *sum;
564
565  if (numComponents == 0) {
566    return TRUE;
567  }
568 
569  sum = mdd_dup(array_fetch(mdd_t *, mddArray, 0));
570 
571  for (i = 1; i < numComponents; i++) {
572    mdd_t *temp         = sum;
573    mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);
574    boolean intersectionIsEmpty = mdd_lequal(ithComponent, sum, 1, 0);
575   
576    /* If the intersection is not empty, then return FALSE. */
577    if (!intersectionIsEmpty) {
578      mdd_free(sum);
579      return FALSE;
580    }
581
582    sum = mdd_or(temp, ithComponent, 1, 1);
583    mdd_free(temp);
584  }
585  mdd_free(sum);
586 
587  /* The components are pairwise disjoint. */
588  return TRUE;
589}
590
591
592/**Function********************************************************************
593
594  Synopsis [Returns true if a multi-valued function is completely specified, else
595  false.]
596
597  Description [Returns true if a multi-valued function is completely
598  specified, else false.  A function is completely specified if, for every
599  minterm over the input space of the function, the function takes at least
600  one value. The complexity of this procedure is linear in the number of
601  values the function can take.]
602
603  SideEffects []
604
605  SeeAlso     [Mvf_FunctionTestIsDeterministic Mvf_FunctionTestIsWellFormed]
606
607******************************************************************************/
608boolean
609Mvf_FunctionTestIsCompletelySpecified(
610  Mvf_Function_t *function)
611{
612  mdd_t   *sum            = Mvf_FunctionComputeDomain(function);
613  boolean  sumIsTautology = mdd_is_tautology(sum, 1);
614
615  mdd_free(sum);
616  return sumIsTautology;
617}
618
619
620/**Function********************************************************************
621
622  Synopsis [Returns true if a multi-valued function is constant, else
623  false.]
624
625  Description [Returns true if a multi-valued function is constant, else
626  false.  A function is constant if exactly one component is the tautology,
627  and the remaining components are zero.  If the function is a constant, then
628  "value" is set to the constant value of the function. The complexity of this
629  procedure is linear in the number of values the function can take.]
630
631  SideEffects []
632
633  SeeAlso     [Mvf_FunctionTestIsNonDeterministicConstant]
634
635******************************************************************************/
636boolean
637Mvf_FunctionTestIsConstant(
638  Mvf_Function_t *function,
639  int            *constantValue /* return value */ )
640{
641  int      i;
642  array_t *mddArray      = (array_t *) function;
643  int      numComponents = array_n(mddArray);
644  int      numTautComps  = 0;
645
646  for (i = 0; i < numComponents; i++) {
647    mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);
648
649    if (mdd_is_tautology(ithComponent, 1)) {
650      *constantValue = i;
651      numTautComps++;
652    }
653    else if (!mdd_is_tautology(ithComponent, 0)) {
654      /* this component is not 1 nor 0, so function can't be a constant */
655      return FALSE;
656    }
657    /* else, must be the zero function */
658  }
659
660  return (numTautComps == 1);
661}
662
663
664/**Function********************************************************************
665
666  Synopsis [Returns true if a multi-valued function is a non-deterministic
667  constant, else false.]
668
669  Description [Returns true if a multi-valued function is a non-deterministic
670  constant, else false.  A function is a non-deterministic constant if more
671  than one component is the tautology, and the remaining components are zero.
672  The complexity of this procedure is linear in the number of values the
673  function can take.]
674
675  SideEffects []
676
677  SeeAlso     [Mvf_FunctionTestIsConstant]
678
679******************************************************************************/
680boolean
681Mvf_FunctionTestIsNonDeterministicConstant(
682  Mvf_Function_t *function)
683{
684  int      i;
685  array_t *mddArray      = (array_t *) function;
686  int      numComponents = array_n(mddArray);
687  int      numTautComps  = 0;
688
689  for (i = 0; i < numComponents; i++) {
690    mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);
691
692    if (mdd_is_tautology(ithComponent, 1)) {
693      numTautComps++;
694    }
695    else if (!mdd_is_tautology(ithComponent, 0)) {
696      /* this component is not 1 nor 0, so function can't be a non-det constant */
697      return FALSE;
698    }
699    /* else, must be the zero function */
700  }
701
702  return (numTautComps > 1);
703}
704
705
706/**Function********************************************************************
707
708  Synopsis    [Computes the domain of a multi-valued function.]
709
710  Description [Returns an MDD representing the set of minterms which turn on
711  some component of a function.  In other words, returns the union of the
712  onsets of the components.  The domain is the tautology if and only if the
713  function is completely specified.]
714
715  SideEffects []
716
717  SeeAlso     [Mvf_FunctionTestIsCompletelySpecified]
718
719******************************************************************************/
720mdd_t *
721Mvf_FunctionComputeDomain(
722  Mvf_Function_t *function)
723{
724  array_t     *mddArray   = (array_t *) function;
725  mdd_manager *mddManager = Mvf_FunctionReadMddManager(function);
726  mdd_t       *sum        = mdd_multiway_or(mddManager, mddArray);
727
728  return sum;
729}
730
731
732/**Function********************************************************************
733
734  Synopsis    [Returns true if a function is deterministic and completely
735  specified, else false.]
736
737  SideEffects []
738
739  SeeAlso     [Mvf_FunctionTestIsDeterministic
740  Mvf_FunctionTestIsCompletelySpecified]
741
742******************************************************************************/
743boolean
744Mvf_FunctionTestIsWellFormed(
745  Mvf_Function_t *function)
746{
747  return (Mvf_FunctionTestIsDeterministic(function) 
748          && Mvf_FunctionTestIsCompletelySpecified(function));
749}
750
751
752/**Function********************************************************************
753
754  Synopsis    [Returns true if two multi-valued functions are equal, else false.]
755
756  Description [Returns true if two multi-valued functions are equal, else
757  false.  Two functions are equal if they have the same number of components,
758  and the ith component of one is equal to the ith component of the other.]
759
760  SideEffects []
761
762******************************************************************************/
763boolean
764Mvf_FunctionTestIsEqualToFunction(
765  Mvf_Function_t *function1,
766  Mvf_Function_t *function2)
767{
768  int      i;
769  array_t *mddArray1     = (array_t *) function1;
770  array_t *mddArray2     = (array_t *) function2;
771  int      numComponents = array_n(mddArray1);
772
773  if (numComponents != array_n(mddArray2)) {
774    return FALSE;
775  }
776
777  for (i = 0; i < numComponents; i++) {
778    mdd_t *mdd1 = array_fetch(mdd_t *, mddArray1, i);
779    mdd_t *mdd2 = array_fetch(mdd_t *, mddArray2, i);
780    if (!mdd_equal(mdd1, mdd2)) {
781      return FALSE;
782    }
783  }
784
785  return TRUE;
786}
787
788
789/**Function********************************************************************
790
791  Synopsis    [Returns the set of minterms on which two functions agree.]
792
793  Description [Returns the set of minterms on which two functions agree.  For
794  f = \[f1, f2, ..., fn\] and g = \[g1, g2, ..., gn\], the returned set is:
795  AND(i = 1, ..., n) (fi XNOR gi).  For the special case where f and g are
796  binary valued, this function computes (f XNOR g).  It is an error if the two
797  functions have a different number of components.]
798
799  SideEffects []
800
801******************************************************************************/
802mdd_t *
803Mvf_FunctionsComputeEquivalentSet(
804  Mvf_Function_t *function1,
805  Mvf_Function_t *function2)
806{
807  int          i;
808  array_t     *mddArray1     = (array_t *) function1;
809  array_t     *mddArray2     = (array_t *) function2;
810  int          numComponents = array_n(mddArray1);
811  mdd_manager *mddManager    = Mvf_FunctionReadMddManager(function1);
812  mdd_t       *product       = mdd_one(mddManager);
813
814  assert(numComponents == array_n(mddArray2));
815 
816  for (i = 0; i < numComponents; i++) {
817    mdd_t *mdd1 = array_fetch(mdd_t *, mddArray1, i);
818    mdd_t *mdd2 = array_fetch(mdd_t *, mddArray2, i);
819    mdd_t *xnor = mdd_xnor(mdd1, mdd2);
820    mdd_t *temp = product;
821
822    product = mdd_and(temp, xnor, 1, 1);
823    mdd_free(temp);
824    mdd_free(xnor);
825  }
826
827  return product;
828}
829
830 
831/**Function********************************************************************
832
833  Synopsis [Calls bdd_cofactor on each component of a multi-valued function.]
834
835  Description [Calls bdd_cofactor on each component of a multi-valued
836  function, cofactoring with respect to wrtMDD. Returns the cofactored
837  function. It is an error to call this function with a multi-valued
838  function that contains null MDDs or with a null wrtMdd.]
839
840  SideEffects []
841
842******************************************************************************/
843Mvf_Function_t *
844Mvf_FunctionCofactor(
845  Mvf_Function_t * function,
846  mdd_t          * wrtMdd)
847{
848  int      i;
849  array_t *mddArray      = (array_t *) function;
850  int      numComponents = array_n(mddArray);
851  array_t *newFunction   = array_alloc(mdd_t *, numComponents);
852 
853  for(i = 0; i < numComponents; i++) {
854    mdd_t *component = array_fetch(mdd_t *, mddArray, i);
855    mdd_t *cofactor  = bdd_cofactor(component, wrtMdd);
856
857    array_insert(mdd_t *, newFunction, i, cofactor);
858  }
859  return((Mvf_Function_t *)newFunction);
860}
861
862
863/**Function********************************************************************
864
865  Synopsis [Calls bdd_minimize on each component of a multi-valued function.]
866
867  Description [Calls bdd_minimize on each component of a multi-valued function
868  f, minimizing with respect to the care function c.  The returned function
869  agrees with f wherever c is true, and may or may not agree with f wherever c
870  is false. It is an error to call this function with a multi-valued function
871  that contains null MDDs or with a null care.]
872
873  SideEffects []
874
875******************************************************************************/
876Mvf_Function_t *
877Mvf_FunctionMinimize(
878  Mvf_Function_t *f,
879  mdd_t          *c)
880{
881  int      i;
882  array_t *mddArray      = (array_t *) f;
883  int      numComponents = array_n(mddArray);
884  array_t *newFunction   = array_alloc(mdd_t *, numComponents);
885 
886  for(i = 0; i < numComponents; i++) {
887    mdd_t *component = array_fetch(mdd_t *, mddArray, i);
888    mdd_t *minimize  = bdd_minimize(component, c);
889
890    array_insert(mdd_t *, newFunction, i, minimize);
891  }
892  return((Mvf_Function_t *)newFunction);
893}
894
895
896/**Function********************************************************************
897
898  Synopsis [Returns the number of BDD nodes of an array of multi-valued
899  functions.]
900
901  Description [Returns the number of BDD nodes of an array of multi-valued
902  functions. A node shared by several functions is counted only once.]
903
904  SideEffects []
905
906******************************************************************************/
907long
908Mvf_FunctionArrayComputeNumBddNodes(
909  array_t * functionArray)
910{
911  int      i;
912  long     numNodes;
913  array_t *mddArray = array_alloc(mdd_t *, 0);
914
915  /* Build an array of all MDDs */
916  for(i = 0; i < array_n(functionArray); i++) {
917    int      j;
918    array_t *function = (array_t *)array_fetch(Mvf_Function_t *, functionArray, i);
919
920    for(j = 0; j < array_n(function); j++) {
921      mdd_t *component = array_fetch(mdd_t *, function, j);
922      array_insert_last(mdd_t *, mddArray, component);
923    }
924  }
925 
926  /* Compute the reduced number of bdd nodes */
927  numNodes = mdd_size_multiple(mddArray);
928  array_free(mddArray);
929 
930  return(numNodes);
931}
932
933
934/**Function********************************************************************
935
936  Synopsis [Returns the number of BDD nodes of a multi-valued function.]
937
938  SideEffects []
939
940******************************************************************************/
941long
942Mvf_FunctionComputeNumBddNodes(
943  Mvf_Function_t * function)
944{
945  return(mdd_size_multiple((array_t *)function));
946}
947
948
949/**Function********************************************************************
950
951  Synopsis [Returns the index of the first component of a multi-valued
952  function that is equal to the tautology.]
953
954  Description [Returns the index of the first component of a multi-valued
955  function that is equal to the tautology. If the multi-valued function is
956  deterministic, this component is unique. Returns -1 if such a component is
957  not found. It is an error to call this function with a multi-valued function
958  that contains null MDDs.]
959
960  SideEffects []
961
962******************************************************************************/
963int
964Mvf_FunctionFindFirstTrueComponent(
965  Mvf_Function_t * function)
966{
967  int      i;
968  array_t *mddArray = (array_t *) function;
969 
970  for(i = 0; i < array_n(mddArray); i++) {
971    mdd_t *component = array_fetch(mdd_t *, mddArray, i);
972    if (mdd_is_tautology(component, 1)) {
973      return(i);
974    }
975  }
976  return(-1);
977}
978
979/**Function********************************************************************
980
981  Synopsis [Hashes A multi-valued function.]
982
983  Description [Hashes A multi-valued function. Each component's top variable id
984  is multiplied by the index of component (+ 1). Returns the sum of this computation
985  on every component. It is an error to call this function with a null
986  multi-valued function.]
987
988  SideEffects []
989
990******************************************************************************/
991int
992Mvf_FunctionComputeHashValue(
993  Mvf_Function_t * function)
994{
995  int      i;
996  int      result   = 0;
997  array_t *mddArray = (array_t *) function;
998 
999  for(i = 0; i < array_n(mddArray); i++) {
1000    mdd_t *component = array_fetch(mdd_t *, mddArray, i);
1001    result += (mdd_top_var_id(component)) * (i + 1);
1002  }
1003  return(result);
1004}
1005
1006
1007
1008/**Function********************************************************************
1009
1010  Synopsis [Computes the variables in the true support of a function.]
1011
1012  Description [Computes the variables in the true support of a function.  Does
1013  this by taking the union of the result of mdd_get_support on each component
1014  of the function.  Returns the support as an (ascending) ordered array of MDD
1015  ids. If the function is a constant, then a NULL array is returned, and the
1016  constant value of the function is written in the "value" variable.]
1017
1018  SideEffects []
1019
1020  SeeAlso     [Mvf_FunctionTestIsConstant]
1021
1022******************************************************************************/
1023array_t *
1024Mvf_FunctionComputeSupport(
1025  Mvf_Function_t *function,
1026  mdd_manager *mddMgr,
1027  int *value)
1028{
1029  int        i;
1030  mdd_t     *component;
1031  array_t   *totalSupportArray;
1032  var_set_t *totalSupportSet;
1033  int        numMddVars = array_n(mdd_ret_mvar_list(mddMgr));
1034
1035  /*
1036   * Handle the case where function is just a constant.
1037   */
1038  if (Mvf_FunctionTestIsConstant(function, value)) {
1039    return NIL(array_t);
1040  }
1041 
1042  /*
1043   * Accumulate the union of supports of the function components into a bit
1044   * array.
1045   */
1046  totalSupportArray = array_alloc(int, 0);
1047  totalSupportSet   = var_set_new(numMddVars);
1048
1049  Mvf_FunctionForEachComponent(function, i, component) {
1050    int      j;
1051    int      mddVarId;
1052    array_t *support = mdd_get_support(mddMgr, component);
1053
1054    arrayForEachItem(int, support, j, mddVarId) {
1055      var_set_set_elt(totalSupportSet, mddVarId);
1056    }
1057    array_free(support);
1058  }
1059 
1060  /* Convert the bit array to an array of mdd ids. */
1061  for (i = 0; i < numMddVars; i++) {
1062    if (var_set_get_elt(totalSupportSet, i)) {
1063      array_insert_last(int, totalSupportArray, i);
1064    }
1065  }
1066  var_set_free(totalSupportSet);
1067
1068  return totalSupportArray;
1069}
1070
1071/*---------------------------------------------------------------------------*/
1072/* Definition of internal functions                                          */
1073/*---------------------------------------------------------------------------*/
1074
1075
1076/*---------------------------------------------------------------------------*/
1077/* Definition of static functions                                            */
1078/*---------------------------------------------------------------------------*/
1079
Note: See TracBrowser for help on using the repository browser.