| 647 | } |
| 648 | |
| 649 | void MaxConstraint::eliminateCase( unsigned variable ) |
| 650 | { |
| 651 | bool proofs = _boundManager && _boundManager->shouldProduceProofs(); |
| 652 | |
| 653 | // Function is not yet supported for proof production |
| 654 | if ( proofs ) |
| 655 | return; |
| 656 | |
| 657 | if ( _cdInfeasibleCases ) |
| 658 | { |
| 659 | markInfeasible( variableToPhase( variable ) ); |
| 660 | } |
| 661 | else |
| 662 | { |
| 663 | _elements.erase( variable ); |
| 664 | _eliminatedElements.insert( variable ); |
| 665 | |
| 666 | if ( _elementToAux.exists( variable ) ) |
| 667 | { |
| 668 | unsigned aux = _elementToAux[variable]; |
| 669 | _elementToAux.erase( variable ); |
| 670 | _auxToElement.erase( aux ); |
| 671 | } |
| 672 | if ( proofs ) |
| 673 | { |
| 674 | if ( _elementToTighteningRow.exists( variable ) && |
| 675 | _elementToTighteningRow[variable] != NULL ) |
| 676 | { |
| 677 | _elementToTighteningRow[variable] = NULL; |
| 678 | _elementToTighteningRow.erase( variable ); |
| 679 | } |
| 680 | |
| 681 | if ( _elementToTableauAux.exists( variable ) ) |
| 682 | _elementToTableauAux.erase( variable ); |
| 683 | } |
| 684 | } |
| 685 | } |
| 686 | |
| 687 | bool MaxConstraint::haveOutOfBoundVariables() const |
| 688 | { |
nothing calls this directly
no test coverage detected