1 | /**CFile*********************************************************************** |
---|
2 | |
---|
3 | FileName [tblIdentity.c] |
---|
4 | |
---|
5 | PackageName [tbl] |
---|
6 | |
---|
7 | Synopsis [Functions used to detect special types of table. Used, for |
---|
8 | instance, in network sweeping.] |
---|
9 | |
---|
10 | SeeAlso [tbl.h] |
---|
11 | |
---|
12 | Author [Fabio Somenzi] |
---|
13 | |
---|
14 | Copyright [Copyright (c) 2009, Regents of the University of Colorado |
---|
15 | |
---|
16 | All rights reserved. |
---|
17 | |
---|
18 | Redistribution and use in source and binary forms, with or without |
---|
19 | modification, are permitted provided that the following conditions |
---|
20 | are met: |
---|
21 | |
---|
22 | Redistributions of source code must retain the above copyright |
---|
23 | notice, this list of conditions and the following disclaimer. |
---|
24 | |
---|
25 | Redistributions in binary form must reproduce the above copyright |
---|
26 | notice, this list of conditions and the following disclaimer in the |
---|
27 | documentation and/or other materials provided with the distribution. |
---|
28 | |
---|
29 | Neither the name of the University of Colorado nor the names of its |
---|
30 | contributors may be used to endorse or promote products derived from |
---|
31 | this software without specific prior written permission. |
---|
32 | |
---|
33 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
34 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
35 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
36 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
37 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
38 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
39 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
40 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
41 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
42 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
43 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
44 | POSSIBILITY OF SUCH DAMAGE.] |
---|
45 | |
---|
46 | ******************************************************************************/ |
---|
47 | #include "tblInt.h" |
---|
48 | |
---|
49 | static char rcsid[] UNUSED = "$Id: tblIdentity.c,v 1.1 2009/04/11 07:10:15 fabio Exp $"; |
---|
50 | |
---|
51 | /*---------------------------------------------------------------------------*/ |
---|
52 | /* Constant declarations */ |
---|
53 | /*---------------------------------------------------------------------------*/ |
---|
54 | |
---|
55 | /*---------------------------------------------------------------------------*/ |
---|
56 | /* Stucture declarations */ |
---|
57 | /*---------------------------------------------------------------------------*/ |
---|
58 | |
---|
59 | |
---|
60 | /*---------------------------------------------------------------------------*/ |
---|
61 | /* Type declarations */ |
---|
62 | /*---------------------------------------------------------------------------*/ |
---|
63 | |
---|
64 | |
---|
65 | /*---------------------------------------------------------------------------*/ |
---|
66 | /* Variable declarations */ |
---|
67 | /*---------------------------------------------------------------------------*/ |
---|
68 | |
---|
69 | |
---|
70 | /*---------------------------------------------------------------------------*/ |
---|
71 | /* Macro declarations */ |
---|
72 | /*---------------------------------------------------------------------------*/ |
---|
73 | |
---|
74 | |
---|
75 | /**AutomaticStart*************************************************************/ |
---|
76 | |
---|
77 | /*---------------------------------------------------------------------------*/ |
---|
78 | /* Static function prototypes */ |
---|
79 | /*---------------------------------------------------------------------------*/ |
---|
80 | |
---|
81 | |
---|
82 | /**AutomaticEnd***************************************************************/ |
---|
83 | |
---|
84 | /**Function******************************************************************** |
---|
85 | |
---|
86 | Synopsis[Check whether a table describes an identity function.] |
---|
87 | |
---|
88 | Description [This function checks whether a table describes an |
---|
89 | identity. An identity table has exactly one input and one output |
---|
90 | variable, which takes the same value as the input.] |
---|
91 | |
---|
92 | SideEffects [] |
---|
93 | |
---|
94 | SeeAlso [] |
---|
95 | |
---|
96 | ******************************************************************************/ |
---|
97 | boolean |
---|
98 | Tbl_TableIsIdentity( |
---|
99 | Tbl_Table_t *table |
---|
100 | ) |
---|
101 | { |
---|
102 | Var_Variable_t *invar = NIL(Var_Variable_t), *outvar = NIL(Var_Variable_t); |
---|
103 | Var_Variable_t *var; |
---|
104 | int colNum, rowNum; |
---|
105 | Tbl_Entry_t *inputEntry, *outputEntry, *defaultEntry, *cumulative; |
---|
106 | boolean result; |
---|
107 | #if 0 |
---|
108 | Mvf_Function_t *outMvf, *inMvf, *identMvf; |
---|
109 | array_t *mvarValues; |
---|
110 | array_t *inMvfArray; |
---|
111 | Tbl_Table_t *ident; |
---|
112 | #endif |
---|
113 | |
---|
114 | if (Tbl_TableReadNumInputs(table) != 1) return FALSE; |
---|
115 | if (Tbl_TableReadNumOutputs(table) != 1) return FALSE; |
---|
116 | |
---|
117 | Tbl_TableForEachInputVar(table,colNum,var) { |
---|
118 | invar = var; |
---|
119 | } |
---|
120 | |
---|
121 | Tbl_TableForEachOutputVar(table,colNum,var) { |
---|
122 | outvar = var; |
---|
123 | } |
---|
124 | |
---|
125 | if (!Var_VariablesTestHaveSameDomain(invar,outvar)) return FALSE; |
---|
126 | |
---|
127 | /* We test the following condition. If a table specifies a value |
---|
128 | * for all inputs and all rows are consistent with the identity, |
---|
129 | * then the table is an identity. A normal default declaration is |
---|
130 | * treated as a row whose input and output parts equal the default |
---|
131 | * value. An equality default declaration is treated like a row |
---|
132 | * with equality output entry and don't care input entry. |
---|
133 | * Completeness and nondeterminism are implicitly tested by this |
---|
134 | * criterion. |
---|
135 | */ |
---|
136 | defaultEntry = Tbl_TableDefaultReadEntry(table, 0); |
---|
137 | if (defaultEntry == NIL(Tbl_Entry_t)) { |
---|
138 | cumulative = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
139 | } else if (Tbl_EntryIsEqual(defaultEntry)) { |
---|
140 | cumulative = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
141 | Tbl_EntrySetValue(cumulative, 0, Var_VariableReadNumValues(invar) - 1); |
---|
142 | } else { |
---|
143 | if (Tbl_EntryReadNumValues(defaultEntry) != 1) return FALSE; |
---|
144 | cumulative = Tbl_EntryDup(defaultEntry); |
---|
145 | } |
---|
146 | Tbl_TableForEachOutputEntry(table, rowNum, colNum, outputEntry) { |
---|
147 | Tbl_Entry_t *tmpEntry; |
---|
148 | assert(colNum == 0); |
---|
149 | inputEntry = Tbl_TableReadEntry(table, rowNum, 0, 0); |
---|
150 | assert(!Tbl_EntryIsEqual(inputEntry)); |
---|
151 | if (!Tbl_EntryIsEqual(outputEntry)) { |
---|
152 | if (Tbl_EntryReadNumValues(outputEntry) != 1 || |
---|
153 | !Tbl_EntryTestEqualEntry(outputEntry,inputEntry)) { |
---|
154 | Tbl_EntryFree(cumulative); |
---|
155 | return FALSE; |
---|
156 | } |
---|
157 | } |
---|
158 | tmpEntry = Tbl_EntryMerge(cumulative, inputEntry); |
---|
159 | Tbl_EntryFree(cumulative); |
---|
160 | cumulative = tmpEntry; |
---|
161 | } |
---|
162 | result = Tbl_EntryReadNumValues(cumulative) == |
---|
163 | Var_VariableReadNumValues(invar); |
---|
164 | Tbl_EntryFree(cumulative); |
---|
165 | return result; |
---|
166 | |
---|
167 | #if 0 |
---|
168 | |
---|
169 | /* Use the MVF sledgehammer. Only proceed if an mdd manager was |
---|
170 | * passed as argument. |
---|
171 | */ |
---|
172 | |
---|
173 | if (mddMgr == NIL(mdd_manager)) return FALSE; |
---|
174 | |
---|
175 | /* Create MDD variables for the table inputs. */ |
---|
176 | mdd_restart(mddMgr); |
---|
177 | mvarValues = array_alloc(int, 1); |
---|
178 | array_insert_last(int, mvarValues, Var_VariableReadNumValues(invar)); |
---|
179 | mdd_create_variables(mddMgr, mvarValues, NIL(array_t), NIL(array_t)); |
---|
180 | array_free(mvarValues); |
---|
181 | |
---|
182 | /* |
---|
183 | * Construct an MVF for each table input. The MVF for column i is the MVF |
---|
184 | * for MDD variable i. |
---|
185 | */ |
---|
186 | inMvf = Mvf_FunctionCreateFromVariable(mddMgr, 0); |
---|
187 | inMvfArray = array_alloc(Mvf_Function_t *, 1); |
---|
188 | array_insert_last(Mvf_Function_t *, inMvfArray, inMvf); |
---|
189 | |
---|
190 | outMvf = Tbl_TableBuildMvfFromFanins(table, 0, inMvfArray, mddMgr); |
---|
191 | |
---|
192 | /* Build a reference identity. This can be sped up quite a bit, but |
---|
193 | we are practicing using the tbl package. */ |
---|
194 | ident = Tbl_TableAlloc(); |
---|
195 | colNum = Tbl_TableAddColumn(ident,invar,0); |
---|
196 | assert(colNum == 1); |
---|
197 | colNum = Tbl_TableAddColumn(ident,outvar,1); |
---|
198 | assert(colNum == 1); |
---|
199 | rowNum = Tbl_TableAddRow(ident); |
---|
200 | assert(rowNum == 0); |
---|
201 | inputEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
202 | Tbl_EntrySetValue(inputEntry, 0, Var_VariableReadNumValues(invar)-1); |
---|
203 | Tbl_TableSetEntry(ident,inputEntry, 0, 0, 0); |
---|
204 | outputEntry = Tbl_EntryAlloc(Tbl_EntryEqual_c); |
---|
205 | Tbl_EntrySetEqual(outputEntry, 0); |
---|
206 | Tbl_TableSetEntry(ident,outputEntry, 0, 0, 1); |
---|
207 | |
---|
208 | identMvf = Tbl_TableBuildMvfFromFanins(ident, 0, inMvfArray, mddMgr); |
---|
209 | Mvf_FunctionArrayFree(inMvfArray); |
---|
210 | Tbl_TableFree(ident); |
---|
211 | result = Mvf_FunctionTestIsEqualToFunction(outMvf, identMvf); |
---|
212 | Mvf_FunctionFree(outMvf); |
---|
213 | Mvf_FunctionFree(identMvf); |
---|
214 | return result; |
---|
215 | #endif |
---|
216 | |
---|
217 | } /* Tbl_TableIsIdentity */ |
---|
218 | |
---|
219 | |
---|
220 | /**Function******************************************************************** |
---|
221 | |
---|
222 | Synopsis[Check whether a table describes an inverter.] |
---|
223 | |
---|
224 | Description [This function checks whether a table describes an |
---|
225 | inverter. An inverter table has exactly one binary input and one |
---|
226 | binary output variable, which takes the opposite value as the |
---|
227 | input.] |
---|
228 | |
---|
229 | SideEffects [] |
---|
230 | |
---|
231 | SeeAlso [] |
---|
232 | |
---|
233 | ******************************************************************************/ |
---|
234 | boolean |
---|
235 | Tbl_TableIsInverter( |
---|
236 | Tbl_Table_t *table |
---|
237 | ) |
---|
238 | { |
---|
239 | Var_Variable_t *invar = NIL(Var_Variable_t), *outvar = NIL(Var_Variable_t); |
---|
240 | Var_Variable_t *var; |
---|
241 | int colNum, rowNum; |
---|
242 | Tbl_Entry_t *inputEntry, *outputEntry, *defaultEntry, *cumulative; |
---|
243 | boolean result; |
---|
244 | |
---|
245 | if (Tbl_TableReadNumInputs(table) != 1) return FALSE; |
---|
246 | if (Tbl_TableReadNumOutputs(table) != 1) return FALSE; |
---|
247 | |
---|
248 | Tbl_TableForEachInputVar(table,colNum,var) { |
---|
249 | invar = var; |
---|
250 | } |
---|
251 | if (Var_VariableReadNumValues(invar) != 2 || |
---|
252 | Var_VariableTestIsSymbolic(invar)) return FALSE; |
---|
253 | |
---|
254 | Tbl_TableForEachOutputVar(table,colNum,var) { |
---|
255 | outvar = var; |
---|
256 | } |
---|
257 | if (Var_VariableReadNumValues(outvar) != 2 || |
---|
258 | Var_VariableTestIsSymbolic(outvar)) return FALSE; |
---|
259 | |
---|
260 | defaultEntry = Tbl_TableDefaultReadEntry(table, 0); |
---|
261 | if (defaultEntry == NIL(Tbl_Entry_t)) { |
---|
262 | cumulative = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
263 | } else if (Tbl_EntryIsEqual(defaultEntry)) { |
---|
264 | return FALSE; |
---|
265 | } else { |
---|
266 | if (Tbl_EntryReadNumValues(defaultEntry) != 1) |
---|
267 | return FALSE; |
---|
268 | cumulative = Tbl_EntryDup(defaultEntry); |
---|
269 | Tbl_EntryComplement(cumulative, 0, 1); |
---|
270 | } |
---|
271 | Tbl_TableForEachOutputEntry(table, rowNum, colNum, outputEntry) { |
---|
272 | Tbl_Entry_t *tmpEntry; |
---|
273 | assert(colNum == 0); |
---|
274 | if (Tbl_EntryIsEqual(outputEntry)) { |
---|
275 | Tbl_EntryFree(cumulative); |
---|
276 | return FALSE; |
---|
277 | } |
---|
278 | |
---|
279 | inputEntry = Tbl_TableReadEntry(table, rowNum, 0, 0); |
---|
280 | assert(!Tbl_EntryIsEqual(inputEntry)); |
---|
281 | if (Tbl_EntryReadNumValues(outputEntry) != 1 || |
---|
282 | Tbl_EntryTestIntersectEntry(outputEntry,inputEntry)) { |
---|
283 | Tbl_EntryFree(cumulative); |
---|
284 | return FALSE; |
---|
285 | } |
---|
286 | tmpEntry = Tbl_EntryMerge(cumulative, inputEntry); |
---|
287 | Tbl_EntryFree(cumulative); |
---|
288 | cumulative = tmpEntry; |
---|
289 | } |
---|
290 | result = Tbl_EntryReadNumValues(cumulative) == 2; |
---|
291 | Tbl_EntryFree(cumulative); |
---|
292 | return result; |
---|
293 | |
---|
294 | } /* Tbl_TableIsInverter */ |
---|