| 535 | |
| 536 | |
| 537 | const Choice* |
| 538 | Space::choice(void) { |
| 539 | if (!stable()) |
| 540 | throw SpaceNotStable("Space::choice"); |
| 541 | if (failed() || (b_status == Brancher::cast(&bl))) { |
| 542 | // There are no more choices to be generated |
| 543 | // Delete all branchers |
| 544 | Brancher* b = Brancher::cast(bl.next()); |
| 545 | while (b != Brancher::cast(&bl)) { |
| 546 | Brancher* d = b; |
| 547 | b = Brancher::cast(b->next()); |
| 548 | rfree(d,d->dispose(*this)); |
| 549 | } |
| 550 | bl.init(); |
| 551 | b_status = b_commit = Brancher::cast(&bl); |
| 552 | return nullptr; |
| 553 | } |
| 554 | /* |
| 555 | * The call to choice() says that no older choices |
| 556 | * can be used. Hence, all branchers that are exhausted can be deleted. |
| 557 | */ |
| 558 | Brancher* b = Brancher::cast(bl.next()); |
| 559 | while (b != b_status) { |
| 560 | Brancher* d = b; |
| 561 | b = Brancher::cast(b->next()); |
| 562 | d->unlink(); |
| 563 | rfree(d,d->dispose(*this)); |
| 564 | } |
| 565 | // Make sure that b_commit does not point to a deleted brancher! |
| 566 | b_commit = b_status; |
| 567 | return b_status->choice(*this); |
| 568 | } |
| 569 | |
| 570 | const Choice* |
| 571 | Space::choice(Archive& e) const { |