HSMT assessment - Githubissues

GaloisInc / cryptol

Cryptol: The Language of Cryptography

https://galoisinc.github.io/cryptol/master/RefMan.html

BSD 3-Clause "New" or "Revised" License

1.14k stars 126 forks source link

HSMT assessment #33

Closed kiniry closed 10 years ago

kiniry commented 10 years ago

possibly pull in HSMT (from Minho) to replace the back-end of SBV?

LeventErkok commented 10 years ago

That'd be something to look at, but arguably that's an SBV task; not a Cryptol one. I'd say "don't fix what's not broken." Your precious cycles would probably be better spent elsewhere.

The issue with HSMT is that it's not a perfect fit. Not every solver out there precisely implements SMT-Lib2; each has its own quirks and SBV sort of adapted them as they moved along. While this is not a very desirable position, it's beyond SBV's (and arguably Cryptol's) control on how these solvers evolve.

brianhuffman commented 10 years ago

Closing because it is outside the scope of Cryptol; as Levent says this is a design decision and task for the SBV project.