Revive max constraint #519
Conversation
There was a problem hiding this comment.
I left a bunch of comments - most are cosmetic, but some are real.
One question that I had that didn't make it into the comments:
in MaxConstraint::getPhaseStatusInAssignment, if f currently has an assignment greater than all the elements, we return phase = ELIMINATED, even if there are no eliminated variables. Is this intended? If it is, maybe add a comment.
src/engine/MaxConstraint.cpp
Outdated
| auto byAssignment = [&](const unsigned& a, const unsigned& b) { | ||
| return _assignment[a] < _assignment[b]; | ||
| }; | ||
| double maxValue = _assignment.get( *std::max_element( _elements.begin(), |
There was a problem hiding this comment.
if f has the maximal assignment, won't just grab f's value as "maxValue"? I think you want to exclude f's value from the computation?
There was a problem hiding this comment.
I think this line is getting the element with the maximal assignment?
There was a problem hiding this comment.
Still not convinced. std::max_element doesn't distinguish between max's f and its elements, no?
I think if you have f=max(x1,x2), and currently f=7, x1=x2=1, you would get maxValue = 7.
There was a problem hiding this comment.
I still think the code is correct, since "_elements" contains only input variables to Max and does not include _f. But I do think the code is more confusing than it needs to be. I got rid of the std::max_element business.
…Verification#514) * minor * minor * Update AbsoluteValueConstraint.cpp * Update SignConstraint.cpp * make all disjuncts bounds * minor * add transform constraint method to PLConstraint.h * split equality into two inequality * override * Update DisjunctionConstraint.cpp * progress * soi for dijsunction * change function name. Add clarification to unit tests * expand on comment * minor * minor * Update DisjunctionConstraint.cpp * progress * soi for dijsunction * Update AbsoluteValueConstraint.cpp * Update SignConstraint.cpp * minor * minor * minor * make all disjuncts bounds * add transform constraint method to PLConstraint.h * split equality into two inequality * minor * fix test * support disjunction * Update GlobalConfiguration.cpp * serailize disjunction (NeuralNetworkVerification#517) Co-authored-by: anwu <anwu@davidson.edu> * Upgrade OpenBLAS version. (NeuralNetworkVerification#516) * Update download_openBLAS.sh * Update OptionParser.cpp * Update Options.h * Update Options.cpp * Update main.cpp * Update main.cpp * Update main.cpp * Update Marabou.py * Update MarabouCore.cpp * Update CMakeLists.txt * Update MarabouCore.cpp * serailize disjunction (NeuralNetworkVerification#517) Co-authored-by: anwu <anwu@davidson.edu> * Upgrade OpenBLAS version. (NeuralNetworkVerification#516) * Update download_openBLAS.sh * Update OptionParser.cpp * Update Options.h * Update Options.cpp * Update main.cpp * Update main.cpp * Update main.cpp * Update Marabou.py * Update MarabouCore.cpp * Update CMakeLists.txt * Update MarabouCore.cpp * make all disjuncts bounds * add transform constraint method to PLConstraint.h * change function name. Add clarification to unit tests * expand on comment * progress * minor * minor * minor * add support soi function, revert unintental changes, make isZero() in LinearExpression const * mock constraint * remove left over * try to fix disjunction * add additional logic to handle corner case * make all disjuncts bounds * add transform constraint method to PLConstraint.h * change function name. Add clarification to unit tests * minor * minor * Update DisjunctionConstraint.cpp * progress * soi for dijsunction * Update AbsoluteValueConstraint.cpp * Update SignConstraint.cpp * minor * minor * progress * soi for dijsunction * minor * make all disjuncts bounds * add transform constraint method to PLConstraint.h * split equality into two inequality * minor * fix test * support disjunction * Update GlobalConfiguration.cpp * make all disjuncts bounds * add transform constraint method to PLConstraint.h * change function name. Add clarification to unit tests * expand on comment * progress * minor * minor * add support soi function, revert unintental changes, make isZero() in LinearExpression const * mock constraint * remove left over * try to fix disjunction * add additional logic to handle corner case * revert change * revert * handle corner case * virtual override * override issue * Update Test_Disjunction.h * Update Test_Disjunction.h * minor Co-authored-by: anwu <anwu@davidson.edu>
My attempt to clean up the MaxConstraint class.
Unit tests pretty much remains unchanged except that
I think in the next few PRs about context dependent object, we should probably just change addAuxilliraryEquations() to transformToUseAuxVariablesIfNeeded() in every constraint class. Because not using aux variables is no longer an option with the context dependent object.
Invariants to maintain in this class (also written in the header file):
Please also note that the case where the output variable is part of the input f = max (f, x1, x2...) is handled by transformtoUseAuxVariablesIfNeeded(). The method will add the constraint f >= x1, f>=x2 and make the constraint obsolete.