search

bruderj15 / Hasmtlib

A monad for interfacing with external SMT solvers
GNU General Public License v3.0
11 stars 1 forks source link

Signed BitVec #42

Closed bruderj15 closed 1 month ago

bruderj15 commented 3 months ago

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 commented 2 months ago

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.