| 1590 | } |
| 1591 | |
| 1592 | void Engine::performMILPSolverBoundedTightening( InputQuery *inputQuery ) |
| 1593 | { |
| 1594 | if ( _networkLevelReasoner && Options::get()->gurobiEnabled() ) |
| 1595 | { |
| 1596 | // Obtain from and store bounds into inputquery if it is not null. |
| 1597 | if ( inputQuery ) |
| 1598 | _networkLevelReasoner->obtainCurrentBounds( *inputQuery ); |
| 1599 | else |
| 1600 | _networkLevelReasoner->obtainCurrentBounds(); |
| 1601 | |
| 1602 | // TODO: Remove this block after getting ready to support sigmoid with MILP Bound |
| 1603 | // Tightening. |
| 1604 | if ( _milpSolverBoundTighteningType != MILPSolverBoundTighteningType::NONE && |
| 1605 | _preprocessedQuery->getNonlinearConstraints().size() > 0 ) |
| 1606 | throw MarabouError( MarabouError::FEATURE_NOT_YET_SUPPORTED, |
| 1607 | "Marabou doesn't support sigmoid with MILP Bound Tightening" ); |
| 1608 | |
| 1609 | switch ( _milpSolverBoundTighteningType ) |
| 1610 | { |
| 1611 | case MILPSolverBoundTighteningType::LP_RELAXATION: |
| 1612 | case MILPSolverBoundTighteningType::LP_RELAXATION_INCREMENTAL: |
| 1613 | case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_ONCE: |
| 1614 | case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE: |
| 1615 | _networkLevelReasoner->lpRelaxationPropagation(); |
| 1616 | break; |
| 1617 | case MILPSolverBoundTighteningType::MILP_ENCODING: |
| 1618 | case MILPSolverBoundTighteningType::MILP_ENCODING_INCREMENTAL: |
| 1619 | _networkLevelReasoner->MILPPropagation(); |
| 1620 | break; |
| 1621 | case MILPSolverBoundTighteningType::ITERATIVE_PROPAGATION: |
| 1622 | _networkLevelReasoner->iterativePropagation(); |
| 1623 | break; |
| 1624 | case MILPSolverBoundTighteningType::NONE: |
| 1625 | return; |
| 1626 | } |
| 1627 | List<Tightening> tightenings; |
| 1628 | _networkLevelReasoner->getConstraintTightenings( tightenings ); |
| 1629 | |
| 1630 | |
| 1631 | if ( inputQuery ) |
| 1632 | { |
| 1633 | for ( const auto &tightening : tightenings ) |
| 1634 | { |
| 1635 | if ( tightening._type == Tightening::LB && |
| 1636 | FloatUtils::gt( tightening._value, |
| 1637 | inputQuery->getLowerBound( tightening._variable ) ) ) |
| 1638 | inputQuery->setLowerBound( tightening._variable, tightening._value ); |
| 1639 | if ( tightening._type == Tightening::UB && |
| 1640 | FloatUtils::lt( tightening._value, |
| 1641 | inputQuery->getUpperBound( tightening._variable ) ) ) |
| 1642 | inputQuery->setUpperBound( tightening._variable, tightening._value ); |
| 1643 | } |
| 1644 | } |
| 1645 | else |
| 1646 | { |
| 1647 | for ( const auto &tightening : tightenings ) |
| 1648 | { |
| 1649 | if ( tightening._type == Tightening::LB ) |
nothing calls this directly
no test coverage detected