#458 CIF/BDD: support discrete/input variables with negative integer values

• Introduction:
  • After quite a few preparation steps, it is finally here: CIF/BDD discrete/input variables with negative integer values.
  • Quite some changes in this one. More than I had expected. Some changes I made for things I encountered along the way, like cleaning and fixing small things in comments and so on. Could have made separate merge request, but these are now in separate commits and they are small and simple. They wouldn't make reviewing the whole thing much easier, so it didn't seem worth the significant effort to split them out again.
• End-user visible changes:
  • CIF data-based synthesis and CIF controller properties checker BDD-based checks now allow models with discrete/input variables with integer types that allow negative integer values, as well as those that include max_int as possible value. Instead, now the total number of possible values of the integer type must not exceed max_int.
• Other/detailed changes:
  • Added CifTypeUtils.getPossibleValuesCount(IntType).
  • Renamed CifBddDomain.getVarNum to getVarCount.
  • BDD bit vectors:
    • Added getLower/getUpper/getLowerInt/getUpperInt methods. Besides uses in 'regular' code, they are also used in various BDD bit vector tests instead of countInt, to improve readability/understandability of the tests.
    • createFromDomain no longer interprets the bits, nor does it add any bits. Also aligned the createFromDomain implementations in both classes to be more similar.
    • Adapted code to account for CifBddDomain never being empty.
    • setDomain now allows any domain, no longer interprets the bits, requires that the bits fit exactly in the vector, and is now implemented in the base class. Moved related tests also to test class that tests base classs.
    • Shared more code between comparison tests.
  • CifBddVariable has various improvements:
    • Some JavaDoc improvements. Also fixed JavaDoc: it is count that must be at least one, not lower.
    • It is now supported for upper to be max_int. It does still require that count fits in an int, which imposes restrictions on the combination of lower and upper.
    • The count is now derived from lower and upper, rather than passed in on construction.
    • Added createBitVector and createBitVectorForExtraDomain methods.
    • Adapted derived classes to match these changes. Also updated all constructor calls, to account for count no longer being a parameter.
  • CifBddEdge: updated for BDD domains allowing negative values.
  • CifToBddConverter: modernized code a bit, and updated for BDD domains allowing negative values. The calculation of error predicates for the conversion of updates took me considerable time to get right, and is not entirely trivial.
  • BddToCif: some small code/JavaDoc improvements, modernize code a bit, updated for BDD domains with negative values. The expressions for algebraic 'bit' variables for 'nodes' output of synthesis are not as nice as I'd like, but I couldn't think of a simpler way to get it to work that can be represented as CIF predicates.
  • BddUtils: small code improvements, updated for BDD domains with negative values, improved tests a bit.
  • ConfluenceCheck: updated for BDD domains with negative values
  • CIF data-based synthesis integration tests: update preconditions test model and its output, added some new tests or extended existing ones for the negative integers and related changes, test_databased.tooldef adapted to no longer crash on countring the number of states of state spaces with deadlock states.
  • Added extra unit tests, to test code that got changed and didn't yet have tests, as well as some new code. I found several issues this way, and serves also as regression tests in case we change things.

Addresses #458 (closed)