Unify variable/expression domains

[glebbelov]

From expressions such as

    ==> a+b >= 5;

and similar, we should construct an ideally precise domain of the expression (in this case, a+b) and use it for efficient representation. Example: #267.

Discussion: https://docs.google.com/document/d/1IWsQLhHbGTHUu3_XeRg99KCGct5KRdNo00AR806HGEw/edit?usp=sharing.

• Preset best defaults for major solvers
• Also for (partially) synced domains, such as ((x<=5 && y<=3) || (x>=7 && y>=9)) && x!=3.
• For Unary Encoding, track which bits are actually used/needed.
• SOS1/logarithmic encoding of domain disjunctions, and any large disjunctions?
• Sync with PL expressions, e.g., when the PL arg/res variable is domain-constrained, or the whole PL is defined via disjunction.