1 | /**CFile*********************************************************************** |
---|
2 | |
---|
3 | FileName [cuPortIter.c] |
---|
4 | |
---|
5 | PackageName [cu_port] |
---|
6 | |
---|
7 | Synopsis [Port routines for CU package.] |
---|
8 | |
---|
9 | Description [optional] |
---|
10 | |
---|
11 | SeeAlso [optional] |
---|
12 | |
---|
13 | Author [Abelardo Pardo <abel@vlsi.colorado.edu> ] |
---|
14 | |
---|
15 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
16 | |
---|
17 | All rights reserved. |
---|
18 | |
---|
19 | Redistribution and use in source and binary forms, with or without |
---|
20 | modification, are permitted provided that the following conditions |
---|
21 | are met: |
---|
22 | |
---|
23 | Redistributions of source code must retain the above copyright |
---|
24 | notice, this list of conditions and the following disclaimer. |
---|
25 | |
---|
26 | Redistributions in binary form must reproduce the above copyright |
---|
27 | notice, this list of conditions and the following disclaimer in the |
---|
28 | documentation and/or other materials provided with the distribution. |
---|
29 | |
---|
30 | Neither the name of the University of Colorado nor the names of its |
---|
31 | contributors may be used to endorse or promote products derived from |
---|
32 | this software without specific prior written permission. |
---|
33 | |
---|
34 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
35 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
36 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
37 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
38 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
39 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
40 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
41 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
42 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
43 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
44 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
45 | POSSIBILITY OF SUCH DAMAGE.] |
---|
46 | |
---|
47 | ******************************************************************************/ |
---|
48 | |
---|
49 | #include "cuPortInt.h" |
---|
50 | |
---|
51 | #ifndef lint |
---|
52 | static char rcsid[] UNUSED = "$Id: cuPortIter.c,v 1.13 2004/08/13 18:39:31 fabio Exp $"; |
---|
53 | #endif |
---|
54 | |
---|
55 | /*---------------------------------------------------------------------------*/ |
---|
56 | /* Constant declarations */ |
---|
57 | /*---------------------------------------------------------------------------*/ |
---|
58 | |
---|
59 | |
---|
60 | /*---------------------------------------------------------------------------*/ |
---|
61 | /* Type declarations */ |
---|
62 | /*---------------------------------------------------------------------------*/ |
---|
63 | |
---|
64 | /*---------------------------------------------------------------------------*/ |
---|
65 | /* Structure declarations */ |
---|
66 | /*---------------------------------------------------------------------------*/ |
---|
67 | typedef struct { |
---|
68 | DdManager *manager; |
---|
69 | DdGen *ddGen; |
---|
70 | array_t *cube; |
---|
71 | } cu_bdd_gen; |
---|
72 | |
---|
73 | /*---------------------------------------------------------------------------*/ |
---|
74 | /* Variable declarations */ |
---|
75 | /*---------------------------------------------------------------------------*/ |
---|
76 | |
---|
77 | |
---|
78 | /*---------------------------------------------------------------------------*/ |
---|
79 | /* Macro declarations */ |
---|
80 | /*---------------------------------------------------------------------------*/ |
---|
81 | |
---|
82 | |
---|
83 | /**AutomaticStart*************************************************************/ |
---|
84 | |
---|
85 | /*---------------------------------------------------------------------------*/ |
---|
86 | /* Static function prototypes */ |
---|
87 | /*---------------------------------------------------------------------------*/ |
---|
88 | |
---|
89 | |
---|
90 | /**AutomaticEnd***************************************************************/ |
---|
91 | |
---|
92 | /*---------------------------------------------------------------------------*/ |
---|
93 | /* Definition of exported functions */ |
---|
94 | /*---------------------------------------------------------------------------*/ |
---|
95 | |
---|
96 | /**Function******************************************************************** |
---|
97 | |
---|
98 | Synopsis [Returns the status of a bdd generator.] |
---|
99 | |
---|
100 | SideEffects [] |
---|
101 | |
---|
102 | SeeAlso [bdd_first_cube bdd_next_cube bdd_gen_free] |
---|
103 | |
---|
104 | ******************************************************************************/ |
---|
105 | bdd_gen_status |
---|
106 | bdd_gen_read_status(bdd_gen *gen) |
---|
107 | { |
---|
108 | if (Cudd_IsGenEmpty(((cu_bdd_gen *)gen)->ddGen)) { |
---|
109 | return bdd_EMPTY; |
---|
110 | } |
---|
111 | else { |
---|
112 | return bdd_NONEMPTY; |
---|
113 | } |
---|
114 | |
---|
115 | } /* end of bdd_gen_read_status */ |
---|
116 | |
---|
117 | |
---|
118 | /**Function******************************************************************** |
---|
119 | |
---|
120 | Synopsis [Returns the first disjoint cube of the function. |
---|
121 | A generator is also returned, which will iterate over the rest.] |
---|
122 | |
---|
123 | Description [Defines an iterator on the onset of a BDD. Two routines |
---|
124 | are provided: bdd_first_cube, which extracts one cube from a BDD and |
---|
125 | returns a bdd_gen structure containing the information necessary to |
---|
126 | continue the enumeration; and bdd_next_disjoint_cube, which returns 1 if |
---|
127 | another cube was found, and 0 otherwise. A cube is represented as an |
---|
128 | array of bdd_literal (which are integers in {0, 1, 2}), where 0 |
---|
129 | represents negated literal, 1 for literal, and 2 for don't care. |
---|
130 | Returns a disjoint cover. A third routine is there to clean up.] |
---|
131 | |
---|
132 | SideEffects [] |
---|
133 | |
---|
134 | SeeAlso [bdd_next_cube bdd_gen_free] |
---|
135 | |
---|
136 | ******************************************************************************/ |
---|
137 | bdd_gen * |
---|
138 | bdd_first_disjoint_cube(bdd_t *fn, array_t **cube /* of bdd_literal */) |
---|
139 | { |
---|
140 | DdManager *manager; |
---|
141 | cu_bdd_gen *gen; |
---|
142 | int i; |
---|
143 | int *icube; |
---|
144 | CUDD_VALUE_TYPE value; |
---|
145 | |
---|
146 | /* Make sure we receive a valid bdd_t. (So to speak.) */ |
---|
147 | assert(fn != 0); |
---|
148 | |
---|
149 | manager = (DdManager *)fn->mgr; |
---|
150 | |
---|
151 | /* Initialize the generator. */ |
---|
152 | gen = ALLOC(cu_bdd_gen,1); |
---|
153 | if (gen == NULL) { |
---|
154 | return(NIL(bdd_gen)); |
---|
155 | } |
---|
156 | gen->manager = manager; |
---|
157 | |
---|
158 | gen->cube = array_alloc(bdd_literal, manager->size); |
---|
159 | if (gen->cube == NULL) { |
---|
160 | fail("Bdd Package: Out of memory in bdd_first_cube"); |
---|
161 | } |
---|
162 | |
---|
163 | gen->ddGen = Cudd_FirstCube(manager,(DdNode *)fn->node,&icube,&value); |
---|
164 | if (gen->ddGen == NULL) { |
---|
165 | fail("Cudd Package: Out of memory in bdd_first_cube"); |
---|
166 | } |
---|
167 | |
---|
168 | if (!Cudd_IsGenEmpty(gen->ddGen)) { |
---|
169 | /* Copy icube to the array_t cube. */ |
---|
170 | for (i = 0; i < manager->size; i++) { |
---|
171 | int myconst = icube[i]; |
---|
172 | array_insert(bdd_literal, gen->cube, i, myconst); |
---|
173 | } |
---|
174 | *cube = gen->cube; |
---|
175 | } |
---|
176 | |
---|
177 | return(gen); |
---|
178 | |
---|
179 | } /* end of bdd_first_disjoint_cube */ |
---|
180 | |
---|
181 | |
---|
182 | /**Function******************************************************************** |
---|
183 | |
---|
184 | Synopsis [Gets the next cube on the generator. Returns {TRUE, |
---|
185 | FALSE} when {more, no more}.] |
---|
186 | |
---|
187 | SideEffects [] |
---|
188 | |
---|
189 | SeeAlso [bdd_first_cube bdd_gen_free] |
---|
190 | |
---|
191 | ******************************************************************************/ |
---|
192 | boolean |
---|
193 | bdd_next_disjoint_cube(bdd_gen *gen_, array_t **cube /* of bdd_literal */) |
---|
194 | { |
---|
195 | cu_bdd_gen *gen; |
---|
196 | int retval; |
---|
197 | int *icube; |
---|
198 | CUDD_VALUE_TYPE value; |
---|
199 | int i; |
---|
200 | |
---|
201 | gen = (cu_bdd_gen *)gen_; |
---|
202 | |
---|
203 | retval = Cudd_NextCube(gen->ddGen,&icube,&value); |
---|
204 | if (!Cudd_IsGenEmpty(gen->ddGen)) { |
---|
205 | /* Copy icube to the array_t cube. */ |
---|
206 | for (i = 0; i < gen->manager->size; i++) { |
---|
207 | int myconst = icube[i]; |
---|
208 | array_insert(bdd_literal, gen->cube, i, myconst); |
---|
209 | } |
---|
210 | *cube = gen->cube; |
---|
211 | } |
---|
212 | |
---|
213 | return(retval); |
---|
214 | |
---|
215 | } /* end of bdd_next_disjoint_cube */ |
---|
216 | |
---|
217 | |
---|
218 | /**Function******************************************************************** |
---|
219 | |
---|
220 | Synopsis [Returns the first cube of the function. |
---|
221 | A generator is also returned, which will iterate over the rest.] |
---|
222 | |
---|
223 | Description [Defines an iterator on the onset of a BDD. Two routines |
---|
224 | are provided: bdd_first_cube, which extracts one cube from a BDD and |
---|
225 | returns a bdd_gen structure containing the information necessary to |
---|
226 | continue the enumeration; and bdd_next_cube, which returns 1 if |
---|
227 | another cube was found, and 0 otherwise. A cube is represented as an |
---|
228 | array of bdd_literal (which are integers in {0, 1, 2}), where 0 |
---|
229 | represents negated literal, 1 for literal, and 2 for don't care. |
---|
230 | Returns a prime and irredundant cover. A third routine is there to |
---|
231 | clean up.] |
---|
232 | |
---|
233 | SideEffects [] |
---|
234 | |
---|
235 | SeeAlso [bdd_next_cube bdd_gen_free] |
---|
236 | |
---|
237 | ******************************************************************************/ |
---|
238 | bdd_gen * |
---|
239 | bdd_first_cube(bdd_t *fn, array_t **cube /* of bdd_literal */) |
---|
240 | { |
---|
241 | DdManager *manager; |
---|
242 | cu_bdd_gen *gen; |
---|
243 | int i; |
---|
244 | int *icube; |
---|
245 | |
---|
246 | /* Make sure we receive a valid bdd_t. (So to speak.) */ |
---|
247 | assert(fn != 0); |
---|
248 | |
---|
249 | manager = (DdManager *)fn->mgr; |
---|
250 | |
---|
251 | /* Initialize the generator. */ |
---|
252 | gen = ALLOC(cu_bdd_gen,1); |
---|
253 | if (gen == NULL) { |
---|
254 | return(NIL(bdd_gen)); |
---|
255 | } |
---|
256 | gen->manager = manager; |
---|
257 | |
---|
258 | gen->cube = array_alloc(bdd_literal, manager->size); |
---|
259 | if (gen->cube == NULL) { |
---|
260 | fail("Bdd Package: Out of memory in bdd_first_cube"); |
---|
261 | } |
---|
262 | |
---|
263 | gen->ddGen = Cudd_FirstPrime(manager,(DdNode *)fn->node, |
---|
264 | (DdNode *)fn->node,&icube); |
---|
265 | if (gen->ddGen == NULL) { |
---|
266 | fail("Cudd Package: Out of memory in bdd_first_cube"); |
---|
267 | } |
---|
268 | |
---|
269 | if (!Cudd_IsGenEmpty(gen->ddGen)) { |
---|
270 | /* Copy icube to the array_t cube. */ |
---|
271 | for (i = 0; i < manager->size; i++) { |
---|
272 | int myconst = icube[i]; |
---|
273 | array_insert(bdd_literal, gen->cube, i, myconst); |
---|
274 | } |
---|
275 | *cube = gen->cube; |
---|
276 | } |
---|
277 | |
---|
278 | return(gen); |
---|
279 | |
---|
280 | } /* end of bdd_first_cube */ |
---|
281 | |
---|
282 | |
---|
283 | /**Function******************************************************************** |
---|
284 | |
---|
285 | Synopsis [Gets the next cube on the generator. Returns {TRUE, |
---|
286 | FALSE} when {more, no more}.] |
---|
287 | |
---|
288 | SideEffects [] |
---|
289 | |
---|
290 | SeeAlso [bdd_first_prime bdd_gen_free] |
---|
291 | |
---|
292 | ******************************************************************************/ |
---|
293 | boolean |
---|
294 | bdd_next_cube(bdd_gen *gen_, array_t **cube /* of bdd_literal */) |
---|
295 | { |
---|
296 | cu_bdd_gen *gen; |
---|
297 | int retval; |
---|
298 | int *icube; |
---|
299 | int i; |
---|
300 | |
---|
301 | gen = (cu_bdd_gen *)gen_; |
---|
302 | |
---|
303 | retval = Cudd_NextPrime(gen->ddGen,&icube); |
---|
304 | if (!Cudd_IsGenEmpty(gen->ddGen)) { |
---|
305 | /* Copy icube to the array_t cube. */ |
---|
306 | for (i = 0; i < gen->manager->size; i++) { |
---|
307 | int myconst = icube[i]; |
---|
308 | array_insert(bdd_literal, gen->cube, i, myconst); |
---|
309 | } |
---|
310 | *cube = gen->cube; |
---|
311 | } |
---|
312 | |
---|
313 | return(retval); |
---|
314 | |
---|
315 | } /* end of bdd_next_cube */ |
---|
316 | |
---|
317 | |
---|
318 | /**Function******************************************************************** |
---|
319 | |
---|
320 | Synopsis [Gets the first node in the BDD and returns a generator.] |
---|
321 | |
---|
322 | SideEffects [] |
---|
323 | |
---|
324 | SeeAlso [bdd_next_node] |
---|
325 | |
---|
326 | ******************************************************************************/ |
---|
327 | bdd_gen * |
---|
328 | bdd_first_node(bdd_t *fn, bdd_node **node /* return */) |
---|
329 | { |
---|
330 | bdd_manager *manager; |
---|
331 | cu_bdd_gen *gen; |
---|
332 | |
---|
333 | /* Make sure we receive a valid bdd_t. (So to speak.) */ |
---|
334 | assert(fn != 0); |
---|
335 | |
---|
336 | manager = fn->mgr; |
---|
337 | |
---|
338 | /* Initialize the generator. */ |
---|
339 | gen = ALLOC(cu_bdd_gen,1); |
---|
340 | if (gen == NULL) return(NULL); |
---|
341 | gen->manager = (DdManager *) manager; |
---|
342 | gen->cube = NULL; |
---|
343 | |
---|
344 | gen->ddGen = Cudd_FirstNode((DdManager *)manager,(DdNode *)fn->node, |
---|
345 | (DdNode **)node); |
---|
346 | if (gen->ddGen == NULL) { |
---|
347 | fail("Cudd Package: Out of memory in bdd_first_node"); |
---|
348 | } |
---|
349 | |
---|
350 | return(gen); |
---|
351 | |
---|
352 | } /* end of bdd_first_node */ |
---|
353 | |
---|
354 | |
---|
355 | /**Function******************************************************************** |
---|
356 | |
---|
357 | Synopsis [Gets the next node in the BDD. Returns {TRUE, FALSE} when |
---|
358 | {more, no more}.] |
---|
359 | |
---|
360 | SideEffects [] |
---|
361 | |
---|
362 | SeeAlso [bdd_first_node] |
---|
363 | |
---|
364 | ******************************************************************************/ |
---|
365 | boolean |
---|
366 | bdd_next_node(bdd_gen *gen, bdd_node **node /* return */) |
---|
367 | { |
---|
368 | return(Cudd_NextNode(((cu_bdd_gen *)gen)->ddGen,(DdNode **)node)); |
---|
369 | |
---|
370 | } /* end of bdd_next_node */ |
---|
371 | |
---|
372 | |
---|
373 | /**Function******************************************************************** |
---|
374 | |
---|
375 | Synopsis [Frees up the space used by the generator. Returns an int |
---|
376 | so that it is easier to fit in a foreach macro. Returns 0 (to make it |
---|
377 | easy to put in expressions).] |
---|
378 | |
---|
379 | SideEffects [] |
---|
380 | |
---|
381 | SeeAlso [] |
---|
382 | |
---|
383 | ******************************************************************************/ |
---|
384 | int |
---|
385 | bdd_gen_free(bdd_gen *gen_) |
---|
386 | { |
---|
387 | cu_bdd_gen *gen; |
---|
388 | |
---|
389 | gen = (cu_bdd_gen *)gen_; |
---|
390 | if (gen->cube != NULL) array_free(gen->cube); |
---|
391 | Cudd_GenFree(gen->ddGen); |
---|
392 | FREE(gen); |
---|
393 | return(0); |
---|
394 | |
---|
395 | } /* end of bdd_gen_free */ |
---|
396 | |
---|
397 | /*---------------------------------------------------------------------------*/ |
---|
398 | /* Definition of static functions */ |
---|
399 | /*---------------------------------------------------------------------------*/ |
---|