Method explainAndCheckContradiction

src/engine/Engine.cpp:3570–3587

}

bool Engine::explainAndCheckContradiction( unsigned var, bool isUpper, const TableauRow *row )
{
    ASSERT( _produceUNSATProofs );

    SparseUnsortedList backup( 0 );
    backup = _boundManager.getExplanation( var, isUpper );

    _boundManager.updateBoundExplanation( *row, isUpper, var );

    // Ensure the proof is correct
    if ( certifyInfeasibility( var ) )
        return true;

    // If not, restores previous certificate if the proof is wrong
    _boundManager.setExplanation( backup, var, isUpper );

    return false;
}

bool Engine::explainAndCheckContradiction( unsigned var,
                                           bool isUpper,