[13] | 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 | /*---------------------------------------------------------------------------*/ |
---|