Method constructNetworkLevelReasoner

src/engine/InputQuery.cpp:733–852

}

bool InputQuery::constructNetworkLevelReasoner( List<Equation> &unhandledEquations,
                                                Set<unsigned> &varsInUnhandledConstraints )
{
    INPUT_QUERY_LOG( "PP: constructing an NLR... " );

    if ( _networkLevelReasoner )
        delete _networkLevelReasoner;
    NLR::NetworkLevelReasoner *nlr = new NLR::NetworkLevelReasoner;

    Map<unsigned, unsigned> handledVariableToLayer;

    // First, put all the input neurons in layer 0
    List<unsigned> inputs = getInputVariables();
    // If there is no input variable, don't construct the nlr
    if ( inputs.empty() )
    {
        INPUT_QUERY_LOG( "unsuccessful\n" );
        delete nlr;
        return false;
    }

    nlr->addLayer( 0, NLR::Layer::INPUT, inputs.size() );
    unsigned index = 0;

    NLR::Layer *inputLayer = nlr->getLayer( 0 );
    for ( const auto &inputVariable : inputs )
    {
        nlr->setNeuronVariable( NLR::NeuronIndex( 0, index ), inputVariable );
        handledVariableToLayer[inputVariable] = 0;

        inputLayer->setLb( index,
                           _lowerBounds.exists( inputVariable ) ? _lowerBounds[inputVariable]
                                                                : FloatUtils::negativeInfinity() );
        inputLayer->setUb( index,
                           _upperBounds.exists( inputVariable ) ? _upperBounds[inputVariable]
                                                                : FloatUtils::infinity() );

        ++index;
    }

    unsigned newLayerIndex = 1;
    Set<unsigned> handledEquations;
    Set<PiecewiseLinearConstraint *> handledPLConstraints;
    Set<NonlinearConstraint *> handledNLConstraints;
    // Now, repeatedly attempt to construct additional layers
    while (
        constructWeighedSumLayer( nlr, handledVariableToLayer, newLayerIndex, handledEquations ) ||
        constructReluLayer( nlr, handledVariableToLayer, newLayerIndex, handledPLConstraints ) ||
        constructRoundLayer( nlr, handledVariableToLayer, newLayerIndex, handledNLConstraints ) ||
        constructLeakyReluLayer(
            nlr, handledVariableToLayer, newLayerIndex, handledPLConstraints ) ||
        constructAbsoluteValueLayer(
            nlr, handledVariableToLayer, newLayerIndex, handledPLConstraints ) ||
        constructSignLayer( nlr, handledVariableToLayer, newLayerIndex, handledPLConstraints ) ||
        constructSigmoidLayer( nlr, handledVariableToLayer, newLayerIndex, handledNLConstraints ) ||
        constructMaxLayer( nlr, handledVariableToLayer, newLayerIndex, handledPLConstraints ) ||
        constructBilinearLayer(
            nlr, handledVariableToLayer, newLayerIndex, handledNLConstraints ) ||