| 400 | } |
| 401 | |
| 402 | bool Checker::checkSingleVarSplits( const List<PiecewiseLinearCaseSplit> &splits ) |
| 403 | { |
| 404 | if ( splits.size() != 2 ) |
| 405 | return false; |
| 406 | |
| 407 | // These are singletons to tightenings |
| 408 | auto &frontSplitTightenings = splits.front().getBoundTightenings(); |
| 409 | auto &backSplitTightenings = splits.back().getBoundTightenings(); |
| 410 | |
| 411 | if ( frontSplitTightenings.size() != 1 || backSplitTightenings.size() != 1 ) |
| 412 | return false; |
| 413 | |
| 414 | // These are the elements in the singletons |
| 415 | auto &frontSplitOnlyTightening = frontSplitTightenings.front(); |
| 416 | auto &backSplitOnlyTightening = backSplitTightenings.front(); |
| 417 | |
| 418 | // Check that cases are of the same var and bound, where the for one the bound is UB, and for |
| 419 | // the other is LB |
| 420 | if ( frontSplitOnlyTightening._variable != backSplitOnlyTightening._variable ) |
| 421 | return false; |
| 422 | |
| 423 | if ( FloatUtils::areDisequal( frontSplitOnlyTightening._value, |
| 424 | backSplitOnlyTightening._value ) ) |
| 425 | return false; |
| 426 | |
| 427 | if ( frontSplitOnlyTightening._type == backSplitOnlyTightening._type ) |
| 428 | return false; |
| 429 | |
| 430 | return true; |
| 431 | } |
| 432 | |
| 433 | PiecewiseLinearConstraint * |
| 434 | Checker::getCorrespondingReluConstraint( const List<PiecewiseLinearCaseSplit> &splits ) |