Method transformToUseAuxVariables

src/engine/MaxConstraint.cpp:543–589

}

void MaxConstraint::transformToUseAuxVariables( InputQuery &inputQuery )
{
    if ( _auxToElement.size() > 0 )
        return;

    bool fInInput = false;
    for ( const auto &element : _elements )
    {
        // If element is equal to _f, skip this step.
        // The reason is to avoid adding equations like `1.00x00 -1.00x00 -1.00x01 = 0.00`.
        if ( element == _f )
        {
            fInInput = true;
            continue;
        }
        // Create an aux variable
        unsigned auxVariable = inputQuery.getNumberOfVariables();
        inputQuery.setNumberOfVariables( auxVariable + 1 );

        // f >= element, or f - element - aux = 0, for non-negative aux
        Equation equation( Equation::EQ );
        equation.addAddend( 1.0, _f );
        equation.addAddend( -1.0, element );
        equation.addAddend( -1.0, auxVariable );
        equation.setScalar( 0 );
        inputQuery.addEquation( equation );

        // Set the bounds for the aux variable
        inputQuery.setLowerBound( auxVariable, 0 );

        _elementToAux[element] = auxVariable;
        _auxToElement[auxVariable] = element;
    }
    if ( fInInput )
    {
        List<unsigned> toRemove;
        for ( const auto &element : _elements )
        {
            if ( element == _f )
                continue;
            toRemove.append( element );
        }
        for ( const auto &element : toRemove )
            eliminateCase( element );
        _obsolete = true;
    }
}

void MaxConstraint::getCostFunctionComponent( LinearExpression &cost, PhaseStatus phase ) const
{