Simplify `IntDomTuple` witness invariants

[sim642]

Before this PR, IntDomTuple outputted witness invariants as conjunction of those from each int domain. Except when it was a definite integer, then only the single equality was returned.

This PR extends this logic to avoid obviously redundant and duplicate information in witness invariants, which can make them annoyingly large:

1. If it is a definite integer, output single equality.
2. If it is inclusion set, output conjunction of equalities (interval bounds and exclusions are redundant).
3. Otherwise, output interval bounds based on all integer domains (avoids duplicate bounds from def_exc exclusion bit ranges). Moreover, exclusion set is filtered based on that interval because often def_exc has x != 0 which is pointless if interval has some strictly positive bounds. Congruence and interval set (latter not used in SV-COMP) domains are added unchanged, so all known information should still be there.

TODO

• [x] Add option: ana.base.invariant.int.simplify.

[michael-schwarz]

Congruence ... (not used in SV-COMP)

I think congruences are enabled by the autotuner.

[sim642]

I think congruences are enabled by the autotuner.

Sorry, yes. I meant that just about interval sets.

[sim642]

There's now an option to disable these simplifications. This includes the possibility to even disable the definite integer simplification. These simplifications are the default, to give nicest output out of the box. If this turns out to not be precise enough and the abstract values are better, the option can be changed. Although it would be nicer to improve all simplifications for such cases as well, if possible.