We currently have simplification rules that changes min to max and max to min as follows where c1 and c2 are constants (let’s call them set 1)
min(c1 - x, c2) -> c1 - max(x, c1-c2) max(c1 - x, c2) -> c1 - min(x, c1-c2)
My guess about the motivation behind these rules is that they try to keep the coefficient of
x positive. is that correct? If yes, (a) what if x itself has a negative sign (b) what do we achieve by this rule?
Now consider the following new rules (set 2)
max(a,b) - a -> max(0, b-a) min(a,b) - a -> min(0, b-a) a - max(a,b) -> min(0, a-b) a - min(a,b) -> max(0, a-b) ...
Note that we can’t have both sets because they lead to infinite recursion. I need set 2 because of the following simplification I have to make in some experimental code:
min (5-min(x,5), max(x,5)-5) --set2--> min(max(5-x,0), max(x-5,0)) --existing rules--> min(max(5-x,x-5),0) --new rule--> 0
where new rule is
min(max(a,-a),0) -> 0
I can think of two suggestions:
Add set 2 and remove set 1 (if there is no good reason to keep set 1)
Add set 2 and add restriction
c2 != 0to set 1 to get rid of infinite recursion
It seems to me that if I don’t add set 2, then I have to come up with an overly complicated (and non-minimal) rule to take care of the specific example above.