source: vis_dev/glu-2.3/src/cuBdd/cuddSign.c @ 42

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

library glu 2.3
File size: 10.3 KB
Line 
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 "util.h"
56#include "cuddInt.h"
57
58
59/*---------------------------------------------------------------------------*/
60/* Constant declarations                                                     */
61/*---------------------------------------------------------------------------*/
62
63
64/*---------------------------------------------------------------------------*/
65/* Stucture declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68
69/*---------------------------------------------------------------------------*/
70/* Type declarations                                                         */
71/*---------------------------------------------------------------------------*/
72
73
74/*---------------------------------------------------------------------------*/
75/* Variable declarations                                                     */
76/*---------------------------------------------------------------------------*/
77
78#ifndef lint
79static char rcsid[] DD_UNUSED = "$Id: cuddSign.c,v 1.22 2009/02/20 02:14:58 fabio Exp $";
80#endif
81
82static int    size;
83
84#ifdef DD_STATS
85static int num_calls;   /* should equal 2n-1 (n is the # of nodes) */
86static int table_mem;
87#endif
88
89
90/*---------------------------------------------------------------------------*/
91/* Macro declarations                                                        */
92/*---------------------------------------------------------------------------*/
93
94
95/**AutomaticStart*************************************************************/
96
97/*---------------------------------------------------------------------------*/
98/* Static function prototypes                                                */
99/*---------------------------------------------------------------------------*/
100
101static double * ddCofMintermAux (DdManager *dd, DdNode *node, st_table *table);
102
103/**AutomaticEnd***************************************************************/
104
105
106/*---------------------------------------------------------------------------*/
107/* Definition of exported functions                                          */
108/*---------------------------------------------------------------------------*/
109
110/**Function********************************************************************
111
112  Synopsis [Computes the fraction of minterms in the on-set of all the
113  positive cofactors of a BDD or ADD.]
114
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.]
122
123  SideEffects [None]
124
125******************************************************************************/
126double *
127Cudd_CofMinterm(
128  DdManager * dd,
129  DdNode * node)
130{
131    st_table    *table;
132    double      *values;
133    double      *result = NULL;
134    int         i, firstLevel;
135
136#ifdef DD_STATS
137    long startTime;
138    startTime = util_cpu_time();
139    num_calls = 0;
140    table_mem = sizeof(st_table);
141#endif
142
143    table = st_init_table(st_ptrcmp, st_ptrhash);
144    if (table == NULL) {
145        (void) fprintf(dd->err,
146                       "out-of-memory, couldn't measure DD cofactors.\n");
147        dd->errorCode = CUDD_MEMORY_OUT;
148        return(NULL);
149    }
150    size = dd->size;
151    values = ddCofMintermAux(dd, node, table);
152    if (values != NULL) {
153        result = ALLOC(double,size + 1);
154        if (result != NULL) {
155#ifdef DD_STATS
156            table_mem += (size + 1) * sizeof(double);
157#endif
158            if (Cudd_IsConstant(node))
159                firstLevel = 1;
160            else
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];
165                } else {
166                    result[dd->invperm[i]] = values[size - firstLevel];
167                }
168            }
169            result[size] = values[size - firstLevel];
170        } else {
171            dd->errorCode = CUDD_MEMORY_OUT;
172        }
173    }
174
175#ifdef DD_STATS
176    table_mem += table->num_bins * sizeof(st_table_entry *);
177#endif
178    if (Cudd_Regular(node)->ref == 1) FREE(values);
179    st_foreach(table, cuddStCountfree, NULL);
180    st_free_table(table);
181#ifdef DD_STATS
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));
186#endif
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;
191    }
192    return(result);
193
194} /* end of Cudd_CofMinterm */
195
196
197/*---------------------------------------------------------------------------*/
198/* Definition of internal functions                                          */
199/*---------------------------------------------------------------------------*/
200
201
202/*---------------------------------------------------------------------------*/
203/* Definition of static functions                                            */
204/*---------------------------------------------------------------------------*/
205
206
207/**Function********************************************************************
208
209  Synopsis    [Recursive Step for Cudd_CofMinterm function.]
210
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.]
221
222  SideEffects [None]
223
224  SeeAlso     []
225
226******************************************************************************/
227static double *
228ddCofMintermAux(
229  DdManager * dd,
230  DdNode * node,
231  st_table * table)
232{
233    DdNode      *N;             /* regular version of node */
234    DdNode      *Nv, *Nnv;
235    double      *values;
236    double      *valuesT, *valuesE;
237    int         i;
238    int         localSize, localSizeT, localSizeE;
239    double      vT, vE;
240
241    statLine(dd);
242#ifdef DD_STATS
243    num_calls++;
244#endif
245
246    if (st_lookup(table, node, &values)) {
247        return(values);
248    }
249
250    N = Cudd_Regular(node);
251    if (cuddIsConstant(N)) {
252        localSize = 1;
253    } else {
254        localSize = size - cuddI(dd,N->index) + 1;
255    }
256    values = ALLOC(double, localSize);
257    if (values == NULL) {
258        dd->errorCode = CUDD_MEMORY_OUT;
259        return(NULL);
260    }
261
262    if (cuddIsConstant(N)) {
263        if (node == DD_ZERO(dd) || node == Cudd_Not(DD_ONE(dd))) {
264            values[0] = 0.0;
265        } else {
266            values[0] = 1.0;
267        }
268    } else {
269        Nv = Cudd_NotCond(cuddT(N),N!=node);
270        Nnv = Cudd_NotCond(cuddE(N),N!=node);
271
272        valuesT = ddCofMintermAux(dd, Nv, table);
273        if (valuesT == NULL) return(NULL);
274        valuesE = ddCofMintermAux(dd, Nnv, table);
275        if (valuesE == NULL) return(NULL);
276
277        if (Cudd_IsConstant(Nv)) {
278            localSizeT = 1;
279        } else {
280            localSizeT = size - cuddI(dd,Cudd_Regular(Nv)->index) + 1;
281        }
282        if (Cudd_IsConstant(Nnv)) {
283            localSizeE = 1;
284        } else {
285            localSizeE = size - cuddI(dd,Cudd_Regular(Nnv)->index) + 1;
286        }
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) +
291                            cuddI(dd,N->index)];
292            } else {
293                vT = valuesT[localSizeT - 1];
294            }
295            if (i >= cuddI(dd,Cudd_Regular(Nnv)->index) - cuddI(dd,N->index)) {
296                vE = valuesE[i - cuddI(dd,Cudd_Regular(Nnv)->index) +
297                            cuddI(dd,N->index)];
298            } else {
299                vE = valuesE[localSizeE - 1];
300            }
301            values[i] = (vT + vE) / 2.0;
302        }
303        if (Cudd_Regular(Nv)->ref == 1) FREE(valuesT);
304        if (Cudd_Regular(Nnv)->ref == 1) FREE(valuesE);
305    }
306
307    if (N->ref > 1) {
308        if (st_add_direct(table, (char *) node, (char *) values) == ST_OUT_OF_MEM) {
309            FREE(values);
310            return(NULL);
311        }
312#ifdef DD_STATS
313        table_mem += localSize * sizeof(double) + sizeof(st_table_entry);
314#endif
315    }
316    return(values);
317
318} /* end of ddCofMintermAux */
Note: See TracBrowser for help on using the repository browser.