Idea: introduce a conditional that can prune constraints/vars

[pvdz]

This is related to multiverse and how the input data from which the constraints are generated is modeled as a tree. In such a model certain branches fan out into other branches. But that model also makes unchosen branches completely irrelevant. Finitedomain will still want to solve all those constraints unless told otherwise. That bit is currently not possible in finitedomain and as such, the conditional doesn't improve anything.

• The conditional is a logical "implication" (if x then y. if not x then y can be anything)
• A new constraint should be introduced that applies this logic, similar to how reifiers work. When the constraint is set to false, it should remove certain given constraints from the current search node onwards. This way the engine won't bother with solving unused parts of the tree.
• Finitedomain is currently not aware of any higher model than a "constraint". And even those are compiled to even lower level "propagators" which have no concept of higher level models. This introduction would slightly change that and it's not certain what kind of effect that will have on things, especially when used in conjunction with one another.
• Should save considerably in large data sets, especially if branches are ignored often.
• Currently the conditional is implemented as a sort of lte(eq(A, B), eq(C, D)), meaning "if A=B then C=D, but if A!=B then don't care about C and D"). This introduces three constraints where maybe one specific one "implication constraint" could suffice, in a similar way as reifiers do. This constraint could then also contain a list of constraints that the condition omits when "A != B". Should be trivial to search that list through the list of unsolved propagators or variables and prune them accordingly.
• An implication constraint could be confusing, similar to how reifiers are kind of confusing. Reifiers don't enforce their operation, they reflect it. However, once a reifier solves its result var, this result is enforced and as such it can still enforce the operation or its inverse. Implication would be even more different in that the left side basically determines whether or not the right side gets solved at all. So it should probably not be called "implication" in the first place.