| 3339 | } |
| 3340 | |
| 3341 | void Engine::explainSimplexFailure() |
| 3342 | { |
| 3343 | ASSERT( _produceUNSATProofs ); |
| 3344 | |
| 3345 | DEBUG( checkGroundBounds() ); |
| 3346 | |
| 3347 | unsigned infeasibleVar = _boundManager.getInconsistentVariable(); |
| 3348 | |
| 3349 | if ( infeasibleVar == IBoundManager::NO_VARIABLE_FOUND || |
| 3350 | !certifyInfeasibility( infeasibleVar ) ) |
| 3351 | infeasibleVar = explainFailureWithTableau(); |
| 3352 | |
| 3353 | if ( infeasibleVar == IBoundManager::NO_VARIABLE_FOUND ) |
| 3354 | infeasibleVar = explainFailureWithCostFunction(); |
| 3355 | |
| 3356 | if ( infeasibleVar == IBoundManager::NO_VARIABLE_FOUND ) |
| 3357 | { |
| 3358 | _costFunctionManager->computeCoreCostFunction(); |
| 3359 | infeasibleVar = explainFailureWithCostFunction(); |
| 3360 | } |
| 3361 | |
| 3362 | if ( infeasibleVar == IBoundManager::NO_VARIABLE_FOUND ) |
| 3363 | { |
| 3364 | markLeafToDelegate(); |
| 3365 | return; |
| 3366 | } |
| 3367 | |
| 3368 | ASSERT( infeasibleVar < _tableau->getN() ); |
| 3369 | ASSERT( _UNSATCertificateCurrentPointer && |
| 3370 | !( **_UNSATCertificateCurrentPointer ).getContradiction() ); |
| 3371 | _statistics.incUnsignedAttribute( Statistics::NUM_CERTIFIED_LEAVES ); |
| 3372 | |
| 3373 | writeContradictionToCertificate( infeasibleVar ); |
| 3374 | |
| 3375 | ( **_UNSATCertificateCurrentPointer ).makeLeaf(); |
| 3376 | } |
| 3377 | |
| 3378 | bool Engine::certifyInfeasibility( unsigned var ) const |
| 3379 | { |
no test coverage detected