Signed BitVec

[bruderj15]

Extend currently implemented unsigned BitVec by sign.
Promote encoding of the corresponding Haskell-Bitvector to the type-level:

data BvEnc = None | Ones | Twos
data SMTSort = BoolSort | ... | BvSort Nat BvEnc

Implement seperate instances: Num, Bounded, Integraled, ...

API for building formulas stays the same, implementation differs. Good.
Types in the API break. Bad. Just release as next major version

x <- var @(BvSort 8)

now becomes

x <- var @(BvSort 8 None)

After parsing solution we need to lookup the encoding in our state-monad. Or can the solver by any chance tell us?
Do not make the Parser do that, add an extra layer.
There will probably be some troubles here.

[bruderj15]

Too much noise.
Just stray a little from the official SMTLib-Spec and add another sort SBvSort for signed bvs.
Maybe rename BvSort to UBvSort for unsigned bvs. Breaks API.
Implementation is straight forward.