| 345 | } |
| 346 | |
| 347 | bool MaxConstraint::satisfied() const |
| 348 | { |
| 349 | DEBUG( { |
| 350 | if ( !( existsAssignment( _f ) ) ) |
| 351 | throw MarabouError( MarabouError::PARTICIPATING_VARIABLE_MISSING_ASSIGNMENT, |
| 352 | Stringf( "f(x%u) assignment missing.", _f ).ascii() ); |
| 353 | for ( const auto &element : _elements ) |
| 354 | if ( !( existsAssignment( element ) ) ) |
| 355 | throw MarabouError( MarabouError::PARTICIPATING_VARIABLE_MISSING_ASSIGNMENT, |
| 356 | Stringf( "input(x%u) assignment missing.", element ).ascii() ); |
| 357 | } ); |
| 358 | |
| 359 | double fValue = getAssignment( _f ); |
| 360 | double maxValue = _maxValueOfEliminatedPhases; |
| 361 | for ( const auto &element : _elements ) |
| 362 | { |
| 363 | double currentValue = getAssignment( element ); |
| 364 | if ( FloatUtils::gt( currentValue, maxValue ) ) |
| 365 | maxValue = currentValue; |
| 366 | } |
| 367 | return FloatUtils::areEqual( maxValue, fValue ); |
| 368 | } |
| 369 | |
| 370 | bool MaxConstraint::isCaseInfeasible( unsigned variable ) const |
| 371 | { |
no test coverage detected