Method performDeepSoILocalSearch

src/engine/Engine.cpp:3009–3125

}

bool Engine::performDeepSoILocalSearch()
{
    ENGINE_LOG( "Performing local search..." );
    struct timespec start = TimeUtils::sampleMicro();
    ASSERT( allVarsWithinBounds() );

    // All the linear constraints have been satisfied at this point.
    // Update the cost function
    _soiManager->initializePhasePattern();

    LinearExpression initialPhasePattern = _soiManager->getCurrentSoIPhasePattern();

    if ( initialPhasePattern.isZero() )
    {
        if ( hasBranchingCandidate() )
            while ( !_smtCore.needToSplit() )
                _smtCore.reportRejectedPhasePatternProposal();
        return false;
    }

    minimizeHeuristicCost( initialPhasePattern );
    ASSERT( allVarsWithinBounds() );
    _soiManager->updateCurrentPhasePatternForSatisfiedPLConstraints();
    // Always accept the first phase pattern.
    _soiManager->acceptCurrentPhasePattern();
    double costOfLastAcceptedPhasePattern =
        computeHeuristicCost( _soiManager->getCurrentSoIPhasePattern() );

    double costOfProposedPhasePattern = FloatUtils::infinity();
    bool lastProposalAccepted = true;
    while ( !_smtCore.needToSplit() )
    {
        struct timespec end = TimeUtils::sampleMicro();
        _statistics.incLongAttribute( Statistics::TOTAL_TIME_LOCAL_SEARCH_MICRO,
                                      TimeUtils::timePassed( start, end ) );
        start = end;

        if ( lastProposalAccepted )
        {
            /*
              Check whether the optimal solution to the last accepted phase
              is a real solution. We only check this when the last proposal
              was accepted, because rejected phase pattern must have resulted in
              increase in the SoI cost.

              HW: Another option is to only do this check when
              costOfLastAcceptedPhasePattern is 0, but this might be too strict.
              The overhead is low anyway.
            */
            collectViolatedPlConstraints();
            if ( allPlConstraintsHold() )
            {
                if ( _lpSolverType == LPSolverType::NATIVE &&
                     _tableau->getBasicAssignmentStatus() !=
                         ITableau::BASIC_ASSIGNMENT_JUST_COMPUTED )
                {
                    if ( _verbosity > 0 )
                    {