Support negative integers with data-based synthesis
Support negative integer literals, operations on negative integers, variables with negative ranges, and so.
Steps:
-
Adding the two's complement bit vector, with unit tests. -
Integrating the two's complement bit vector into synthesis, to support negative integer literals, and operations on it. -
Extending JavaBDD as needed. -
Supporting variables with negative ranges in synthesis.
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).