Method performSimplexStep

src/engine/Engine.cpp:627–826

}

bool Engine::performSimplexStep()
{
    // Statistics
    _statistics.incLongAttribute( Statistics::NUM_SIMPLEX_STEPS );
    struct timespec start = TimeUtils::sampleMicro();

    /*
      In order to increase numerical stability, we attempt to pick a
      "good" entering/leaving combination, by trying to avoid tiny pivot
      values. We do this as follows:

      1. Pick an entering variable according to the strategy in use.
      2. Find the entailed leaving variable.
      3. If the combination is bad, go back to (1) and find the
         next-best entering variable.
    */

    if ( _tableau->isOptimizing() )
        _costFunctionManager->computeGivenCostFunction( _heuristicCost._addends );
    if ( _costFunctionManager->costFunctionInvalid() )
        _costFunctionManager->computeCoreCostFunction();
    else
        _costFunctionManager->adjustBasicCostAccuracy();

    DEBUG( {
        // Since we're performing a simplex step, there are out-of-bounds variables.
        // Therefore, if the cost function is fresh, it should not be zero.
        if ( _costFunctionManager->costFunctionJustComputed() )
        {
            const double *costFunction = _costFunctionManager->getCostFunction();
            unsigned size = _tableau->getN() - _tableau->getM();
            bool found = false;
            for ( unsigned i = 0; i < size; ++i )
            {
                if ( !FloatUtils::isZero( costFunction[i] ) )
                {
                    found = true;
                    break;
                }
            }

            if ( !found )
            {
                printf( "Error! Have OOB vars but cost function is zero.\n"
                        "Recomputing cost function. New one is:\n" );
                _costFunctionManager->computeCoreCostFunction();
                _costFunctionManager->dumpCostFunction();
                throw MarabouError( MarabouError::DEBUGGING_ERROR,
                                    "Have OOB vars but cost function is zero" );
            }
        }
    } );

    // Obtain all eligible entering variables
    List<unsigned> enteringVariableCandidates;
    _tableau->getEntryCandidates( enteringVariableCandidates );

    unsigned bestLeaving = 0;