CIF/BDD: BddUtils.getVarDomain is very inefficient for large domains
Currently, BddUtils.getVarDomain creates a disjunction between each of the different values of the CIF variable's domain. So, if it has a thousand values, then a thousand BDDs are created and a disjunction is created 999 times. It would be much more efficient to create lower <= x and x <= upper.
An exception may be very small domains, where the current approach is maybe more efficient. Another exception is cases where lower is the lowest representable value, as then x >= lower is true, and similar for upper. Although I'm not yet sure handling these exceptional cases differently pays off enough to justify the added complexity.
Changing this improves performance for the cases where this method is used:
- Creating the update relation for input variables.
- Adding implicit variable never-out-of-range requirements.
- Determining the initialization predicate for discrete variables initialized using
in any.
Furthermore, I'm trying to get rid of all BDDDomain.ithVar uses for #458 (closed), and BddUtils.getVarDomain is the only non-trivial use of this method.
Addresses #458 (closed)