Method constructSignLayer

src/engine/InputQuery.cpp:1502–1598

}

bool InputQuery::constructSignLayer( NLR::NetworkLevelReasoner *nlr,
                                     Map<unsigned, unsigned> &handledVariableToLayer,
                                     unsigned newLayerIndex,
                                     Set<PiecewiseLinearConstraint *> &handledPLConstraints )
{
    INPUT_QUERY_LOG( "Attempting to construct SignLayer..." );
    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 Signs where the b variables have already been handled
    const List<PiecewiseLinearConstraint *> &plConstraints = getPiecewiseLinearConstraints();

    unsigned currentSourceLayer = 0;
    for ( const auto &plc : plConstraints )
    {
        if ( handledPLConstraints.exists( plc ) )
            continue;

        // Only consider Signs
        if ( plc->getType() != SIGN )
            continue;

        const SignConstraint *sign = (const SignConstraint *)plc;

        // Has the b variable been handled?
        unsigned b = sign->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 = sign->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 ) );
        nlr->addConstraintInTopologicalOrder( plc );
        handledPLConstraints.insert( plc );
    }