1 | /**CHeaderFile***************************************************************** |
---|
2 | |
---|
3 | FileName [mvf.h] |
---|
4 | |
---|
5 | PackageName [mvf] |
---|
6 | |
---|
7 | Synopsis [Creation and manipulation of MDD-based multi-valued functions.] |
---|
8 | |
---|
9 | Description [This package is used to create and manipulate single output |
---|
10 | functions that take multiple values, and are defined over multi-valued |
---|
11 | variables. Mathematically, such a function is described as, f: Y1 x Y2 x |
---|
12 | ... x Yn --> Yn+1. Each Yi is a finite, ordered set; if Yi is of |
---|
13 | cardinality k, then the elements of Yi are {0, 1, ..., k-1}. We use yi do |
---|
14 | denote a variable over Yi. If<p> |
---|
15 | |
---|
16 | A single MDD over variables y1,...,yn cannot be used to represent f, because |
---|
17 | an MDD can only represent binary-valued functions, not multi-valued |
---|
18 | functions. Instead, to represent f, we use an array of MDDs, of length |
---|
19 | equal to the cardinality of Yn+1. Each MDD of this array is defined over |
---|
20 | y1,...,yn. Furthermore, the minterms for which the ith MDD, fi, evaluates |
---|
21 | to one, are exactly those minterms for which f evaluates to the ith member |
---|
22 | of Yn+1. If f is deterministic, then the intersection of fi and fj, for i |
---|
23 | not equal to j, is empty. If f is completely specified, then the union of |
---|
24 | the fi's is the tautology. The union of the fi's is referred to as the |
---|
25 | "domain" of the function.] |
---|
26 | |
---|
27 | SeeAlso [mdd] |
---|
28 | |
---|
29 | Author [Tom Shiple] |
---|
30 | |
---|
31 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
---|
32 | All rights reserved. |
---|
33 | |
---|
34 | Permission is hereby granted, without written agreement and without license |
---|
35 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
36 | documentation for any purpose, provided that the above copyright notice and |
---|
37 | the following two paragraphs appear in all copies of this software. |
---|
38 | |
---|
39 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
---|
40 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
---|
41 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
---|
42 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
---|
43 | |
---|
44 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
---|
45 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
---|
46 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
---|
47 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
---|
48 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
---|
49 | |
---|
50 | Revision [$Id: mvf.h,v 1.2 2002/09/08 21:42:15 fabio Exp $] |
---|
51 | |
---|
52 | ******************************************************************************/ |
---|
53 | |
---|
54 | #ifndef _MVF |
---|
55 | #define _MVF |
---|
56 | |
---|
57 | /*---------------------------------------------------------------------------*/ |
---|
58 | /* Nested includes */ |
---|
59 | /*---------------------------------------------------------------------------*/ |
---|
60 | #include "vm.h" |
---|
61 | |
---|
62 | /*---------------------------------------------------------------------------*/ |
---|
63 | /* Type declarations */ |
---|
64 | /*---------------------------------------------------------------------------*/ |
---|
65 | typedef array_t Mvf_Function_t; |
---|
66 | |
---|
67 | |
---|
68 | /*---------------------------------------------------------------------------*/ |
---|
69 | /* Macro declarations */ |
---|
70 | /*---------------------------------------------------------------------------*/ |
---|
71 | |
---|
72 | /**Macro*********************************************************************** |
---|
73 | |
---|
74 | Synopsis [Iterates over the components of a multi-valued function.] |
---|
75 | |
---|
76 | Description [This macro iterates over the components of a multi-valued |
---|
77 | function.] |
---|
78 | |
---|
79 | SideEffects [This macro instantiates macros from the array package. Hence |
---|
80 | it is advisable not to nest this macro within array macros.] |
---|
81 | |
---|
82 | SeeAlso [Mvf_FunctionAlloc] |
---|
83 | |
---|
84 | ******************************************************************************/ |
---|
85 | #define Mvf_FunctionForEachComponent( \ |
---|
86 | /* Mvf_Function_t * */ function /* function to iterate components */, \ |
---|
87 | /* int */ i /* local variable for iterator */, \ |
---|
88 | /* mdd_t * */ component /* component of function */ \ |
---|
89 | ) \ |
---|
90 | arrayForEachItem(mdd_t *, (array_t *) function, i, component) |
---|
91 | |
---|
92 | |
---|
93 | /**AutomaticStart*************************************************************/ |
---|
94 | |
---|
95 | /*---------------------------------------------------------------------------*/ |
---|
96 | /* Function prototypes */ |
---|
97 | /*---------------------------------------------------------------------------*/ |
---|
98 | |
---|
99 | EXTERN void Mvf_Init(void); |
---|
100 | EXTERN void Mvf_End(void); |
---|
101 | EXTERN Mvf_Function_t * Mvf_FunctionAlloc(mdd_manager *mddManager, int n); |
---|
102 | EXTERN void Mvf_FunctionAddMintermsToComponent(Mvf_Function_t *function, int i, mdd_t *g); |
---|
103 | EXTERN mdd_t * Mvf_FunctionBuildRelationWithVariable(Mvf_Function_t *function, int mddId); |
---|
104 | EXTERN int Mvf_FunctionReadNumComponents(Mvf_Function_t *function); |
---|
105 | EXTERN mdd_manager * Mvf_FunctionReadMddManager(Mvf_Function_t *function); |
---|
106 | EXTERN Mvf_Function_t * Mvf_FunctionDuplicate(Mvf_Function_t *function); |
---|
107 | EXTERN void Mvf_FunctionFree(Mvf_Function_t *function); |
---|
108 | EXTERN void Mvf_FunctionArrayFree(array_t *functionArray); |
---|
109 | EXTERN mdd_t * Mvf_FunctionObtainComponent(Mvf_Function_t *function, int i); |
---|
110 | EXTERN mdd_t * Mvf_FunctionReadComponent(Mvf_Function_t *function, int i); |
---|
111 | EXTERN Mvf_Function_t * Mvf_FunctionCreateFromVariable(mdd_manager *mddManager, int mddId); |
---|
112 | EXTERN Mvf_Function_t * Mvf_FunctionComposeWithFunctionArray(Mvf_Function_t *f, array_t *mddIdArray, array_t *functionArray); |
---|
113 | EXTERN Mvf_Function_t * Mvf_FunctionComposeWithFunction(Mvf_Function_t *f, int mddId, Mvf_Function_t *g); |
---|
114 | EXTERN mdd_t * Mvf_MddComposeWithFunction(mdd_t *f, int mddId, Mvf_Function_t *g); |
---|
115 | EXTERN boolean Mvf_FunctionTestIsDeterministic(Mvf_Function_t *function); |
---|
116 | EXTERN boolean Mvf_FunctionTestIsCompletelySpecified(Mvf_Function_t *function); |
---|
117 | EXTERN boolean Mvf_FunctionTestIsConstant(Mvf_Function_t *function, int *constantValue); |
---|
118 | EXTERN boolean Mvf_FunctionTestIsNonDeterministicConstant(Mvf_Function_t *function); |
---|
119 | EXTERN mdd_t * Mvf_FunctionComputeDomain(Mvf_Function_t *function); |
---|
120 | EXTERN boolean Mvf_FunctionTestIsWellFormed(Mvf_Function_t *function); |
---|
121 | EXTERN boolean Mvf_FunctionTestIsEqualToFunction(Mvf_Function_t *function1, Mvf_Function_t *function2); |
---|
122 | EXTERN mdd_t * Mvf_FunctionsComputeEquivalentSet(Mvf_Function_t *function1, Mvf_Function_t *function2); |
---|
123 | EXTERN Mvf_Function_t * Mvf_FunctionCofactor(Mvf_Function_t * function, mdd_t * wrtMdd); |
---|
124 | EXTERN Mvf_Function_t * Mvf_FunctionMinimize(Mvf_Function_t *f, mdd_t *c); |
---|
125 | EXTERN long Mvf_FunctionArrayComputeNumBddNodes(array_t * functionArray); |
---|
126 | EXTERN long Mvf_FunctionComputeNumBddNodes(Mvf_Function_t * function); |
---|
127 | EXTERN int Mvf_FunctionFindFirstTrueComponent(Mvf_Function_t * function); |
---|
128 | EXTERN int Mvf_FunctionComputeHashValue(Mvf_Function_t * function); |
---|
129 | EXTERN array_t * Mvf_FunctionComputeSupport(Mvf_Function_t *outMvf, mdd_manager *mddMgr, int *value); |
---|
130 | |
---|
131 | |
---|
132 | /**AutomaticEnd***************************************************************/ |
---|
133 | |
---|
134 | |
---|
135 | #endif /* _MVF */ |
---|
136 | |
---|
137 | |
---|
138 | |
---|