Expand TypedValue type
The SBV-module needs to be expanded for various types. I.e. support for signed and unsigned bit vectors as well as (unbounded) integers needs to be provided. Arithmetic operations need to follow certain rules:
- Operations on BitVectors of same type result in a BitVector of same type.
- Operations on BitVectors of different type should not be allowed.
- The result of numerical Operations on Booleans should be treated as integer (in Matlab: double)
- BitVectors may not overflow or underflow (Being capped at minValue or maxValue)
(Note: Considering an SBV instance for TypedValue may be an option to simplify handling of variables of different type?)