Method constructRoundLayer

src/engine/InputQuery.cpp:1208–1303

}

bool InputQuery::constructRoundLayer( NLR::NetworkLevelReasoner *nlr,
                                      Map<unsigned, unsigned> &handledVariableToLayer,
                                      unsigned newLayerIndex,
                                      Set<NonlinearConstraint *> &handledNLConstraints )
{
    INPUT_QUERY_LOG( "Attempting to construct RoundLayer..." );
    struct NeuronInformation
    {
    public:
        NeuronInformation( unsigned variable, unsigned neuron, unsigned sourceVariable )
            : _variable( variable )
            , _neuron( neuron )
            , _sourceVariable( sourceVariable )
        {
        }

        unsigned _variable;
        unsigned _neuron;
        unsigned _sourceVariable;
    };

    List<NeuronInformation> newNeurons;

    // Look for ReLUs where all b variables have already been handled
    const List<NonlinearConstraint *> &nlConstraints = getNonlinearConstraints();

    unsigned currentSourceLayer = 0;
    for ( const auto &nlc : nlConstraints )
    {
        if ( handledNLConstraints.exists( nlc ) )
            continue;

        // Only consider Rounds
        if ( nlc->getType() != ROUND )
            continue;

        const RoundConstraint *round = (const RoundConstraint *)nlc;

        // Has the b variable been handled?
        unsigned b = round->getB();
        if ( !handledVariableToLayer.exists( b ) ||
             ( _ensureSameSourceLayerInNLR && !newNeurons.empty() &&
               handledVariableToLayer[b] != currentSourceLayer ) )
            continue;

        // If the f variable has also been handled, ignore this constraint
        unsigned f = round->getF();
        if ( handledVariableToLayer.exists( f ) )
            continue;

        // B has been handled, f hasn't. Add f
        if ( _ensureSameSourceLayerInNLR && newNeurons.empty() )
            currentSourceLayer = handledVariableToLayer[b];
        newNeurons.append( NeuronInformation( f, newNeurons.size(), b ) );
        handledNLConstraints.insert( nlc );
    }

    // No neurons found for the new layer