Method pickSplitPLConstraint

src/engine/Engine.cpp:2820–2857

}

PiecewiseLinearConstraint *Engine::pickSplitPLConstraint( DivideStrategy strategy )
{
    ENGINE_LOG( Stringf( "Picking a split PLConstraint..." ).ascii() );

    PiecewiseLinearConstraint *candidatePLConstraint = NULL;
    if ( strategy == DivideStrategy::PseudoImpact )
    {
        if ( _smtCore.getStackDepth() > 3 )
            candidatePLConstraint = _smtCore.getConstraintsWithHighestScore();
        else if ( !_preprocessedQuery->getInputVariables().empty() &&
                  _preprocessedQuery->getInputVariables().size() <
                      GlobalConfiguration::INTERVAL_SPLITTING_THRESHOLD )
            candidatePLConstraint = pickSplitPLConstraintBasedOnIntervalWidth();
        else
        {
            candidatePLConstraint = pickSplitPLConstraintBasedOnPolarity();
            if ( candidatePLConstraint == NULL )
                candidatePLConstraint = _smtCore.getConstraintsWithHighestScore();
        }
    }
    else if ( strategy == DivideStrategy::Polarity )
        candidatePLConstraint = pickSplitPLConstraintBasedOnPolarity();
    else if ( strategy == DivideStrategy::EarliestReLU )
        candidatePLConstraint = pickSplitPLConstraintBasedOnTopology();
    else if ( strategy == DivideStrategy::LargestInterval &&
              ( ( _smtCore.getStackDepth() + 1 ) %
                    GlobalConfiguration::INTERVAL_SPLITTING_FREQUENCY !=
                0 ) )
    {
        // Conduct interval splitting periodically.
        candidatePLConstraint = pickSplitPLConstraintBasedOnIntervalWidth();
    }
    ENGINE_LOG(
        Stringf( ( candidatePLConstraint ? "Picked..."
                                         : "Unable to pick using the current strategy..." ) )
            .ascii() );
    return candidatePLConstraint;
}

PiecewiseLinearConstraint *Engine::pickSplitPLConstraintSnC( SnCDivideStrategy strategy )
{