Support negative integers with data-based synthesis

Support negative integer literals, operations on negative integers, variables with negative ranges, and so on.

Steps:

• Adding the two's complement bit vector, with unit tests. (!1254 (merged))
• Renamed the non-negative CIF/BDD bit vector related classes. And introduce a common base class for both CIF/BDD bit vector representations. Put in a separate bitvectors package. (!1266 (merged))
• Integrating the two's complement bit vector into synthesis, to support negative integer literals, support unary negation, and allow arbitrary use of binary subtraction. (!1290 (merged))
• Consider renaming TwosComplementCifBddBitVector to something shorter. See !1290 (comment 3783266). (!1311 (merged))
• Resolve use of BDDDomain.ithVar in BddUtils.getVarDomain (see #1199 (closed)).
• Introduce CifBddDomain, replacing JavaBDD's BDDDomain, making sure CifDddDomain doesn't assume anything at what the bits represent. (!1306 (merged))
• Supporting variables with negative ranges in synthesis. (!1312 (merged))
• Update multi-level splitter to support integer types that allow negative values. (!1317 (merged))
• Optimize bit vector operations to not increase the length unnecessarily. See !1290 (comment 3783258).

Original description

Currently, data-based synthesis only supports positive integers (including zero). Conceptually, data-based synthesis should work fine with negative integers as well, as long as the range remains finite. So probably there are some (BDD?) implementations details that makes working with negative integers more difficult.

The motivation for this issue is that I'm implementing a UPPAAL model in CIF that contains negative integers. While a workaround is to shift all integer values in the CIF model so they become positive, doing this looses some tracability with the UPPAAL model and the underlying meaning of the variable in the model (the variable tracks a discrete speed of a vehicle, a negative speed implies drying backwards).