1 /**CFile***********************************************************************
7 Synopsis [Computation of signatures.]
9 Description [External procedures included in this module:
11 <li> Cudd_CofMinterm();
13 Static procedures included in this module:
15 <li> ddCofMintermAux()
19 Author [Fabio Somenzi]
21 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
25 Redistribution and use in source and binary forms, with or without
26 modification, are permitted provided that the following conditions
29 Redistributions of source code must retain the above copyright
30 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
53 ******************************************************************************/
59 /*---------------------------------------------------------------------------*/
60 /* Constant declarations */
61 /*---------------------------------------------------------------------------*/
64 /*---------------------------------------------------------------------------*/
65 /* Stucture declarations */
66 /*---------------------------------------------------------------------------*/
69 /*---------------------------------------------------------------------------*/
70 /* Type declarations */
71 /*---------------------------------------------------------------------------*/
74 /*---------------------------------------------------------------------------*/
75 /* Variable declarations */
76 /*---------------------------------------------------------------------------*/
79 static char rcsid
[] DD_UNUSED
= "$Id: cuddSign.c,v 1.22 2009/02/20 02:14:58 fabio Exp $";
85 static int num_calls
; /* should equal 2n-1 (n is the # of nodes) */
90 /*---------------------------------------------------------------------------*/
91 /* Macro declarations */
92 /*---------------------------------------------------------------------------*/
95 /**AutomaticStart*************************************************************/
97 /*---------------------------------------------------------------------------*/
98 /* Static function prototypes */
99 /*---------------------------------------------------------------------------*/
101 static double * ddCofMintermAux (DdManager
*dd
, DdNode
*node
, st_table
*table
);
103 /**AutomaticEnd***************************************************************/
106 /*---------------------------------------------------------------------------*/
107 /* Definition of exported functions */
108 /*---------------------------------------------------------------------------*/
110 /**Function********************************************************************
112 Synopsis [Computes the fraction of minterms in the on-set of all the
113 positive cofactors of a BDD or ADD.]
115 Description [Computes the fraction of minterms in the on-set of all
116 the positive cofactors of DD. Returns the pointer to an array of
117 doubles if successful; NULL otherwise. The array has as many
118 positions as there are BDD variables in the manager plus one. The
119 last position of the array contains the fraction of the minterms in
120 the ON-set of the function represented by the BDD or ADD. The other
121 positions of the array hold the variable signatures.]
125 ******************************************************************************/
133 double *result
= NULL
;
138 startTime
= util_cpu_time();
140 table_mem
= sizeof(st_table
);
143 table
= st_init_table(st_ptrcmp
, st_ptrhash
);
145 (void) fprintf(dd
->err
,
146 "out-of-memory, couldn't measure DD cofactors.\n");
147 dd
->errorCode
= CUDD_MEMORY_OUT
;
151 values
= ddCofMintermAux(dd
, node
, table
);
152 if (values
!= NULL
) {
153 result
= ALLOC(double,size
+ 1);
154 if (result
!= NULL
) {
156 table_mem
+= (size
+ 1) * sizeof(double);
158 if (Cudd_IsConstant(node
))
161 firstLevel
= cuddI(dd
,Cudd_Regular(node
)->index
);
162 for (i
= 0; i
< size
; i
++) {
163 if (i
>= cuddI(dd
,Cudd_Regular(node
)->index
)) {
164 result
[dd
->invperm
[i
]] = values
[i
- firstLevel
];
166 result
[dd
->invperm
[i
]] = values
[size
- firstLevel
];
169 result
[size
] = values
[size
- firstLevel
];
171 dd
->errorCode
= CUDD_MEMORY_OUT
;
176 table_mem
+= table
->num_bins
* sizeof(st_table_entry
*);
178 if (Cudd_Regular(node
)->ref
== 1) FREE(values
);
179 st_foreach(table
, cuddStCountfree
, NULL
);
180 st_free_table(table
);
182 (void) fprintf(dd
->out
,"Number of calls: %d\tTable memory: %d bytes\n",
183 num_calls
, table_mem
);
184 (void) fprintf(dd
->out
,"Time to compute measures: %s\n",
185 util_print_time(util_cpu_time() - startTime
));
187 if (result
== NULL
) {
188 (void) fprintf(dd
->out
,
189 "out-of-memory, couldn't measure DD cofactors.\n");
190 dd
->errorCode
= CUDD_MEMORY_OUT
;
194 } /* end of Cudd_CofMinterm */
197 /*---------------------------------------------------------------------------*/
198 /* Definition of internal functions */
199 /*---------------------------------------------------------------------------*/
202 /*---------------------------------------------------------------------------*/
203 /* Definition of static functions */
204 /*---------------------------------------------------------------------------*/
207 /**Function********************************************************************
209 Synopsis [Recursive Step for Cudd_CofMinterm function.]
211 Description [Traverses the DD node and computes the fraction of
212 minterms in the on-set of all positive cofactors simultaneously.
213 It allocates an array with two more entries than there are
214 variables below the one labeling the node. One extra entry (the
215 first in the array) is for the variable labeling the node. The other
216 entry (the last one in the array) holds the fraction of minterms of
217 the function rooted at node. Each other entry holds the value for
218 one cofactor. The array is put in a symbol table, to avoid repeated
219 computation, and its address is returned by the procedure, for use
220 by the caller. Returns a pointer to the array of cofactor measures.]
226 ******************************************************************************/
233 DdNode
*N
; /* regular version of node */
236 double *valuesT
, *valuesE
;
238 int localSize
, localSizeT
, localSizeE
;
246 if (st_lookup(table
, node
, &values
)) {
250 N
= Cudd_Regular(node
);
251 if (cuddIsConstant(N
)) {
254 localSize
= size
- cuddI(dd
,N
->index
) + 1;
256 values
= ALLOC(double, localSize
);
257 if (values
== NULL
) {
258 dd
->errorCode
= CUDD_MEMORY_OUT
;
262 if (cuddIsConstant(N
)) {
263 if (node
== DD_ZERO(dd
) || node
== Cudd_Not(DD_ONE(dd
))) {
269 Nv
= Cudd_NotCond(cuddT(N
),N
!=node
);
270 Nnv
= Cudd_NotCond(cuddE(N
),N
!=node
);
272 valuesT
= ddCofMintermAux(dd
, Nv
, table
);
273 if (valuesT
== NULL
) return(NULL
);
274 valuesE
= ddCofMintermAux(dd
, Nnv
, table
);
275 if (valuesE
== NULL
) return(NULL
);
277 if (Cudd_IsConstant(Nv
)) {
280 localSizeT
= size
- cuddI(dd
,Cudd_Regular(Nv
)->index
) + 1;
282 if (Cudd_IsConstant(Nnv
)) {
285 localSizeE
= size
- cuddI(dd
,Cudd_Regular(Nnv
)->index
) + 1;
287 values
[0] = valuesT
[localSizeT
- 1];
288 for (i
= 1; i
< localSize
; i
++) {
289 if (i
>= cuddI(dd
,Cudd_Regular(Nv
)->index
) - cuddI(dd
,N
->index
)) {
290 vT
= valuesT
[i
- cuddI(dd
,Cudd_Regular(Nv
)->index
) +
293 vT
= valuesT
[localSizeT
- 1];
295 if (i
>= cuddI(dd
,Cudd_Regular(Nnv
)->index
) - cuddI(dd
,N
->index
)) {
296 vE
= valuesE
[i
- cuddI(dd
,Cudd_Regular(Nnv
)->index
) +
299 vE
= valuesE
[localSizeE
- 1];
301 values
[i
] = (vT
+ vE
) / 2.0;
303 if (Cudd_Regular(Nv
)->ref
== 1) FREE(valuesT
);
304 if (Cudd_Regular(Nnv
)->ref
== 1) FREE(valuesE
);
308 if (st_add_direct(table
, (char *) node
, (char *) values
) == ST_OUT_OF_MEM
) {
313 table_mem
+= localSize
* sizeof(double) + sizeof(st_table_entry
);
318 } /* end of ddCofMintermAux */