| 707 | } |
| 708 | |
| 709 | void Preprocessor::eliminateVariables() |
| 710 | { |
| 711 | // If there's nothing to eliminate, we just eliminate obsolete constraints. |
| 712 | if ( _fixedVariables.empty() && _mergedVariables.empty() ) |
| 713 | { |
| 714 | List<PiecewiseLinearConstraint *> &constraints( |
| 715 | _preprocessed->getPiecewiseLinearConstraints() ); |
| 716 | List<PiecewiseLinearConstraint *>::iterator constraint = constraints.begin(); |
| 717 | while ( constraint != constraints.end() ) |
| 718 | { |
| 719 | if ( ( *constraint )->constraintObsolete() ) |
| 720 | { |
| 721 | if ( _statistics ) |
| 722 | _statistics->incUnsignedAttribute( Statistics::PP_NUM_CONSTRAINTS_REMOVED ); |
| 723 | |
| 724 | if ( _preprocessed->_networkLevelReasoner ) |
| 725 | _preprocessed->_networkLevelReasoner->removeConstraintFromTopologicalOrder( |
| 726 | *constraint ); |
| 727 | delete *constraint; |
| 728 | *constraint = NULL; |
| 729 | constraint = constraints.erase( constraint ); |
| 730 | } |
| 731 | else |
| 732 | ++constraint; |
| 733 | } |
| 734 | |
| 735 | List<NonlinearConstraint *> &nlConstraints( _preprocessed->getNonlinearConstraints() ); |
| 736 | List<NonlinearConstraint *>::iterator nlConstraint = nlConstraints.begin(); |
| 737 | while ( nlConstraint != nlConstraints.end() ) |
| 738 | { |
| 739 | if ( ( *nlConstraint )->constraintObsolete() ) |
| 740 | { |
| 741 | if ( _statistics ) |
| 742 | _statistics->incUnsignedAttribute( Statistics::PP_NUM_CONSTRAINTS_REMOVED ); |
| 743 | |
| 744 | delete *nlConstraint; |
| 745 | *nlConstraint = NULL; |
| 746 | nlConstraint = nlConstraints.erase( nlConstraint ); |
| 747 | } |
| 748 | else |
| 749 | ++nlConstraint; |
| 750 | } |
| 751 | return; |
| 752 | } |
| 753 | |
| 754 | if ( _statistics ) |
| 755 | _statistics->setUnsignedAttribute( Statistics::PP_NUM_ELIMINATED_VARS, |
| 756 | _fixedVariables.size() + _mergedVariables.size() ); |
| 757 | |
| 758 | // Check and remove any fixed variables from the debugging solution |
| 759 | for ( unsigned i = 0; i < _preprocessed->getNumberOfVariables(); ++i ) |
| 760 | { |
| 761 | if ( _fixedVariables.exists( i ) && _preprocessed->_debuggingSolution.exists( i ) ) |
| 762 | { |
| 763 | if ( !FloatUtils::areEqual( _fixedVariables[i], _preprocessed->_debuggingSolution[i] ) ) |
| 764 | throw MarabouError( MarabouError::DEBUGGING_ERROR, |
| 765 | Stringf( "Variable %u fixed to %.5lf, " |
| 766 | "contradicts possible solution %.5lf", |
nothing calls this directly
no test coverage detected