[13] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [calPortIter.c] |
---|
| 4 | |
---|
| 5 | PackageName [calPort] |
---|
| 6 | |
---|
| 7 | Synopsis [required] |
---|
| 8 | |
---|
| 9 | Description [optional] |
---|
| 10 | |
---|
| 11 | SeeAlso [optional] |
---|
| 12 | |
---|
| 13 | Author [Rajeev K. Ranjan. Modified from the CMU port package |
---|
| 14 | written by Tom Shiple.] |
---|
| 15 | |
---|
| 16 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
---|
| 17 | All rights reserved. |
---|
| 18 | |
---|
| 19 | Permission is hereby granted, without written agreement and without license |
---|
| 20 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
| 21 | documentation for any purpose, provided that the above copyright notice and |
---|
| 22 | the following two paragraphs appear in all copies of this software. |
---|
| 23 | |
---|
| 24 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
---|
| 25 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
---|
| 26 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
---|
| 27 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
---|
| 28 | |
---|
| 29 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
---|
| 30 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
---|
| 31 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
---|
| 32 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
---|
| 33 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
---|
| 34 | |
---|
| 35 | ******************************************************************************/ |
---|
| 36 | #include "calPortInt.h" |
---|
| 37 | |
---|
| 38 | /*---------------------------------------------------------------------------*/ |
---|
| 39 | /* Constant declarations */ |
---|
| 40 | /*---------------------------------------------------------------------------*/ |
---|
| 41 | |
---|
| 42 | |
---|
| 43 | /*---------------------------------------------------------------------------*/ |
---|
| 44 | /* Type declarations */ |
---|
| 45 | /*---------------------------------------------------------------------------*/ |
---|
| 46 | typedef struct CalBddGenStruct CalBddGen_t; |
---|
| 47 | /* |
---|
| 48 | * Traversal of BDD Formulas |
---|
| 49 | */ |
---|
| 50 | |
---|
| 51 | typedef enum { |
---|
| 52 | bdd_gen_cubes, |
---|
| 53 | bdd_gen_nodes |
---|
| 54 | } bdd_gen_type; |
---|
| 55 | |
---|
| 56 | |
---|
| 57 | /*---------------------------------------------------------------------------*/ |
---|
| 58 | /* Structure declarations */ |
---|
| 59 | /*---------------------------------------------------------------------------*/ |
---|
| 60 | struct CalBddGenStruct { |
---|
| 61 | Cal_BddManager manager; |
---|
| 62 | bdd_gen_status status; |
---|
| 63 | bdd_gen_type type; |
---|
| 64 | union { |
---|
| 65 | struct { |
---|
| 66 | array_t *cube; /* of bdd_literal */ |
---|
| 67 | } cubes; |
---|
| 68 | struct { |
---|
| 69 | st_table *visited; /* of bdd_node* */ |
---|
| 70 | } nodes; |
---|
| 71 | } gen; |
---|
| 72 | struct { |
---|
| 73 | int sp; |
---|
| 74 | CalBddNode_t **nodeStack; |
---|
| 75 | int *idStack; |
---|
| 76 | } stack; |
---|
| 77 | CalBddNode_t *node; |
---|
| 78 | }; |
---|
| 79 | |
---|
| 80 | |
---|
| 81 | |
---|
| 82 | |
---|
| 83 | /*---------------------------------------------------------------------------*/ |
---|
| 84 | /* Variable declarations */ |
---|
| 85 | /*---------------------------------------------------------------------------*/ |
---|
| 86 | |
---|
| 87 | |
---|
| 88 | /*---------------------------------------------------------------------------*/ |
---|
| 89 | /* Macro declarations */ |
---|
| 90 | /*---------------------------------------------------------------------------*/ |
---|
| 91 | |
---|
| 92 | |
---|
| 93 | /**AutomaticStart*************************************************************/ |
---|
| 94 | |
---|
| 95 | /*---------------------------------------------------------------------------*/ |
---|
| 96 | /* Static function prototypes */ |
---|
| 97 | /*---------------------------------------------------------------------------*/ |
---|
| 98 | static void pop_node_stack(CalBddGen_t *gen); |
---|
| 99 | static void push_node_stack(Cal_Bdd_t f, CalBddGen_t *gen); |
---|
| 100 | static void pop_cube_stack(CalBddGen_t *gen); |
---|
| 101 | static void push_cube_stack(Cal_Bdd_t f, CalBddGen_t *gen); |
---|
| 102 | |
---|
| 103 | /**AutomaticEnd***************************************************************/ |
---|
| 104 | |
---|
| 105 | |
---|
| 106 | /*---------------------------------------------------------------------------*/ |
---|
| 107 | /* Definition of exported functions */ |
---|
| 108 | /*---------------------------------------------------------------------------*/ |
---|
| 109 | /* |
---|
| 110 | * Defines an iterator on the onset of a BDD. Two routines are |
---|
| 111 | * provided: bdd_first_cube, which extracts one cube from a BDD and |
---|
| 112 | * returns a bdd_gen structure containing the information necessary to |
---|
| 113 | * continue the enumeration; and bdd_next_cube, which returns 1 if |
---|
| 114 | * another cube was |
---|
| 115 | * found, and 0 otherwise. A cube is represented |
---|
| 116 | * as an array of bdd_literal (which are integers in {0, 1, 2}), |
---|
| 117 | * where 0 represents |
---|
| 118 | * negated literal, 1 for literal, and 2 for don't care. Returns a |
---|
| 119 | * disjoint |
---|
| 120 | * cover. A third routine is there to clean up. |
---|
| 121 | */ |
---|
| 122 | |
---|
| 123 | bdd_gen_status |
---|
| 124 | bdd_gen_read_status(bdd_gen *gen) |
---|
| 125 | { |
---|
| 126 | return ((CalBddGen_t *)gen)->status; |
---|
| 127 | } |
---|
| 128 | |
---|
| 129 | /**Function******************************************************************** |
---|
| 130 | |
---|
| 131 | Synopsis [required] |
---|
| 132 | |
---|
| 133 | Description [bdd_first_cube - return the first cube of the function. |
---|
| 134 | A generator is returned that will iterate over the rest. Return the |
---|
| 135 | generator. ] |
---|
| 136 | |
---|
| 137 | SideEffects [required] |
---|
| 138 | |
---|
| 139 | SeeAlso [optional] |
---|
| 140 | |
---|
| 141 | ******************************************************************************/ |
---|
| 142 | bdd_gen * |
---|
| 143 | bdd_first_cube(bdd_t *fn,array_t **cube) |
---|
| 144 | { |
---|
| 145 | Cal_BddManager_t *manager; |
---|
| 146 | CalBddGen_t *gen; |
---|
| 147 | int i; |
---|
| 148 | long numVars; |
---|
| 149 | Cal_Bdd function; |
---|
| 150 | Cal_Bdd_t calBdd; |
---|
| 151 | |
---|
| 152 | if (fn == NIL(bdd_t)) { |
---|
| 153 | CalBddFatalMessage("bdd_first_cube: invalid BDD"); |
---|
| 154 | } |
---|
| 155 | |
---|
| 156 | manager = fn->bddManager; |
---|
| 157 | function = fn->calBdd; |
---|
| 158 | |
---|
| 159 | /* |
---|
| 160 | * Allocate a new generator structure and fill it in; the stack and the |
---|
| 161 | * cube will be used, but the visited table and the node will not be used. |
---|
| 162 | */ |
---|
| 163 | gen = ALLOC(CalBddGen_t, 1); |
---|
| 164 | |
---|
| 165 | /* |
---|
| 166 | * first - init all the members to a rational value for cube iteration |
---|
| 167 | */ |
---|
| 168 | gen->manager = manager; |
---|
| 169 | gen->status = bdd_EMPTY; |
---|
| 170 | gen->type = bdd_gen_cubes; |
---|
| 171 | gen->gen.cubes.cube = NIL(array_t); |
---|
| 172 | gen->stack.sp = 0; |
---|
| 173 | gen->stack.nodeStack = NIL(CalBddNode_t *); |
---|
| 174 | gen->stack.idStack = NIL(int); |
---|
| 175 | gen->node = NIL(CalBddNode_t); |
---|
| 176 | |
---|
| 177 | numVars = Cal_BddVars(manager); |
---|
| 178 | gen->gen.cubes.cube = array_alloc(bdd_literal, numVars); |
---|
| 179 | |
---|
| 180 | /* |
---|
| 181 | * Initialize each literal to 2 (don't care). |
---|
| 182 | */ |
---|
| 183 | for (i = 0; i < numVars; i++) { |
---|
| 184 | array_insert(bdd_literal, gen->gen.cubes.cube, i, 2); |
---|
| 185 | } |
---|
| 186 | |
---|
| 187 | /* |
---|
| 188 | * The stack size will never exceed the number of variables in the BDD, since |
---|
| 189 | * the longest possible path from root to constant 1 is the number |
---|
| 190 | * of variables in the BDD. |
---|
| 191 | */ |
---|
| 192 | gen->stack.sp = 0; |
---|
| 193 | gen->stack.nodeStack = ALLOC(CalBddNode_t *, numVars); |
---|
| 194 | gen->stack.idStack = ALLOC(int, numVars); |
---|
| 195 | |
---|
| 196 | /* |
---|
| 197 | * Clear out the stack so that in bdd_gen_free, we can decrement the |
---|
| 198 | * ref count of those nodes still on the stack. |
---|
| 199 | */ |
---|
| 200 | for (i = 0; i < numVars; i++) { |
---|
| 201 | gen->stack.nodeStack[i] = NIL(CalBddNode_t); |
---|
| 202 | gen->stack.idStack[i] = -1; |
---|
| 203 | } |
---|
| 204 | |
---|
| 205 | if (Cal_BddIsBddZero(manager, function)){ |
---|
| 206 | /* |
---|
| 207 | * All done, for this was but the zero constant ... |
---|
| 208 | * We are enumerating the onset, (which is vacuous). |
---|
| 209 | * gen->status initialized to bdd_EMPTY above, so this |
---|
| 210 | * appears to be redundant. |
---|
| 211 | */ |
---|
| 212 | gen->status = bdd_EMPTY; |
---|
| 213 | } else { |
---|
| 214 | /* |
---|
| 215 | * Get to work enumerating the onset. Get the first cube. Note that |
---|
| 216 | * if fn is just the constant 1, push_cube_stack will properly |
---|
| 217 | * handle this. |
---|
| 218 | * Get a new pointer to fn->node beforehand: this increments |
---|
| 219 | * the reference count of fn->node; this is necessary, because |
---|
| 220 | * when fn->node |
---|
| 221 | * is popped from the stack at the very end, it's ref count is |
---|
| 222 | * decremented. |
---|
| 223 | */ |
---|
| 224 | gen->status = bdd_NONEMPTY; |
---|
| 225 | calBdd = CalBddGetInternalBdd(manager, function); |
---|
| 226 | push_cube_stack(calBdd, gen); |
---|
| 227 | } |
---|
| 228 | *cube = gen->gen.cubes.cube; |
---|
| 229 | return (bdd_gen *)(gen); |
---|
| 230 | } |
---|
| 231 | |
---|
| 232 | /**Function******************************************************************** |
---|
| 233 | |
---|
| 234 | Synopsis [required] |
---|
| 235 | |
---|
| 236 | Description [bdd_next_cube - get the next cube on the generator. |
---|
| 237 | Returns {TRUE, FALSE} when {more, no more}.] |
---|
| 238 | |
---|
| 239 | SideEffects [required] |
---|
| 240 | |
---|
| 241 | SeeAlso [optional] |
---|
| 242 | |
---|
| 243 | ******************************************************************************/ |
---|
| 244 | boolean |
---|
| 245 | bdd_next_cube(bdd_gen *gen_, array_t **cube) |
---|
| 246 | { |
---|
| 247 | CalBddGen_t *gen = (CalBddGen_t *) gen_; |
---|
| 248 | pop_cube_stack(gen); |
---|
| 249 | if (gen->status == bdd_EMPTY) { |
---|
| 250 | return (FALSE); |
---|
| 251 | } |
---|
| 252 | *cube = gen->gen.cubes.cube; |
---|
| 253 | return (TRUE); |
---|
| 254 | } |
---|
| 255 | |
---|
| 256 | bdd_gen * |
---|
| 257 | bdd_first_disjoint_cube(bdd_t *fn,array_t **cube) |
---|
| 258 | { |
---|
| 259 | return(bdd_first_cube(fn,cube)); |
---|
| 260 | } |
---|
| 261 | |
---|
| 262 | boolean |
---|
| 263 | bdd_next_disjoint_cube(bdd_gen *gen_, array_t **cube) |
---|
| 264 | { |
---|
| 265 | return(bdd_next_cube(gen_,cube)); |
---|
| 266 | } |
---|
| 267 | |
---|
| 268 | /**Function******************************************************************** |
---|
| 269 | |
---|
| 270 | Synopsis [required] |
---|
| 271 | |
---|
| 272 | Description [bdd_first_node - enumerates all bdd_node in fn. |
---|
| 273 | Return the generator.] |
---|
| 274 | |
---|
| 275 | SideEffects [required] |
---|
| 276 | |
---|
| 277 | SeeAlso [optional] |
---|
| 278 | |
---|
| 279 | ******************************************************************************/ |
---|
| 280 | bdd_gen * |
---|
| 281 | bdd_first_node(bdd_t *fn, bdd_node **node) |
---|
| 282 | { |
---|
| 283 | Cal_BddManager_t *manager; |
---|
| 284 | CalBddGen_t *gen; |
---|
| 285 | long numVars; |
---|
| 286 | int i; |
---|
| 287 | Cal_Bdd_t calBdd; |
---|
| 288 | Cal_Bdd function; |
---|
| 289 | |
---|
| 290 | if (fn == NIL(bdd_t)) { |
---|
| 291 | CalBddFatalMessage("bdd_first_node: invalid BDD"); |
---|
| 292 | } |
---|
| 293 | |
---|
| 294 | manager = fn->bddManager; |
---|
| 295 | function = fn->calBdd; |
---|
| 296 | |
---|
| 297 | /* |
---|
| 298 | * Allocate a new generator structure and fill it in; the |
---|
| 299 | * visited table will be used, as will the stack, but the |
---|
| 300 | * cube array will not be used. |
---|
| 301 | */ |
---|
| 302 | gen = ALLOC(CalBddGen_t, 1); |
---|
| 303 | |
---|
| 304 | /* |
---|
| 305 | * first - init all the members to a rational value for node iteration. |
---|
| 306 | */ |
---|
| 307 | gen->manager = manager; |
---|
| 308 | gen->status = bdd_NONEMPTY; |
---|
| 309 | gen->type = bdd_gen_nodes; |
---|
| 310 | gen->gen.nodes.visited = NIL(st_table); |
---|
| 311 | gen->stack.sp = 0; |
---|
| 312 | gen->stack.nodeStack = NIL(CalBddNode_t *); |
---|
| 313 | gen->stack.idStack = NIL(int); |
---|
| 314 | gen->node = NIL(CalBddNode_t); |
---|
| 315 | |
---|
| 316 | /* |
---|
| 317 | * Set up the hash table for visited nodes. Every time we visit a node, |
---|
| 318 | * we insert it into the table. |
---|
| 319 | */ |
---|
| 320 | gen->gen.nodes.visited = st_init_table(st_ptrcmp, st_ptrhash); |
---|
| 321 | |
---|
| 322 | /* |
---|
| 323 | * The stack size will never exceed the number of variables in the BDD, since |
---|
| 324 | * the longest possible path from root to constant 1 is the number |
---|
| 325 | * of variables in the BDD. |
---|
| 326 | */ |
---|
| 327 | gen->stack.sp = 0; |
---|
| 328 | numVars = Cal_BddVars(manager); |
---|
| 329 | gen->stack.nodeStack = ALLOC(CalBddNode_t *, numVars); |
---|
| 330 | gen->stack.idStack = ALLOC(int, numVars); |
---|
| 331 | /* |
---|
| 332 | * Clear out the stack so that in bdd_gen_free, we can decrement the |
---|
| 333 | * ref count of those nodes still on the stack. |
---|
| 334 | */ |
---|
| 335 | for (i = 0; i < numVars; i++) { |
---|
| 336 | gen->stack.nodeStack[i] = NIL(CalBddNode_t); |
---|
| 337 | gen->stack.idStack[i] = -1; |
---|
| 338 | } |
---|
| 339 | |
---|
| 340 | /* |
---|
| 341 | * Get the first node. Get a new pointer to fn->node beforehand: |
---|
| 342 | * this increments |
---|
| 343 | * the reference count of fn->node; this is necessary, because when fn->node |
---|
| 344 | * is popped from the stack at the very end, it's ref count is decremented. |
---|
| 345 | */ |
---|
| 346 | calBdd = CalBddGetInternalBdd(manager, function); |
---|
| 347 | push_node_stack(calBdd, gen); |
---|
| 348 | gen->status = bdd_NONEMPTY; |
---|
| 349 | |
---|
| 350 | *node = (bdd_node *)gen->node; /* return the node */ |
---|
| 351 | return (bdd_gen *)(gen); /* and the new generator */ |
---|
| 352 | } |
---|
| 353 | |
---|
| 354 | /**Function******************************************************************** |
---|
| 355 | |
---|
| 356 | Synopsis [required] |
---|
| 357 | |
---|
| 358 | Description [bdd_next_node - get the next node in the BDD. |
---|
| 359 | Return {TRUE, FALSE} when {more, no more}. ] |
---|
| 360 | |
---|
| 361 | SideEffects [required] |
---|
| 362 | |
---|
| 363 | SeeAlso [optional] |
---|
| 364 | |
---|
| 365 | ******************************************************************************/ |
---|
| 366 | boolean |
---|
| 367 | bdd_next_node(bdd_gen *gen_,bdd_node **node) |
---|
| 368 | { |
---|
| 369 | CalBddGen_t *gen = (CalBddGen_t *) gen_; |
---|
| 370 | pop_node_stack(gen); |
---|
| 371 | if (gen->status == bdd_EMPTY) { |
---|
| 372 | return (FALSE); |
---|
| 373 | } |
---|
| 374 | *node = (bdd_node *) gen->node; |
---|
| 375 | return (TRUE); |
---|
| 376 | } |
---|
| 377 | |
---|
| 378 | /**Function******************************************************************** |
---|
| 379 | |
---|
| 380 | Synopsis [required] |
---|
| 381 | |
---|
| 382 | Description [bdd_gen_free - frees up the space used by the generator. |
---|
| 383 | Return an int so that it is easier to fit in a foreach macro. |
---|
| 384 | Return 0 (to make it easy to put in expressions). ] |
---|
| 385 | |
---|
| 386 | SideEffects [required] |
---|
| 387 | |
---|
| 388 | SeeAlso [optional] |
---|
| 389 | |
---|
| 390 | ******************************************************************************/ |
---|
| 391 | int |
---|
| 392 | bdd_gen_free(bdd_gen *gen_) |
---|
| 393 | { |
---|
| 394 | CalBddGen_t *gen = (CalBddGen_t *) gen_; |
---|
| 395 | st_table *visited_table; |
---|
| 396 | |
---|
| 397 | switch (gen->type) { |
---|
| 398 | case bdd_gen_cubes: |
---|
| 399 | array_free(gen->gen.cubes.cube); |
---|
| 400 | gen->gen.cubes.cube = NIL(array_t); |
---|
| 401 | break; |
---|
| 402 | case bdd_gen_nodes: |
---|
| 403 | visited_table = gen->gen.nodes.visited; |
---|
| 404 | st_free_table(visited_table); |
---|
| 405 | visited_table = NIL(st_table); |
---|
| 406 | break; |
---|
| 407 | } |
---|
| 408 | FREE(gen->stack.nodeStack); |
---|
| 409 | FREE(gen->stack.idStack); |
---|
| 410 | FREE(gen); |
---|
| 411 | return (0); /* make it return some sort of an int */ |
---|
| 412 | } |
---|
| 413 | |
---|
| 414 | /*---------------------------------------------------------------------------*/ |
---|
| 415 | /* Definition of exported functions */ |
---|
| 416 | /*---------------------------------------------------------------------------*/ |
---|
| 417 | /* |
---|
| 418 | * Invariants: |
---|
| 419 | * |
---|
| 420 | * gen->stack.stack contains nodes that remain to be explored. |
---|
| 421 | * |
---|
| 422 | * For a cube generator, |
---|
| 423 | * gen->gen.cubes.cube reflects the choices made to reach node |
---|
| 424 | * at top of the stack. |
---|
| 425 | * For a node generator, |
---|
| 426 | * gen->gen.nodes.visited reflects the nodes already visited in |
---|
| 427 | * the BDD dag. |
---|
| 428 | */ |
---|
| 429 | |
---|
| 430 | /**Function******************************************************************** |
---|
| 431 | |
---|
| 432 | Synopsis [required] |
---|
| 433 | |
---|
| 434 | Description [push_cube_stack - push a cube onto the stack to |
---|
| 435 | visit. Return nothing, just do it. |
---|
| 436 | The BDD is traversed using depth-first search, with the ELSE branch |
---|
| 437 | searched before the THEN branch. |
---|
| 438 | Caution: If you are creating new BDD's while iterating through the |
---|
| 439 | cubes, and a garbage collection happens to be performed during this |
---|
| 440 | process, then the BDD generator will get lost and an error will result. ] |
---|
| 441 | |
---|
| 442 | SideEffects [required] |
---|
| 443 | |
---|
| 444 | SeeAlso [optional] |
---|
| 445 | |
---|
| 446 | ******************************************************************************/ |
---|
| 447 | static void |
---|
| 448 | push_cube_stack(Cal_Bdd_t f, CalBddGen_t *gen) |
---|
| 449 | { |
---|
| 450 | bdd_variableId topId; |
---|
| 451 | Cal_Bdd_t f0, f1; |
---|
| 452 | Cal_BddManager_t *manager; |
---|
| 453 | |
---|
| 454 | manager = gen->manager; |
---|
| 455 | |
---|
| 456 | if (CalBddIsBddOne(manager, f)){ |
---|
| 457 | return; |
---|
| 458 | } |
---|
| 459 | |
---|
| 460 | topId = f.bddId-1; |
---|
| 461 | CalBddGetElseBdd(f, f0); |
---|
| 462 | CalBddGetThenBdd(f, f1); |
---|
| 463 | |
---|
| 464 | if (CalBddIsBddZero(manager, f1)){ |
---|
| 465 | /* |
---|
| 466 | * No choice: take the 0 branch. Since there is only one branch to |
---|
| 467 | * explore from f, there is no need to push f onto the stack, because |
---|
| 468 | * after exploring this branch we are done with f. A consequence of |
---|
| 469 | * this is that there will be no f to pop either. Same goes for the |
---|
| 470 | * next case. Decrement the ref count of f and of the branch leading |
---|
| 471 | * to zero, since we will no longer need to access these nodes. |
---|
| 472 | */ |
---|
| 473 | array_insert(bdd_literal, gen->gen.cubes.cube, topId, 0); |
---|
| 474 | push_cube_stack(f0, gen); |
---|
| 475 | } |
---|
| 476 | else if (CalBddIsBddZero(manager, f0)){ |
---|
| 477 | /* |
---|
| 478 | * No choice: take the 1 branch |
---|
| 479 | */ |
---|
| 480 | array_insert(bdd_literal, gen->gen.cubes.cube, topId, 1); |
---|
| 481 | push_cube_stack(f1, gen); |
---|
| 482 | } else { |
---|
| 483 | /* |
---|
| 484 | * In this case, we must explore both branches of f. We always choose |
---|
| 485 | * to explore the 0 branch first. We must push f on the stack, so that |
---|
| 486 | * we can later pop it and explore its 1 branch. Decrement the ref count |
---|
| 487 | * of f1 since we will no longer need to access this node. Note that |
---|
| 488 | * the parent of f1 was bdd_freed above or in pop_cube_stack. |
---|
| 489 | */ |
---|
| 490 | gen->stack.nodeStack[gen->stack.sp] = f.bddNode; |
---|
| 491 | gen->stack.idStack[gen->stack.sp++] = f.bddId; |
---|
| 492 | array_insert(bdd_literal, gen->gen.cubes.cube, topId, 0); |
---|
| 493 | push_cube_stack(f0, gen); |
---|
| 494 | } |
---|
| 495 | } |
---|
| 496 | |
---|
| 497 | /**Function******************************************************************** |
---|
| 498 | |
---|
| 499 | Synopsis [required] |
---|
| 500 | |
---|
| 501 | Description [optional] |
---|
| 502 | |
---|
| 503 | SideEffects [required] |
---|
| 504 | |
---|
| 505 | SeeAlso [optional] |
---|
| 506 | |
---|
| 507 | ******************************************************************************/ |
---|
| 508 | static void |
---|
| 509 | pop_cube_stack(CalBddGen_t *gen) |
---|
| 510 | { |
---|
| 511 | CalBddNode_t *fNode; |
---|
| 512 | int fId, fIndex, i; |
---|
| 513 | Cal_Bdd_t f1, f; |
---|
| 514 | Cal_BddManager_t *manager; |
---|
| 515 | |
---|
| 516 | manager = gen->manager; |
---|
| 517 | if (gen->stack.sp == 0) { |
---|
| 518 | /* |
---|
| 519 | * Stack is empty. Have already explored both the 0 and 1 branches of |
---|
| 520 | * the root of the BDD. |
---|
| 521 | */ |
---|
| 522 | gen->status = bdd_EMPTY; |
---|
| 523 | } else { |
---|
| 524 | /* |
---|
| 525 | * Explore the 1 branch of the node at the top of the stack (since it is |
---|
| 526 | * on the stack, this means we have already explored the 0 branch). We |
---|
| 527 | * permanently pop the top node, and bdd_free it, since there are |
---|
| 528 | * no more edges left to explore. |
---|
| 529 | */ |
---|
| 530 | fNode = gen->stack.nodeStack[--gen->stack.sp]; |
---|
| 531 | fId = gen->stack.idStack[gen->stack.sp]; |
---|
| 532 | gen->stack.nodeStack[gen->stack.sp] = NIL(CalBddNode_t); /* overwrite */ |
---|
| 533 | /* with NIL */ |
---|
| 534 | gen->stack.idStack[gen->stack.sp] = -1; |
---|
| 535 | array_insert(bdd_literal, gen->gen.cubes.cube, fId-1, 1); |
---|
| 536 | fIndex = manager->idToIndex[fId]; |
---|
| 537 | for (i = fIndex + 1; i < array_n(gen->gen.cubes.cube); i++) { |
---|
| 538 | array_insert(bdd_literal, gen->gen.cubes.cube, |
---|
| 539 | manager->indexToId[i]-1, 2); |
---|
| 540 | } |
---|
| 541 | f.bddNode = fNode; |
---|
| 542 | f.bddId = fId; |
---|
| 543 | CalBddGetThenBdd(f, f1); |
---|
| 544 | push_cube_stack(f1, gen); |
---|
| 545 | } |
---|
| 546 | } |
---|
| 547 | |
---|
| 548 | /**Function******************************************************************** |
---|
| 549 | |
---|
| 550 | Synopsis [required] |
---|
| 551 | |
---|
| 552 | Description [push_node_stack - push a node onto the stack. |
---|
| 553 | The same as push_cube_stack but for enumerating nodes instead of cubes. |
---|
| 554 | The BDD is traversed using depth-first search, with the ELSE branch |
---|
| 555 | searched before the THEN branch, and a node returned only after its |
---|
| 556 | children have been returned. Note that the returned bdd_node |
---|
| 557 | pointer has the complement bit zeroed out. |
---|
| 558 | Caution: If you are creating new BDD's while iterating through the |
---|
| 559 | nodes, and a garbage collection happens to be performed during this |
---|
| 560 | process, then the BDD generator will get lost and an error will result. ] |
---|
| 561 | |
---|
| 562 | SideEffects [required] |
---|
| 563 | |
---|
| 564 | SeeAlso [optional] |
---|
| 565 | |
---|
| 566 | ******************************************************************************/ |
---|
| 567 | static void |
---|
| 568 | push_node_stack(Cal_Bdd_t f, CalBddGen_t *gen) |
---|
| 569 | { |
---|
| 570 | Cal_Bdd_t f0, f1; |
---|
| 571 | bdd_node *reg_f, *reg_f0, *reg_f1; |
---|
| 572 | |
---|
| 573 | reg_f = (CalBddNode_t *) CAL_BDD_POINTER(f.bddNode); /* use of calInt.h */ |
---|
| 574 | if (st_is_member(gen->gen.nodes.visited, (char *) reg_f)){ |
---|
| 575 | /* |
---|
| 576 | * Already been visited. |
---|
| 577 | */ |
---|
| 578 | return; |
---|
| 579 | } |
---|
| 580 | |
---|
| 581 | if (CalBddIsBddConst(f)){ |
---|
| 582 | /* |
---|
| 583 | * If f is the constant node and it has not been visited yet, then |
---|
| 584 | * put it in the visited table and set the gen->node pointer. |
---|
| 585 | * There is no need to put it in the stack because |
---|
| 586 | * the constant node does not have any branches, and there is no |
---|
| 587 | * need to free f because constant nodes have a saturated |
---|
| 588 | * reference count. |
---|
| 589 | */ |
---|
| 590 | st_insert(gen->gen.nodes.visited, (char *) reg_f, NIL(char)); |
---|
| 591 | gen->node = (CalBddNode_t *) reg_f; |
---|
| 592 | } else { |
---|
| 593 | /* |
---|
| 594 | * f has not been marked as visited. We don't know yet if any of |
---|
| 595 | * its branches remain to be explored. First get its branches. |
---|
| 596 | */ |
---|
| 597 | CalBddGetElseBdd(f, f0); |
---|
| 598 | CalBddGetThenBdd(f, f1); |
---|
| 599 | |
---|
| 600 | reg_f0 = (CalBddNode_t *) CAL_BDD_POINTER(f0.bddNode); |
---|
| 601 | reg_f1 = (CalBddNode_t *) CAL_BDD_POINTER(f1.bddNode); |
---|
| 602 | |
---|
| 603 | if (st_is_member(gen->gen.nodes.visited, (char *) reg_f0) == 0){ |
---|
| 604 | /* |
---|
| 605 | * The 0 child has not been visited, so explore the 0 branch. |
---|
| 606 | * First push f on the stack. Bdd_free f1 since we will not |
---|
| 607 | * need to access this exact pointer any more. |
---|
| 608 | */ |
---|
| 609 | gen->stack.nodeStack[gen->stack.sp] = f.bddNode; |
---|
| 610 | gen->stack.idStack[gen->stack.sp++] = f.bddId; |
---|
| 611 | push_node_stack(f0, gen); |
---|
| 612 | } else{ |
---|
| 613 | if (st_is_member(gen->gen.nodes.visited, (char *) reg_f1) == 0){ |
---|
| 614 | /* |
---|
| 615 | * The 0 child has been visited, but the 1 child has not been |
---|
| 616 | * visited, so explore the 1 branch. First push f on the |
---|
| 617 | * stack. |
---|
| 618 | */ |
---|
| 619 | gen->stack.nodeStack[gen->stack.sp] = f.bddNode; |
---|
| 620 | gen->stack.idStack[gen->stack.sp++] = f.bddId; |
---|
| 621 | push_node_stack(f1, gen); |
---|
| 622 | } else { |
---|
| 623 | /* |
---|
| 624 | * Both the 0 and 1 children have been visited. Thus we are done |
---|
| 625 | * exploring from f. |
---|
| 626 | * Mark f as visited (put it in the visited table), and set the |
---|
| 627 | * gen->node pointer. |
---|
| 628 | */ |
---|
| 629 | st_insert(gen->gen.nodes.visited, (char *) reg_f, NIL(char)); |
---|
| 630 | gen->node = (CalBddNode_t *) reg_f; |
---|
| 631 | } |
---|
| 632 | } |
---|
| 633 | } |
---|
| 634 | } |
---|
| 635 | |
---|
| 636 | /**Function******************************************************************** |
---|
| 637 | |
---|
| 638 | Synopsis [required] |
---|
| 639 | |
---|
| 640 | Description [optional] |
---|
| 641 | |
---|
| 642 | SideEffects [required] |
---|
| 643 | |
---|
| 644 | SeeAlso [optional] |
---|
| 645 | |
---|
| 646 | ******************************************************************************/ |
---|
| 647 | |
---|
| 648 | static void |
---|
| 649 | pop_node_stack(CalBddGen_t *gen) |
---|
| 650 | { |
---|
| 651 | CalBddNode_t *fNode; |
---|
| 652 | int fId; |
---|
| 653 | Cal_Bdd_t calBdd; |
---|
| 654 | |
---|
| 655 | if (gen->stack.sp == 0) { |
---|
| 656 | gen->status = bdd_EMPTY; |
---|
| 657 | return; |
---|
| 658 | } |
---|
| 659 | fNode = gen->stack.nodeStack[--gen->stack.sp]; |
---|
| 660 | fId = gen->stack.idStack[gen->stack.sp]; |
---|
| 661 | gen->stack.nodeStack[gen->stack.sp] = NIL(CalBddNode_t); |
---|
| 662 | gen->stack.idStack[gen->stack.sp] = -1; |
---|
| 663 | calBdd.bddNode = fNode; |
---|
| 664 | calBdd.bddId = fId; |
---|
| 665 | push_node_stack(calBdd, gen); |
---|
| 666 | } |
---|
| 667 | |
---|