1 /**CFile***********************************************************************
2
3 FileName [cuddSign.c]
4
5 PackageName [cudd]
6
7 Synopsis [Computation of signatures.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_CofMinterm();
12 </ul>
13 Static procedures included in this module:
14 <ul>
15 <li> ddCofMintermAux()
16 </ul>
17 ]
18
19 Author [Fabio Somenzi]
20
21 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
22
23 All rights reserved.
24
25 Redistribution and use in source and binary forms, with or without
26 modification, are permitted provided that the following conditions
27 are met:
28
29 Redistributions of source code must retain the above copyright
30 notice, this list of conditions and the following disclaimer.
31
32 Redistributions in binary form must reproduce the above copyright
33 notice, this list of conditions and the following disclaimer in the
34 documentation and/or other materials provided with the distribution.
35
36 Neither the name of the University of Colorado nor the names of its
37 contributors may be used to endorse or promote products derived from
38 this software without specific prior written permission.
39
40 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
41 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
42 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
43 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
44 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
45 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
46 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
47 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
48 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
49 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
50 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
51 POSSIBILITY OF SUCH DAMAGE.]
52
53 ******************************************************************************/
54
55 #include "misc/util/util_hack.h"
56 #include "cuddInt.h"
57
58 ABC_NAMESPACE_IMPL_START
59
60
61
62
63 /*---------------------------------------------------------------------------*/
64 /* Constant declarations */
65 /*---------------------------------------------------------------------------*/
66
67
68 /*---------------------------------------------------------------------------*/
69 /* Stucture declarations */
70 /*---------------------------------------------------------------------------*/
71
72
73 /*---------------------------------------------------------------------------*/
74 /* Type declarations */
75 /*---------------------------------------------------------------------------*/
76
77
78 /*---------------------------------------------------------------------------*/
79 /* Variable declarations */
80 /*---------------------------------------------------------------------------*/
81
82 #ifndef lint
83 static char rcsid[] DD_UNUSED = "$Id: cuddSign.c,v 1.22 2009/02/20 02:14:58 fabio Exp $";
84 #endif
85
86 static int size;
87
88 #ifdef DD_STATS
89 static int num_calls; /* should equal 2n-1 (n is the # of nodes) */
90 static int table_mem;
91 #endif
92
93
94 /*---------------------------------------------------------------------------*/
95 /* Macro declarations */
96 /*---------------------------------------------------------------------------*/
97
98
99 /**AutomaticStart*************************************************************/
100
101 /*---------------------------------------------------------------------------*/
102 /* Static function prototypes */
103 /*---------------------------------------------------------------------------*/
104
105 static double * ddCofMintermAux (DdManager *dd, DdNode *node, st__table *table);
106
107 /**AutomaticEnd***************************************************************/
108
109
110 /*---------------------------------------------------------------------------*/
111 /* Definition of exported functions */
112 /*---------------------------------------------------------------------------*/
113
114 /**Function********************************************************************
115
116 Synopsis [Computes the fraction of minterms in the on-set of all the
117 positive cofactors of a BDD or ADD.]
118
119 Description [Computes the fraction of minterms in the on-set of all
120 the positive cofactors of DD. Returns the pointer to an array of
121 doubles if successful; NULL otherwise. The array has as many
122 positions as there are BDD variables in the manager plus one. The
123 last position of the array contains the fraction of the minterms in
124 the ON-set of the function represented by the BDD or ADD. The other
125 positions of the array hold the variable signatures.]
126
127 SideEffects [None]
128
129 ******************************************************************************/
130 double *
Cudd_CofMinterm(DdManager * dd,DdNode * node)131 Cudd_CofMinterm(
132 DdManager * dd,
133 DdNode * node)
134 {
135 st__table *table;
136 double *values;
137 double *result = NULL;
138 int i, firstLevel;
139
140 #ifdef DD_STATS
141 long startTime;
142 startTime = util_cpu_time();
143 num_calls = 0;
144 table_mem = sizeof( st__table);
145 #endif
146
147 table = st__init_table( st__ptrcmp, st__ptrhash);
148 if (table == NULL) {
149 (void) fprintf(dd->err,
150 "out-of-memory, couldn't measure DD cofactors.\n");
151 dd->errorCode = CUDD_MEMORY_OUT;
152 return(NULL);
153 }
154 size = dd->size;
155 values = ddCofMintermAux(dd, node, table);
156 if (values != NULL) {
157 result = ABC_ALLOC(double,size + 1);
158 if (result != NULL) {
159 #ifdef DD_STATS
160 table_mem += (size + 1) * sizeof(double);
161 #endif
162 if (Cudd_IsConstant(node))
163 firstLevel = 1;
164 else
165 firstLevel = cuddI(dd,Cudd_Regular(node)->index);
166 for (i = 0; i < size; i++) {
167 if (i >= cuddI(dd,Cudd_Regular(node)->index)) {
168 result[dd->invperm[i]] = values[i - firstLevel];
169 } else {
170 result[dd->invperm[i]] = values[size - firstLevel];
171 }
172 }
173 result[size] = values[size - firstLevel];
174 } else {
175 dd->errorCode = CUDD_MEMORY_OUT;
176 }
177 }
178
179 #ifdef DD_STATS
180 table_mem += table->num_bins * sizeof( st__table_entry *);
181 #endif
182 if (Cudd_Regular(node)->ref == 1) ABC_FREE(values);
183 st__foreach(table, cuddStCountfree, NULL);
184 st__free_table(table);
185 #ifdef DD_STATS
186 (void) fprintf(dd->out,"Number of calls: %d\tTable memory: %d bytes\n",
187 num_calls, table_mem);
188 (void) fprintf(dd->out,"Time to compute measures: %s\n",
189 util_print_time(util_cpu_time() - startTime));
190 #endif
191 if (result == NULL) {
192 (void) fprintf(dd->out,
193 "out-of-memory, couldn't measure DD cofactors.\n");
194 dd->errorCode = CUDD_MEMORY_OUT;
195 }
196 return(result);
197
198 } /* end of Cudd_CofMinterm */
199
200
201 /*---------------------------------------------------------------------------*/
202 /* Definition of internal functions */
203 /*---------------------------------------------------------------------------*/
204
205
206 /*---------------------------------------------------------------------------*/
207 /* Definition of static functions */
208 /*---------------------------------------------------------------------------*/
209
210
211 /**Function********************************************************************
212
213 Synopsis [Recursive Step for Cudd_CofMinterm function.]
214
215 Description [Traverses the DD node and computes the fraction of
216 minterms in the on-set of all positive cofactors simultaneously.
217 It allocates an array with two more entries than there are
218 variables below the one labeling the node. One extra entry (the
219 first in the array) is for the variable labeling the node. The other
220 entry (the last one in the array) holds the fraction of minterms of
221 the function rooted at node. Each other entry holds the value for
222 one cofactor. The array is put in a symbol table, to avoid repeated
223 computation, and its address is returned by the procedure, for use
224 by the caller. Returns a pointer to the array of cofactor measures.]
225
226 SideEffects [None]
227
228 SeeAlso []
229
230 ******************************************************************************/
231 static double *
ddCofMintermAux(DdManager * dd,DdNode * node,st__table * table)232 ddCofMintermAux(
233 DdManager * dd,
234 DdNode * node,
235 st__table * table)
236 {
237 DdNode *N; /* regular version of node */
238 DdNode *Nv, *Nnv;
239 double *values;
240 double *valuesT, *valuesE;
241 int i;
242 int localSize, localSizeT, localSizeE;
243 double vT, vE;
244
245 statLine(dd);
246 #ifdef DD_STATS
247 num_calls++;
248 #endif
249
250 if ( st__lookup(table, (const char *)node, (char **)&values)) {
251 return(values);
252 }
253
254 N = Cudd_Regular(node);
255 if (cuddIsConstant(N)) {
256 localSize = 1;
257 } else {
258 localSize = size - cuddI(dd,N->index) + 1;
259 }
260 values = ABC_ALLOC(double, localSize);
261 if (values == NULL) {
262 dd->errorCode = CUDD_MEMORY_OUT;
263 return(NULL);
264 }
265
266 if (cuddIsConstant(N)) {
267 if (node == DD_ZERO(dd) || node == Cudd_Not(DD_ONE(dd))) {
268 values[0] = 0.0;
269 } else {
270 values[0] = 1.0;
271 }
272 } else {
273 Nv = Cudd_NotCond(cuddT(N),N!=node);
274 Nnv = Cudd_NotCond(cuddE(N),N!=node);
275
276 valuesT = ddCofMintermAux(dd, Nv, table);
277 if (valuesT == NULL) return(NULL);
278 valuesE = ddCofMintermAux(dd, Nnv, table);
279 if (valuesE == NULL) return(NULL);
280
281 if (Cudd_IsConstant(Nv)) {
282 localSizeT = 1;
283 } else {
284 localSizeT = size - cuddI(dd,Cudd_Regular(Nv)->index) + 1;
285 }
286 if (Cudd_IsConstant(Nnv)) {
287 localSizeE = 1;
288 } else {
289 localSizeE = size - cuddI(dd,Cudd_Regular(Nnv)->index) + 1;
290 }
291 values[0] = valuesT[localSizeT - 1];
292 for (i = 1; i < localSize; i++) {
293 if (i >= cuddI(dd,Cudd_Regular(Nv)->index) - cuddI(dd,N->index)) {
294 vT = valuesT[i - cuddI(dd,Cudd_Regular(Nv)->index) +
295 cuddI(dd,N->index)];
296 } else {
297 vT = valuesT[localSizeT - 1];
298 }
299 if (i >= cuddI(dd,Cudd_Regular(Nnv)->index) - cuddI(dd,N->index)) {
300 vE = valuesE[i - cuddI(dd,Cudd_Regular(Nnv)->index) +
301 cuddI(dd,N->index)];
302 } else {
303 vE = valuesE[localSizeE - 1];
304 }
305 values[i] = (vT + vE) / 2.0;
306 }
307 if (Cudd_Regular(Nv)->ref == 1) ABC_FREE(valuesT);
308 if (Cudd_Regular(Nnv)->ref == 1) ABC_FREE(valuesE);
309 }
310
311 if (N->ref > 1) {
312 if ( st__add_direct(table, (char *) node, (char *) values) == st__OUT_OF_MEM) {
313 ABC_FREE(values);
314 return(NULL);
315 }
316 #ifdef DD_STATS
317 table_mem += localSize * sizeof(double) + sizeof( st__table_entry);
318 #endif
319 }
320 return(values);
321
322 } /* end of ddCofMintermAux */
323
324
325 ABC_NAMESPACE_IMPL_END
326
327