| 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 | /*---------------------------------------------------------------------------*/ |
|---|