| 591 | } |
| 592 | |
| 593 | void MILPEncoder::encodeSoftmaxConstraint( GurobiWrapper &gurobi, SoftmaxConstraint *softmax ) |
| 594 | { |
| 595 | Vector<double> sourceLbs; |
| 596 | Vector<double> sourceUbs; |
| 597 | Vector<double> sourceMids; |
| 598 | Vector<double> targetLbs; |
| 599 | Vector<double> targetUbs; |
| 600 | Vector<unsigned> sourceVariables = softmax->getInputs(); |
| 601 | Vector<unsigned> targetVariables = softmax->getOutputs(); |
| 602 | unsigned size = sourceVariables.size(); |
| 603 | for ( unsigned i = 0; i < size; ++i ) |
| 604 | { |
| 605 | double sourceLb = _tableau.getLowerBound( sourceVariables[i] ); |
| 606 | sourceLbs.append( sourceLb - GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); |
| 607 | double sourceUb = _tableau.getUpperBound( sourceVariables[i] ); |
| 608 | sourceUbs.append( sourceUb + GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS ); |
| 609 | sourceMids.append( ( sourceLb + sourceUb ) / 2 ); |
| 610 | targetLbs.append( _tableau.getLowerBound( targetVariables[i] ) ); |
| 611 | targetUbs.append( _tableau.getUpperBound( targetVariables[i] ) ); |
| 612 | } |
| 613 | |
| 614 | for ( unsigned i = 0; i < size; ++i ) |
| 615 | { |
| 616 | // The output is fixed, no need to encode symbolic bounds |
| 617 | if ( FloatUtils::areEqual( targetLbs[i], targetUbs[i] ) ) |
| 618 | continue; |
| 619 | else |
| 620 | { |
| 621 | // lower-bound |
| 622 | bool wellFormed = true; |
| 623 | List<GurobiWrapper::Term> terms; |
| 624 | terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", targetVariables[i] ) ) ); |
| 625 | double symbolicLowerBias; |
| 626 | bool useLSE2 = false; |
| 627 | for ( const auto &lb : targetLbs ) |
| 628 | { |
| 629 | if ( lb > GlobalConfiguration::SOFTMAX_LSE2_THRESHOLD ) |
| 630 | useLSE2 = true; |
| 631 | } |
| 632 | if ( !useLSE2 ) |
| 633 | { |
| 634 | symbolicLowerBias = NLR::DeepPolySoftmaxElement::LSELowerBound( |
| 635 | sourceMids, sourceLbs, sourceUbs, i ); |
| 636 | if ( !FloatUtils::wellFormed( symbolicLowerBias ) ) |
| 637 | wellFormed = false; |
| 638 | for ( unsigned j = 0; j < size; ++j ) |
| 639 | { |
| 640 | double dldj = NLR::DeepPolySoftmaxElement::dLSELowerBound( |
| 641 | sourceMids, sourceLbs, sourceUbs, i, j ); |
| 642 | if ( !FloatUtils::wellFormed( dldj ) ) |
| 643 | wellFormed = false; |
| 644 | terms.append( |
| 645 | GurobiWrapper::Term( -dldj, Stringf( "x%u", sourceVariables[j] ) ) ); |
| 646 | symbolicLowerBias -= dldj * sourceMids[j]; |
| 647 | } |
| 648 | } |
| 649 | else |
| 650 | { |
nothing calls this directly
no test coverage detected