Method generateQuery

src/input_parsers/BerkeleyParser.cpp:27–89

}

void BerkeleyParser::generateQuery( InputQuery &inputQuery )
{
    _berkeleyNeuralNetwork.parseFile();

    // The total number of variables required for the encoding is computed as follows:
    //   1. One for every variable that's part of the query

    unsigned numberOfVariables = _berkeleyNeuralNetwork.getNumVariables();

    printf( "Total number of Marabou variables: %u\n", numberOfVariables );

    inputQuery.setNumberOfVariables( numberOfVariables );

    // Set bounds for inputs. Currently just [0,1]
    Set<unsigned> inputVariables = _berkeleyNeuralNetwork.getInputVariables();
    for ( const auto &it : inputVariables )
    {
        double min = 0.0;
        double max = 1.0;

        inputQuery.setLowerBound( it, min );
        inputQuery.setUpperBound( it, max );
    }

    // Declare relu pairs and set bounds
    Map<unsigned, unsigned> fToB = _berkeleyNeuralNetwork.getFToB();
    for ( const auto &it : fToB )
    {
        unsigned f = it.first;
        unsigned b = it.second;

        PiecewiseLinearConstraint *relu = new ReluConstraint( b, f );
        inputQuery.addPiecewiseLinearConstraint( relu );

        inputQuery.setLowerBound( f, 0.0 );
        inputQuery.setUpperBound( f, FloatUtils::infinity() );

        inputQuery.setLowerBound( b, FloatUtils::negativeInfinity() );
        inputQuery.setUpperBound( b, FloatUtils::infinity() );
    }

    // Create the equations
    List<BerkeleyNeuralNetwork::Equation> equations = _berkeleyNeuralNetwork.getEquations();
    for ( const auto &berkeleyEquation : equations )
    {
        Equation marabouEquation;

        // The Berkeley equation is of the form y = x1 + x2 + x3 + c.
        // The Marabou equation is of the form y - x1 - x2 - x3 = c.
        unsigned lhs = berkeleyEquation._lhs;
        marabouEquation.addAddend( 1.0, lhs );

        for ( const auto &rhs : berkeleyEquation._rhs )
        {
            unsigned var = rhs._var;
            double coefficient = rhs._coefficient;
            marabouEquation.addAddend( -coefficient, var );
        }