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

Last change on this file since 23 was 14, checked in by cecile, 15 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.