source: vis_dev/glu-2.3/src/cuBdd/cuddZddCount.c @ 84

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

library glu 2.3
File size: 10.0 KB
RevLine 
[13]1/**CFile***********************************************************************
2
3  FileName    [cuddZddCount.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Procedures to count the number of minterms of a ZDD.]
8
9  Description [External procedures included in this module:
10                    <ul>
11                    <li> Cudd_zddCount();
12                    <li> Cudd_zddCountDouble();
13                    </ul>
14               Internal procedures included in this module:
15                    <ul>
16                    </ul>
17               Static procedures included in this module:
18                    <ul>
19                    <li> cuddZddCountStep();
20                    <li> cuddZddCountDoubleStep();
21                    <li> st_zdd_count_dbl_free()
22                    <li> st_zdd_countfree()
23                    </ul>
24              ]
25
26  SeeAlso     []
27
28  Author      [Hyong-Kyoon Shin, In-Ho Moon]
29
30  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
31
32  All rights reserved.
33
34  Redistribution and use in source and binary forms, with or without
35  modification, are permitted provided that the following conditions
36  are met:
37
38  Redistributions of source code must retain the above copyright
39  notice, this list of conditions and the following disclaimer.
40
41  Redistributions in binary form must reproduce the above copyright
42  notice, this list of conditions and the following disclaimer in the
43  documentation and/or other materials provided with the distribution.
44
45  Neither the name of the University of Colorado nor the names of its
46  contributors may be used to endorse or promote products derived from
47  this software without specific prior written permission.
48
49  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60  POSSIBILITY OF SUCH DAMAGE.]
61
62******************************************************************************/
63
64#include "util.h"
65#include "cuddInt.h"
66
67/*---------------------------------------------------------------------------*/
68/* Constant declarations                                                     */
69/*---------------------------------------------------------------------------*/
70
71
72/*---------------------------------------------------------------------------*/
73/* Stucture declarations                                                     */
74/*---------------------------------------------------------------------------*/
75
76
77/*---------------------------------------------------------------------------*/
78/* Type declarations                                                         */
79/*---------------------------------------------------------------------------*/
80
81
82/*---------------------------------------------------------------------------*/
83/* Variable declarations                                                     */
84/*---------------------------------------------------------------------------*/
85
86#ifndef lint
87static char rcsid[] DD_UNUSED = "$Id: cuddZddCount.c,v 1.14 2004/08/13 18:04:53 fabio Exp $";
88#endif
89
90/*---------------------------------------------------------------------------*/
91/* Macro declarations                                                        */
92/*---------------------------------------------------------------------------*/
93
94#ifdef __cplusplus
95extern "C" {
96#endif
97
98/**AutomaticStart*************************************************************/
99
100/*---------------------------------------------------------------------------*/
101/* Static function prototypes                                                */
102/*---------------------------------------------------------------------------*/
103
104static int cuddZddCountStep (DdNode *P, st_table *table, DdNode *base, DdNode *empty);
105static double cuddZddCountDoubleStep (DdNode *P, st_table *table, DdNode *base, DdNode *empty);
106static enum st_retval st_zdd_countfree (char *key, char *value, char *arg);
107static enum st_retval st_zdd_count_dbl_free (char *key, char *value, char *arg);
108
109/**AutomaticEnd***************************************************************/
110
111#ifdef __cplusplus
112}
113#endif
114
115/*---------------------------------------------------------------------------*/
116/* Definition of exported functions                                          */
117/*---------------------------------------------------------------------------*/
118
119
120/**Function********************************************************************
121
122  Synopsis [Counts the number of minterms in a ZDD.]
123
124  Description [Returns an integer representing the number of minterms
125  in a ZDD.]
126
127  SideEffects [None]
128
129  SeeAlso     [Cudd_zddCountDouble]
130
131******************************************************************************/
132int
133Cudd_zddCount(
134  DdManager * zdd,
135  DdNode * P)
136{
137    st_table    *table;
138    int         res;
139    DdNode      *base, *empty;
140
141    base  = DD_ONE(zdd);
142    empty = DD_ZERO(zdd);
143    table = st_init_table(st_ptrcmp, st_ptrhash);
144    if (table == NULL) return(CUDD_OUT_OF_MEM);
145    res = cuddZddCountStep(P, table, base, empty);
146    if (res == CUDD_OUT_OF_MEM) {
147        zdd->errorCode = CUDD_MEMORY_OUT;
148    }
149    st_foreach(table, st_zdd_countfree, NIL(char));
150    st_free_table(table);
151
152    return(res);
153
154} /* end of Cudd_zddCount */
155
156
157/**Function********************************************************************
158
159  Synopsis [Counts the number of minterms of a ZDD.]
160
161  Description [Counts the number of minterms of a ZDD. The result is
162  returned as a double. If the procedure runs out of memory, it
163  returns (double) CUDD_OUT_OF_MEM. This procedure is used in
164  Cudd_zddCountMinterm.]
165
166  SideEffects [None]
167
168  SeeAlso     [Cudd_zddCountMinterm Cudd_zddCount]
169
170******************************************************************************/
171double
172Cudd_zddCountDouble(
173  DdManager * zdd,
174  DdNode * P)
175{
176    st_table    *table;
177    double      res;
178    DdNode      *base, *empty;
179
180    base  = DD_ONE(zdd);
181    empty = DD_ZERO(zdd);
182    table = st_init_table(st_ptrcmp, st_ptrhash);
183    if (table == NULL) return((double)CUDD_OUT_OF_MEM);
184    res = cuddZddCountDoubleStep(P, table, base, empty);
185    if (res == (double)CUDD_OUT_OF_MEM) {
186        zdd->errorCode = CUDD_MEMORY_OUT;
187    }
188    st_foreach(table, st_zdd_count_dbl_free, NIL(char));
189    st_free_table(table);
190
191    return(res);
192
193} /* end of Cudd_zddCountDouble */
194
195
196/*---------------------------------------------------------------------------*/
197/* Definition of internal functions                                          */
198/*---------------------------------------------------------------------------*/
199
200
201/*---------------------------------------------------------------------------*/
202/* Definition of static functions                                            */
203/*---------------------------------------------------------------------------*/
204
205
206/**Function********************************************************************
207
208  Synopsis [Performs the recursive step of Cudd_zddCount.]
209
210  Description []
211
212  SideEffects [None]
213
214  SeeAlso     []
215
216******************************************************************************/
217static int
218cuddZddCountStep(
219  DdNode * P,
220  st_table * table,
221  DdNode * base,
222  DdNode * empty)
223{
224    int         res;
225    int         *dummy;
226
227    if (P == empty)
228        return(0);
229    if (P == base)
230        return(1);
231
232    /* Check cache. */
233    if (st_lookup(table, P, &dummy)) {
234        res = *dummy;
235        return(res);
236    }
237
238    res = cuddZddCountStep(cuddE(P), table, base, empty) +
239        cuddZddCountStep(cuddT(P), table, base, empty);
240
241    dummy = ALLOC(int, 1);
242    if (dummy == NULL) {
243        return(CUDD_OUT_OF_MEM);
244    }
245    *dummy = res;
246    if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
247        FREE(dummy);
248        return(CUDD_OUT_OF_MEM);
249    }
250
251    return(res);
252
253} /* end of cuddZddCountStep */
254
255
256/**Function********************************************************************
257
258  Synopsis [Performs the recursive step of Cudd_zddCountDouble.]
259
260  Description []
261
262  SideEffects [None]
263
264  SeeAlso     []
265
266******************************************************************************/
267static double
268cuddZddCountDoubleStep(
269  DdNode * P,
270  st_table * table,
271  DdNode * base,
272  DdNode * empty)
273{
274    double      res;
275    double      *dummy;
276
277    if (P == empty)
278        return((double)0.0);
279    if (P == base)
280        return((double)1.0);
281
282    /* Check cache */
283    if (st_lookup(table, P, &dummy)) {
284        res = *dummy;
285        return(res);
286    }
287
288    res = cuddZddCountDoubleStep(cuddE(P), table, base, empty) +
289        cuddZddCountDoubleStep(cuddT(P), table, base, empty);
290
291    dummy = ALLOC(double, 1);
292    if (dummy == NULL) {
293        return((double)CUDD_OUT_OF_MEM);
294    }
295    *dummy = res;
296    if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
297        FREE(dummy);
298        return((double)CUDD_OUT_OF_MEM);
299    }
300
301    return(res);
302
303} /* end of cuddZddCountDoubleStep */
304
305
306/**Function********************************************************************
307
308  Synopsis [Frees the memory associated with the computed table of
309  Cudd_zddCount.]
310
311  Description []
312
313  SideEffects [None]
314
315  SeeAlso     []
316
317******************************************************************************/
318static enum st_retval
319st_zdd_countfree(
320  char * key,
321  char * value,
322  char * arg)
323{
324    int *d;
325
326    d = (int *)value;
327    FREE(d);
328    return(ST_CONTINUE);
329
330} /* end of st_zdd_countfree */
331
332
333/**Function********************************************************************
334
335  Synopsis [Frees the memory associated with the computed table of
336  Cudd_zddCountDouble.]
337
338  Description []
339
340  SideEffects [None]
341
342  SeeAlso     []
343
344******************************************************************************/
345static enum st_retval
346st_zdd_count_dbl_free(
347  char * key,
348  char * value,
349  char * arg)
350{
351    double      *d;
352
353    d = (double *)value;
354    FREE(d);
355    return(ST_CONTINUE);
356
357} /* end of st_zdd_count_dbl_free */
Note: See TracBrowser for help on using the repository browser.