Extending Linear Two-Variable Equalities with Coefficients

[DrMichaelPetter]

PRs #1297 and #1412 brought an efficient implementation of conjunctions of basic linear two-variable equalities of the form

However, the same basic principle for the domain can be transferred to conjunctions of the form

with a minimal amount of additional runtime overhead. These kinds of equalities however promise to be a lot more useful for either directly proving invariants or refining e.g. intervals.

** Implementation **

We need to

• add two more integers to each right-hand-side
• migrate essential domain functions like forget, meet and join
• revisit linearTwoVarEqualitiesDomain and exploit new capabilities

[michael-schwarz]

LGTM!