source: vis_dev/vis-2.3/src/synth/synthCount.c

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

vis2.3
File size: 10.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [synthCount.c]
4
5  PackageName [synth]
6
7  Synopsis    [Literal counting functions.]
8
9  Author      [In-Ho Moon, Balakrishna Kumthekar]
10
11  Copyright [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "synthInt.h"
18
19static char rcsid[] UNUSED = "$Id: synthCount.c,v 1.14 1998/08/31 19:22:12 mooni Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25
26/*---------------------------------------------------------------------------*/
27/* Type declarations                                                         */
28/*---------------------------------------------------------------------------*/
29
30
31/*---------------------------------------------------------------------------*/
32/* Structure declarations                                                    */
33/*---------------------------------------------------------------------------*/
34
35
36/*---------------------------------------------------------------------------*/
37/* Variable declarations                                                     */
38/*---------------------------------------------------------------------------*/
39
40/**AutomaticStart*************************************************************/
41
42/*---------------------------------------------------------------------------*/
43/* Static function prototypes                                                */
44/*---------------------------------------------------------------------------*/
45
46static int CountMultiLevelFactor(bdd_manager *dd, MlTree *top, MlTree *tree, int ref);
47static int GetLiteralCount(bdd_manager *dd, bdd_node *node, int nLiterals);
48
49/**AutomaticEnd***************************************************************/
50
51
52/*---------------------------------------------------------------------------*/
53/* Definition of exported functions                                          */
54/*---------------------------------------------------------------------------*/
55
56
57/*---------------------------------------------------------------------------*/
58/* Definition of internal functions                                          */
59/*---------------------------------------------------------------------------*/
60
61/**Function********************************************************************
62
63  Synopsis [Counts the number of literals of a MlTree.]
64
65  Description [Counts the number of literals of a MlTree. The argument
66  ref controls whether to count shared literals or non-shared. If ref is
67  1, it counts shared literals.]
68
69  SideEffects []
70
71  SeeAlso     []
72
73******************************************************************************/
74int
75SynthCountMlLiteral(bdd_manager *dd,
76                    MlTree *tree,
77                    int ref)
78{
79  bdd_node      *one = bdd_read_one(dd);
80  bdd_node      *zero = bdd_read_zero(dd);
81  int           count = 0;
82
83  if (tree->top || tree->shared) {
84    if (ref && tree->ref) {
85      if (tree->node != zero && tree->node != one)
86        count = 1;
87      return(count);
88    }
89    count += CountMultiLevelFactor(dd, tree, tree, ref);
90  }
91
92  if (tree->leaf)
93    return(count);
94
95  if (tree->q_ref == 0)
96    count += SynthCountMlLiteral(dd, tree->q, ref);
97  if (tree->d_ref == 0)
98    count += SynthCountMlLiteral(dd, tree->d, ref);
99  if (tree->r_ref == 0)
100    count += SynthCountMlLiteral(dd, tree->r, ref);
101
102  return(count);
103}
104
105
106/**Function********************************************************************
107
108  Synopsis [Makes a bit string for representing the support of a node.]
109
110  Description [Makes a bit string for representing the support of a node.
111  It returns the number of support variables of the ZDD node. The
112  argument mask is given by caller, which is array of unsigned integer.]
113
114  SideEffects []
115
116  SeeAlso     []
117
118******************************************************************************/
119int
120SynthGetSupportMask(bdd_manager *dd,
121                    bdd_node *node,
122                    unsigned int *mask)
123{
124  int           i, pos, count;
125  int           word, size;
126  int           bit, bit_mask;
127  int           *support;
128  int           zddSize = bdd_num_zdd_vars(dd);
129
130  count = 0;
131  word = sizeof(int) * 8;
132  size = zddSize / word + 1;
133
134  support = ALLOC(int, zddSize);
135  (void)memset((void *)support, 0, sizeof(int) * zddSize);
136  (void)memset((void *)mask, 0, size * sizeof(int));
137  SynthZddSupportStep(bdd_regular(node), support);
138  SynthZddClearFlag(bdd_regular(node));
139  for (i = 0; i < zddSize; i++) {
140    if (support[i]) {
141      pos = i / word;
142      bit = i % word;
143      bit_mask = 01 << bit;
144      mask[pos] |= bit_mask;
145      count++;
146    }
147  }
148  FREE(support);
149  return(count);
150}
151
152
153/**Function********************************************************************
154
155  Synopsis [Returns the number of support variables of a node.]
156
157  Description [Returns the number of support variables of a node.]
158
159  SideEffects []
160
161  SeeAlso     []
162
163******************************************************************************/
164int
165SynthGetSupportCount(bdd_manager *dd,
166                     bdd_node *node)
167{
168  int           i, count;
169  int           *support;
170  int           zddSize = bdd_num_zdd_vars(dd);
171
172  count = 0;
173  support = ALLOC(int, zddSize);
174  (void)memset((void *)support, 0, sizeof(int) * zddSize);
175  SynthZddSupportStep(bdd_regular(node), support);
176  SynthZddClearFlag(bdd_regular(node));
177  for (i = 0; i < zddSize; i++) {
178    if (support[i])
179      count++;
180  }
181  FREE(support);
182  return(count);
183}
184
185
186/**Function********************************************************************
187
188  Synopsis [Finds the support of f.]
189
190  Description [Finds the support of f. Performs a DFS from f. Whenever a node
191  is visited, the variable of the node is accumulated in support, and the
192  the node is marked not to be visited again. Uses the LSB of the next pointer
193  as visited flag.]
194
195  SideEffects [Once this function is called, SynthZddClearFlag() should
196  be called right after.]
197
198  SeeAlso     [SynthZddClearFlag]
199
200******************************************************************************/
201void
202SynthZddSupportStep(bdd_node *f, int *support)
203{
204  if (bdd_is_constant(f) || bdd_is_complement(bdd_read_next(f))) {
205    return;
206  }
207
208  support[bdd_node_read_index(f)] = 1;
209  SynthZddSupportStep(bdd_bdd_T(f),support);
210  SynthZddSupportStep(bdd_regular(bdd_bdd_E(f)),support);
211  /* Mark as visited. */
212  bdd_set_next(f, bdd_not_bdd_node(bdd_read_next(f)));
213  return;
214}
215
216
217/**Function********************************************************************
218
219  Synopsis [Performs a DFS from f, clearing the LSB of the next pointers.]
220
221  Description [Performs a DFS from f, clearing the LSB of the next pointers.]
222
223  SideEffects []
224
225  SeeAlso     [SynthZddSupportStep]
226
227******************************************************************************/
228void
229SynthZddClearFlag(bdd_node *f)
230{
231  bdd_node *temp;
232
233  temp = bdd_read_next(f);
234
235  if (!bdd_is_complement(temp)) {
236    return;
237  }
238  /* Clear visited flag. */
239  bdd_set_next(f, bdd_regular(temp));
240  if (bdd_is_constant(f)) {
241    return;
242  }
243  SynthZddClearFlag(bdd_bdd_T(f));
244  SynthZddClearFlag(bdd_regular(bdd_bdd_E(f)));
245  return;
246}
247
248
249/**Function********************************************************************
250
251  Synopsis [Counts the number of literals in a ZDD cover.]
252
253  Description [Counts the number of literals in a ZDD cover.]
254
255  SideEffects []
256
257  SeeAlso     []
258
259******************************************************************************/
260int
261SynthGetLiteralCount(bdd_manager *dd,
262                     bdd_node *node)
263{
264  return(GetLiteralCount(dd, node, 0));
265}
266
267
268/*---------------------------------------------------------------------------*/
269/* Definition of static functions                                            */
270/*---------------------------------------------------------------------------*/
271
272/**Function********************************************************************
273
274  Synopsis [Counts the number of literals of a MlTree.]
275
276  Description [Counts the number of literals of a MlTree.]
277
278  SideEffects []
279
280  SeeAlso     [SynthCountMlLiteral]
281
282******************************************************************************/
283static int
284CountMultiLevelFactor(bdd_manager *dd,
285                      MlTree *top,
286                      MlTree *tree,
287                      int ref)
288{
289  bdd_node      *one = bdd_read_one(dd);
290  bdd_node      *zero = bdd_read_zero(dd);
291  bdd_node      *f;
292  int           i, *support;
293  int           count = 0;
294  int           sizeZ = bdd_num_zdd_vars(dd);
295
296  if (ref && tree != top && tree->shared)
297    return(1);
298
299  f = tree->node;
300  if (f == one || f == zero)
301    return(0);
302
303  if (tree->leaf) {
304    support = ALLOC(int, sizeZ);
305    if (!support)
306      return(0);
307    (void)memset((void *)support, 0, sizeof(int) * sizeZ);
308    SynthZddSupportStep(bdd_regular(tree->node), support);
309    SynthZddClearFlag(bdd_regular(tree->node));
310    for (i = 0; i < sizeZ; i++) {
311      if (support[i])
312        count++;
313    }
314    FREE(support);
315    return(count);
316  }
317
318  count += CountMultiLevelFactor(dd, top, tree->q, ref);
319  count += CountMultiLevelFactor(dd, top, tree->d, ref);
320  count += CountMultiLevelFactor(dd, top, tree->r, ref);
321
322  return(count);
323}
324
325
326/**Function********************************************************************
327
328  Synopsis [Recursive procedure of SynthGetLiteralCount.]
329
330  Description [Recursive procedure of SynthGetLiteralCount. Counts the
331  number of literals in a ZDD cover. The argument nLiterals is the
332  number of literals currently counted.]
333
334  SideEffects []
335
336  SeeAlso     []
337
338******************************************************************************/
339static int
340GetLiteralCount(bdd_manager *dd,
341                bdd_node *node,
342                int nLiterals)
343{
344  bdd_node      *one = bdd_read_one(dd);
345  bdd_node      *zero = bdd_read_zero(dd);
346  int           count = 0;
347
348  if (node == zero)
349    return(0);
350  if (node == one)
351    return(nLiterals);
352
353  count = GetLiteralCount(dd, bdd_bdd_T(node), nLiterals + 1);
354  count += GetLiteralCount(dd, bdd_bdd_E(node), nLiterals);
355
356  return(count);
357}
Note: See TracBrowser for help on using the repository browser.