| 3525 | } |
| 3526 | |
| 3527 | unsigned Engine::explainFailureWithCostFunction() |
| 3528 | { |
| 3529 | ASSERT( _produceUNSATProofs ); |
| 3530 | |
| 3531 | // Failure of a simplex step might imply infeasible bounds imposed by the cost function |
| 3532 | unsigned curBasicVar; |
| 3533 | unsigned infVar = IBoundManager::NO_VARIABLE_FOUND; |
| 3534 | double curCost; |
| 3535 | bool curUpper; |
| 3536 | const SparseUnsortedList *costRow = _costFunctionManager->createRowOfCostFunction(); |
| 3537 | |
| 3538 | for ( unsigned i = 0; i < _tableau->getM(); ++i ) |
| 3539 | { |
| 3540 | curBasicVar = _tableau->basicIndexToVariable( i ); |
| 3541 | curCost = _costFunctionManager->getBasicCost( i ); |
| 3542 | |
| 3543 | if ( FloatUtils::isZero( curCost ) ) |
| 3544 | continue; |
| 3545 | |
| 3546 | curUpper = ( curCost < 0 ); |
| 3547 | |
| 3548 | // Check the basic variable has no slack |
| 3549 | if ( !( !curUpper && FloatUtils::gt( _boundManager.computeSparseRowBound( |
| 3550 | *costRow, Tightening::LB, curBasicVar ), |
| 3551 | _boundManager.getUpperBound( curBasicVar ) ) ) && |
| 3552 | !( curUpper && FloatUtils::lt( _boundManager.computeSparseRowBound( |
| 3553 | *costRow, Tightening::UB, curBasicVar ), |
| 3554 | _boundManager.getLowerBound( curBasicVar ) ) ) ) |
| 3555 | |
| 3556 | continue; |
| 3557 | |
| 3558 | // Check the explanation indeed proves a contradiction |
| 3559 | if ( explainAndCheckContradiction( curBasicVar, curUpper, costRow ) ) |
| 3560 | { |
| 3561 | infVar = curBasicVar; |
| 3562 | break; |
| 3563 | } |
| 3564 | } |
| 3565 | |
| 3566 | delete costRow; |
| 3567 | return infVar; |
| 3568 | } |
| 3569 | |
| 3570 | bool Engine::explainAndCheckContradiction( unsigned var, bool isUpper, const TableauRow *row ) |
| 3571 | { |
nothing calls this directly
no test coverage detected