MCPcopy Create free account
hub / github.com/NeuralNetworkVerification/Marabou / collectFixedValues

Method collectFixedValues

src/engine/Preprocessor.cpp:650–707  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

648}
649
650void Preprocessor::collectFixedValues()
651{
652 // Compute all used variables:
653 // 1. Variables that appear in equations
654 // 2. Variables that participate in PL and nonlinear constraints
655 // 3. Variables that have been merged (and hence, previously
656 // appeared in an equation)
657 Set<unsigned> usedVariables;
658 for ( const auto &equation : _preprocessed->getEquations() )
659 usedVariables += equation.getParticipatingVariables();
660 for ( const auto &constraint : _preprocessed->getPiecewiseLinearConstraints() )
661 {
662 for ( const auto &var : constraint->getParticipatingVariables() )
663 usedVariables.insert( var );
664 }
665 for ( const auto &constraint : _preprocessed->getNonlinearConstraints() )
666 {
667 for ( const auto &var : constraint->getParticipatingVariables() )
668 usedVariables.insert( var );
669 }
670 for ( const auto &merged : _mergedVariables )
671 usedVariables.insert( merged.first );
672
673 // Collect any variables with identical lower and upper bounds, or
674 // which are unused
675 for ( unsigned i = 0; i < _preprocessed->getNumberOfVariables(); ++i )
676 {
677 if ( FloatUtils::areEqual( getLowerBound( i ), getUpperBound( i ) ) )
678 {
679 _fixedVariables[i] = getLowerBound( i );
680 }
681 else if ( !usedVariables.exists( i ) )
682 {
683 // If possible, choose a value that matches the debugging
684 // solution. Otherwise, pick an arbitrary values. If the
685 // bounds are infinite for this variable, set them
686 // arbitrarily as well.
687 if ( _preprocessed->_debuggingSolution.exists( i ) &&
688 _preprocessed->_debuggingSolution[i] >= getLowerBound( i ) &&
689 _preprocessed->_debuggingSolution[i] <= getUpperBound( i ) )
690 {
691 _fixedVariables[i] = _preprocessed->_debuggingSolution[i];
692 }
693 else
694 {
695 if ( FloatUtils::isFinite( getLowerBound( i ) ) )
696 _fixedVariables[i] = getLowerBound( i );
697 else if ( FloatUtils::isFinite( getUpperBound( i ) ) )
698 _fixedVariables[i] = getUpperBound( i );
699 else
700 _fixedVariables[i] = 0;
701 }
702
703 setLowerBound( i, _fixedVariables[i] );
704 setUpperBound( i, _fixedVariables[i] );
705 }
706 }
707}

Callers

nothing calls this directly

Calls 5

getEquationsMethod · 0.80
insertMethod · 0.45
getNumberOfVariablesMethod · 0.45
existsMethod · 0.45

Tested by

no test coverage detected