Extend ReLU/Max constraint with SoI cost term. #502
Conversation
Moved computeHeuristicCost from Engine to CostFunctionManager
…/Marabou into marabou-soi-cont
| Compute the error of the current assignment with respect to the cost compoenent | ||
| corresponding to the given phase. | ||
| */ | ||
| virtual double computeCostFunctionComponent( PhaseStatus /* phase */ ) const |
There was a problem hiding this comment.
Due to their names, it sounds like {add/compute}CostFunctionComponent are doing similar things. But I guess compute is computing not the component, but its value?
There was a problem hiding this comment.
Yeah exactly. add is adding a "symbolic term" to the cost function, compute returns the values of the term based on the current assignment.
| This is done in the SumOfInfeasibilitiesManager class, which maintains/updates the | ||
| SoI function. | ||
| */ | ||
| virtual void removeCostFunctionComponent( Map<unsigned, double> &/* cost */, |
There was a problem hiding this comment.
Instead of add/remove, why not have a get(), and let the manager do with it as it will?
There was a problem hiding this comment.
Yeah that makes sense. I'll defer this method to the SoIManager class.
wu-haoze
changed the title
|
Updates: |
| @@ -512,11 +512,10 @@ List<PiecewiseLinearConstraint::Fix> MaxConstraint::getSmartFixes( ITableau * ) | |||
|
|
|||
| List<PhaseStatus> MaxConstraint::getAllCases() const | |||
| { | |||
| if ( _phaseStatus != PHASE_NOT_FIXED ) | |||
| if ( phaseFixed() ) | |||
There was a problem hiding this comment.
This is a quick fix to the issue (#504) resulting from the refactored MaxConstraint. For now this is probably enough for the current master to be sound, because most of the refactored functionality is not in use. A more thorough change in the MaxConstraint is needed for the context dependent stuff to be actually usable.
| #define __LinearExpression_h__ | ||
|
|
||
| #include "Map.h" | ||
|
|
There was a problem hiding this comment.
Is this class different from the Equation class? Can we use the existing one?
There was a problem hiding this comment.
The difference is that linear expression is the lhs of an equation plus a constant: Ax +b
There was a problem hiding this comment.
Okay. I believe an equation is Ax = b, so it could also be used, right?
Just trying to reduce code duplication
There was a problem hiding this comment.
Never mind, I take my comment back. I think the linear expression has a sufficiently different meaning
| @@ -785,3 +832,21 @@ String MaxConstraint::serializeToString() const | |||
|
|
|||
| return output; | |||
| } | |||
|
|
|||
…tion#502) * change tableau for optimization * optimize a cost function * minor * Cost function manager unit test * Add unit test * make optimization code public * fix numerical issue * add unit tests for tableau * Changed {is/not}Optimizing to toggleOptimization. Moved computeHeuristicCost from Engine to CostFunctionManager * extend relu constraints with soi * add unit test * Update PiecewiseLinearConstraint.h * change add/removeCostTerm to getCostTerm * add SoI for Max * add linear expression struct * add two more unit tests * change from HeuristicCost to LinearExpression * make linear expression a class * minor * Update MaxConstraint.cpp
Add methods in the ReLU constraints to contribute a cost term in the SoI function. This is a small PR.
The next one is more involved with a SumOfInfeasibilitiesManager class which maintains/update the current heuristic cost (sum of the cost terms from the piecewise linear constraints).