Redefinition context

[glebbelov]

This issue tracks implementation of checks ensuring that redefinitions consider expression context. Related: #153 #201.
Example:

minimize Obj:
   if x==1 then 1;

s.t. Con:
   numberof 1 in (x) >= 1;

When IfThen is flattened, it produces conditional expression for x==1 in negative context. Then, only when numberof is redefined, it adds positive context to x==1. Make sure this happens before x==1 is redefined.

Tasks.

1. Implement checks that context is not extended beyond that used for redefinition.
2. Or, alternatively, enable redefinition context extension. This is likely not necessary as long as we don't support model modification.
3. Partial topological sorting of the redefinition graph to stay correct. UnaryEncodings are redefined last, and then their CondLinConEQs; to avoid adding new context to previously redefined CondLinConEQ's. However they are now redefined straight into indicators, to avoid adding new context to Or.
4. Full topological redefinition graph sorting.
5. Refactor to only pass the graph once and implement (redundant) checks that no constraints are added whose reformulation is finished