source: vis_dev/glu-2.3/src/cuBdd/cuddZddMisc.c @ 66

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

library glu 2.3
File size: 8.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddZddMisc.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Miscellaneous utility functions for ZDDs.]
8
9  Description [External procedures included in this module:
10                    <ul>
11                    <li> Cudd_zddDagSize()
12                    <li> Cudd_zddCountMinterm()
13                    <li> Cudd_zddPrintSubtable()
14                    </ul>
15               Internal procedures included in this module:
16                    <ul>
17                    </ul>
18               Static procedures included in this module:
19                    <ul>
20                    <li> cuddZddDagInt()
21                    </ul>
22              ]
23
24  SeeAlso     []
25
26  Author      [Hyong-Kyoon Shin, In-Ho Moon]
27
28  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
29
30  All rights reserved.
31
32  Redistribution and use in source and binary forms, with or without
33  modification, are permitted provided that the following conditions
34  are met:
35
36  Redistributions of source code must retain the above copyright
37  notice, this list of conditions and the following disclaimer.
38
39  Redistributions in binary form must reproduce the above copyright
40  notice, this list of conditions and the following disclaimer in the
41  documentation and/or other materials provided with the distribution.
42
43  Neither the name of the University of Colorado nor the names of its
44  contributors may be used to endorse or promote products derived from
45  this software without specific prior written permission.
46
47  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
48  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
49  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
50  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
51  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
52  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
53  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
54  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
55  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
56  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
57  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
58  POSSIBILITY OF SUCH DAMAGE.]
59
60******************************************************************************/
61
62#include <math.h>
63#include "util.h"
64#include "cuddInt.h"
65
66/*---------------------------------------------------------------------------*/
67/* Constant declarations                                                     */
68/*---------------------------------------------------------------------------*/
69
70
71/*---------------------------------------------------------------------------*/
72/* Stucture declarations                                                     */
73/*---------------------------------------------------------------------------*/
74
75
76/*---------------------------------------------------------------------------*/
77/* Type declarations                                                         */
78/*---------------------------------------------------------------------------*/
79
80
81/*---------------------------------------------------------------------------*/
82/* Variable declarations                                                     */
83/*---------------------------------------------------------------------------*/
84
85#ifndef lint
86static char rcsid[] DD_UNUSED = "$Id: cuddZddMisc.c,v 1.17 2009/03/08 02:49:02 fabio Exp $";
87#endif
88
89/*---------------------------------------------------------------------------*/
90/* Macro declarations                                                        */
91/*---------------------------------------------------------------------------*/
92
93
94/**AutomaticStart*************************************************************/
95
96/*---------------------------------------------------------------------------*/
97/* Static function prototypes                                                */
98/*---------------------------------------------------------------------------*/
99
100static int cuddZddDagInt (DdNode *n, st_table *tab);
101
102/**AutomaticEnd***************************************************************/
103
104
105/*---------------------------------------------------------------------------*/
106/* Definition of exported functions                                          */
107/*---------------------------------------------------------------------------*/
108
109
110/**Function********************************************************************
111
112  Synopsis    [Counts the number of nodes in a ZDD.]
113
114  Description [Counts the number of nodes in a ZDD. This function
115  duplicates Cudd_DagSize and is only retained for compatibility.]
116
117  SideEffects [None]
118
119  SeeAlso     [Cudd_DagSize]
120
121******************************************************************************/
122int
123Cudd_zddDagSize(
124  DdNode * p_node)
125{
126
127    int         i;
128    st_table    *table;
129
130    table = st_init_table(st_ptrcmp, st_ptrhash);
131    i = cuddZddDagInt(p_node, table);
132    st_free_table(table);
133    return(i);
134
135} /* end of Cudd_zddDagSize */
136
137
138/**Function********************************************************************
139
140  Synopsis    [Counts the number of minterms of a ZDD.]
141
142  Description [Counts the number of minterms of the ZDD rooted at
143  <code>node</code>. This procedure takes a parameter
144  <code>path</code> that specifies how many variables are in the
145  support of the function. If the procedure runs out of memory, it
146  returns (double) CUDD_OUT_OF_MEM.]
147
148  SideEffects [None]
149
150  SeeAlso     [Cudd_zddCountDouble]
151
152******************************************************************************/
153double
154Cudd_zddCountMinterm(
155  DdManager * zdd,
156  DdNode * node,
157  int  path)
158{
159    double      dc_var, minterms;
160
161    dc_var = (double)((double)(zdd->sizeZ) - (double)path);
162    minterms = Cudd_zddCountDouble(zdd, node) / pow(2.0, dc_var);
163    return(minterms);
164
165} /* end of Cudd_zddCountMinterm */
166
167
168/**Function********************************************************************
169
170  Synopsis    [Prints the ZDD table.]
171
172  Description [Prints the ZDD table for debugging purposes.]
173
174  SideEffects [None]
175
176  SeeAlso     []
177
178******************************************************************************/
179void
180Cudd_zddPrintSubtable(
181  DdManager * table)
182{
183    int         i, j;
184    DdNode      *z1, *z1_next, *base;
185    DdSubtable  *ZSubTable;
186
187    base = table->one;
188    for (i = table->sizeZ - 1; i >= 0; i--) {
189        ZSubTable = &(table->subtableZ[i]);
190        printf("subtable[%d]:\n", i);
191        for (j = ZSubTable->slots - 1; j >= 0; j--) {
192            z1 = ZSubTable->nodelist[j];
193            while (z1 != NIL(DdNode)) {
194                (void) fprintf(table->out,
195#if SIZEOF_VOID_P == 8
196                    "ID = 0x%lx\tindex = %u\tr = %u\t",
197                    (ptruint) z1 / (ptruint) sizeof(DdNode),
198                    z1->index, z1->ref);
199#else
200                    "ID = 0x%x\tindex = %hu\tr = %hu\t",
201                    (ptruint) z1 / (ptruint) sizeof(DdNode),
202                    z1->index, z1->ref);
203#endif
204                z1_next = cuddT(z1);
205                if (Cudd_IsConstant(z1_next)) {
206                    (void) fprintf(table->out, "T = %d\t\t",
207                        (z1_next == base));
208                }
209                else {
210#if SIZEOF_VOID_P == 8
211                    (void) fprintf(table->out, "T = 0x%lx\t",
212                        (ptruint) z1_next / (ptruint) sizeof(DdNode));
213#else
214                    (void) fprintf(table->out, "T = 0x%x\t",
215                        (ptruint) z1_next / (ptruint) sizeof(DdNode));
216#endif
217                }
218                z1_next = cuddE(z1);
219                if (Cudd_IsConstant(z1_next)) {
220                    (void) fprintf(table->out, "E = %d\n",
221                        (z1_next == base));
222                }
223                else {
224#if SIZEOF_VOID_P == 8
225                    (void) fprintf(table->out, "E = 0x%lx\n",
226                        (ptruint) z1_next / (ptruint) sizeof(DdNode));
227#else
228                    (void) fprintf(table->out, "E = 0x%x\n",
229                        (ptruint) z1_next / (ptruint) sizeof(DdNode));
230#endif
231                }
232
233                z1_next = z1->next;
234                z1 = z1_next;
235            }
236        }
237    }
238    putchar('\n');
239
240} /* Cudd_zddPrintSubtable */
241
242
243/*---------------------------------------------------------------------------*/
244/* Definition of static functions                                            */
245/*---------------------------------------------------------------------------*/
246
247
248/**Function********************************************************************
249
250  Synopsis    [Performs the recursive step of Cudd_zddDagSize.]
251
252  Description [Performs the recursive step of Cudd_zddDagSize. Does
253  not check for out-of-memory conditions.]
254
255  SideEffects [None]
256
257  SeeAlso     []
258
259******************************************************************************/
260static int
261cuddZddDagInt(
262  DdNode * n,
263  st_table * tab)
264{
265    if (n == NIL(DdNode))
266        return(0);
267
268    if (st_is_member(tab, (char *)n) == 1)
269        return(0);
270
271    if (Cudd_IsConstant(n))
272        return(0);
273
274    (void)st_insert(tab, (char *)n, NIL(char));
275    return(1 + cuddZddDagInt(cuddT(n), tab) +
276        cuddZddDagInt(cuddE(n), tab));
277
278} /* cuddZddDagInt */
Note: See TracBrowser for help on using the repository browser.