| 28 | } |
| 29 | |
| 30 | void MILPEncoder::encodeInputQuery( GurobiWrapper &gurobi, |
| 31 | const InputQuery &inputQuery, |
| 32 | bool relax ) |
| 33 | { |
| 34 | struct timespec start = TimeUtils::sampleMicro(); |
| 35 | |
| 36 | gurobi.reset(); |
| 37 | // Add variables |
| 38 | for ( unsigned var = 0; var < inputQuery.getNumberOfVariables(); var++ ) |
| 39 | { |
| 40 | double lb = _tableau.getLowerBound( var ); |
| 41 | double ub = _tableau.getUpperBound( var ); |
| 42 | String varName = Stringf( "x%u", var ); |
| 43 | gurobi.addVariable( varName, lb, ub ); |
| 44 | _variableToVariableName[var] = varName; |
| 45 | } |
| 46 | |
| 47 | // Add equations |
| 48 | for ( const auto &equation : inputQuery.getEquations() ) |
| 49 | { |
| 50 | encodeEquation( gurobi, equation ); |
| 51 | } |
| 52 | |
| 53 | // Add Piecewise-linear Constraints |
| 54 | for ( const auto &plConstraint : inputQuery.getPiecewiseLinearConstraints() ) |
| 55 | { |
| 56 | if ( plConstraint->constraintObsolete() ) |
| 57 | { |
| 58 | continue; |
| 59 | } |
| 60 | switch ( plConstraint->getType() ) |
| 61 | { |
| 62 | case PiecewiseLinearFunctionType::RELU: |
| 63 | encodeReLUConstraint( gurobi, (ReluConstraint *)plConstraint, relax ); |
| 64 | break; |
| 65 | case PiecewiseLinearFunctionType::LEAKY_RELU: |
| 66 | encodeLeakyReLUConstraint( gurobi, (LeakyReluConstraint *)plConstraint, relax ); |
| 67 | break; |
| 68 | case PiecewiseLinearFunctionType::MAX: |
| 69 | encodeMaxConstraint( gurobi, (MaxConstraint *)plConstraint, relax ); |
| 70 | break; |
| 71 | case PiecewiseLinearFunctionType::SIGN: |
| 72 | encodeSignConstraint( gurobi, (SignConstraint *)plConstraint, relax ); |
| 73 | break; |
| 74 | case PiecewiseLinearFunctionType::ABSOLUTE_VALUE: |
| 75 | encodeAbsoluteValueConstraint( gurobi, (AbsoluteValueConstraint *)plConstraint, relax ); |
| 76 | break; |
| 77 | case PiecewiseLinearFunctionType::DISJUNCTION: |
| 78 | encodeDisjunctionConstraint( gurobi, (DisjunctionConstraint *)plConstraint, relax ); |
| 79 | break; |
| 80 | default: |
| 81 | throw MarabouError( MarabouError::UNSUPPORTED_PIECEWISE_LINEAR_CONSTRAINT, |
| 82 | "GurobiWrapper::encodeInputQuery: " |
| 83 | "Unsupported piecewise-linear constraints\n" ); |
| 84 | } |
| 85 | } |
| 86 | |
| 87 | // Add Nonlinear Constraints |