Method explainFailureWithTableau

src/engine/Engine.cpp:3494–3525

}

unsigned Engine::explainFailureWithTableau()
{
    ASSERT( _produceUNSATProofs );

    // Failure of a simplex step implies infeasible bounds imposed by the row
    TableauRow boundUpdateRow = TableauRow( _tableau->getN() );

    //  For every basic, check that is has no slack and its explanations indeed prove a
    //  contradiction
    unsigned basicVar;

    for ( unsigned i = 0; i < _tableau->getM(); ++i )
    {
        if ( _tableau->basicOutOfBounds( i ) )
        {
            _tableau->getTableauRow( i, &boundUpdateRow );
            basicVar = boundUpdateRow._lhs;

            if ( FloatUtils::gt( _boundManager.computeRowBound( boundUpdateRow, Tightening::LB ),
                                 _boundManager.getUpperBound( basicVar ) ) &&
                 explainAndCheckContradiction( basicVar, Tightening::LB, &boundUpdateRow ) )
                return basicVar;

            if ( FloatUtils::lt( _boundManager.computeRowBound( boundUpdateRow, Tightening::UB ),
                                 _boundManager.getLowerBound( basicVar ) ) &&
                 explainAndCheckContradiction( basicVar, Tightening::UB, &boundUpdateRow ) )
                return basicVar;
        }
    }

    return IBoundManager::NO_VARIABLE_FOUND;
}

unsigned Engine::explainFailureWithCostFunction()
{